Summary: Methd Postconditions -- a contract on method exit
Backto: SpecSharpIntroduction
Nearby: PreconditionsIntroduction

A method postcondition is a boolean expression that must hold on exit from the method. In Spec#, a method postcondition is considered to be part of the signature of a method. Among other things, this means that the references within a postcondition 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 postcondition must be public.

In general, a method postcondition should give enough information to a caller so that they can depend on the state after the call. In particular, this means it should provide enough information to satisfy the preconditions of methods called after this method returns.

Method postconditions are specified using the ensures keyword. For instance:

		 class A{
		   public static int [AddTogether(int] x, int y)
		     ensures result == x+y;
		   { return x + y; }
		 }
	

(Okay, so it is a particularly stupid example.) Note that the return value of the method can be referred to by the context-dependent keyword result. At runtime, postconditions are enforced by a check the Spec# compiler emits into the code; this check is evaluated on all non-exceptional returns (but see CheckedExceptions). When the static verification processes this method, it must prove that the postcondition holds when the method ends. When verifying calls to the method, its postcondition is assumed to hold. Here's an example using the method defined in PreconditionsIntroduction.

		 class Client{
		    public static void Main(){
		      int x = [A.AddTogether(4,2);]
		      [A.IntegerDivide(27,x);] // no error: can prove x != 0
		    }
		 }