Summary: Method preconditions -- a contract on method entry
Backto: SpecSharpIntroduction
Nearby: PostconditionsIntroduction

A method precondition is a boolean expression that must hold on entry to the method. In Spec#, a method precondition is considered to be part of the signature of a method. Among other things, this means that the references within a precondition must be at least as accessible as the method itself. So if the method is public, then all of the members referred to in the precondition must be public.

In general, a method precondition should give enough information to a caller so that they can call the method with a guarantee that they will not cause an unexpected exception to be thrown. This means that they should either a) know statically that the condition is true, or b) be able to test the condition dynamically.

Method preconditions are specified using the requires keyword. For instance:

		 class A{
		   public static int [IntegerDivide(int] x, int y)
		     requires y != 0;
		   { return x / y; }
		 }
	

Note that the method does not check y for being non-zero, but instead depends upon the client never passing it such a value. At runtime, this is enforced by a check the Spec# compiler emits into the code on the callee side. When the static verification is used, the body of the method is verified under the assumption that the precondition holds. The static verification will produce an error message for calls in a program state in which the theorem prover cannot prove that the second argument is non-zero.

		 class Client{
		    public static void TryOK(int z)
		      requires z != 0;
		    {
		      [A.IntegerDivide(27,z);] // no error: can prove that z != 0
		    }
		    public static void [TryBad(int] z)
		    {
		      [A.IntegerDivide(27,z);] // error: cannot prove that z != 0
		    }
		    public static void Main(){
		      [A.IntegerDivide(4,2);] // no error: can prove 2 != 0
		      int z = 3;
		      [A.IntegerDivide(z,z);] // no error: can prove z != 0
		    }
		 }