Code contracts: how to express these conditions?

Question

I'm currently playing with code contracts, and I'm not quite sure if the static methods of the Contract class are powerful enough to compete with the mathematical notation of conditions.

Suppose we got a simple factorial method

int Factorial(int n); 

I would state the following conditions:

 Precondition: n >= 0 Postconditions: Factorial(n) = 1, in case n = 0 Factorial(n) = n*(n-1)*...*1, in case n > 0 

These conditions clearly define Factorial behavior in a short and clean way. My question is whether they can be expressed through Code Contracts.

The precondition is trivial:

 Contract.Requires(n >= 0) 

A conditional message condition can be expressed using

 if(n==0) Contract.Ensures(Contract.Result<int>() == 1); if(n > 0) ... 

But I don't like the way I need the if statement here, as it makes it easier to read the usual list of preconditions and postconditions. I was hoping we would have something like

 Contract.Ensures(...).InCase(...); 

And last but not least, I don’t know how to express this, which is a general note regarding mathematics:

 n*(n-1)*...*1 

Suppose I need some kind of loop, but this will copy the entire implementation. Is there any smart way to express such designations?

Thanks in advance.

Answer 1

You can try the following:

 Contract.Ensures(Contract.Result<int>() == AlternativeFactorial(n)); 

where AlternativeFactorial :

 [Pure] public static int AlternativeFactorial(int n) { if(n==0) return 1; if(n > 0) { //Alternative implementation. } } 

Of course, everything that you use in the contract should be free from side effects (pure).

Now, as for the factorial implementation, I cannot come up with a more compact “alternative” implementation than w0lf. What you have to consider is changing the return value of your method from int to BigInteger . Factorials can become very large very quickly. Also note that adding a post-condition to a factorial value will almost double the time your method takes to return the result. This can be solved by building CodeContracts only in the debug configuration.

Answer 2

What you are looking for is Unit Tests, not Code Contracts.

Typically, tests such as if n=0, then f(n) = 1 and if n=3, then f(n) = 6 are test cases that should be expressed as unit tests.

In your case, I think that the appropriate message condition would look like "Result Always> = 1." And nothing more.

Assuming your factor class looks something like this:

 public class Factorial { public int Compute(int n) { if (n == 0) return 1; return n * Compute(n - 1); } } 

suitable Unit Test written with the NUnit Framework :

 [TestFixture] public class FactorialTests { [TestCase(0, 1)] [TestCase(1, 1)] [TestCase(2, 2)] [TestCase(7, 5040)] [TestCase(10, 3628800)] public void Compute_ReturnsCorrectResult(int n, int expectedResult) { var sut = new Factorial(); Assert.AreEqual(expectedResult, sut.Compute(n)); } } 

Update (after comments)

The result of the check> = 1 does not completely determine the algorithm.

I do not think that the work of Code Contract is to describe the algorithm in detail. the algorithm is specified by the method.

If Code Contract was complex logic similar to the method itself, then I think we will need a code contract to verify that the Code Contract is performing the correct checks. This obviously leads to infinite recursion.

I did not expect n*(n-1)*...*1 be accepted by the compiler. But some general range operator in the LINQ-matched way will undoubtedly be a complement to gread. From (n) .To (1) .Product () or From (n) .To (m) .Sum ()

If there was such a form of factorial expression (and probably is), you could use it in your code, and not in Code Contracts.

Update 2

Just for fun, I found a LINQ way to calculate Factorials:

 Enumerable.Range(1, n == 0 ? 1 : n).Aggregate((a, i) => a * i);