Divide

ESC

• ESC attempts to find specification errors in Java programs by static analysis of the program text.
• ESC Language summary

  ESC expression (pragma)	Meaning
  pre p;	p is a precondition for the call
  post p;	p is a postcondition for the call
  loop_invariant p;	p is a loop invariant
  \result == e	e is the result returned by the call
  (\forall int x ; range(x); p(x) )	Universal quantifier over range(x) for quantifier expression p(x)
  \old( v )	The value of v prior to method call or loop.

   

The following example returns the quotient of division.
 

• Pragmas define pre and postconditions.
   
  • pre - method parameter b != 0
  • post - \result == a/b

class Divide { //@ pre b != 0; //@ post \result == a/b;        int divide(int a, int b) {          return a/b;      } }

Example

1. When the precondition is removed, ESCjava warns below:

Divide.java:7: Warning: Possible division by zero (ZeroDiv) return a/b;

2. ESCjava warns that the postcondition below may not be true.

//@ post \result == a*b;

Divide.java:7: Warning: Postcondition possibly not established (Post) Associated declaration is "Divide.java", line 4, col 4: //@ post \result == a * b;

Question 2.7

1. Find the weakest precondition and give the ESC pre annotation for:

//@ post \result >= 5; int increment(int x) { return x + 1; }

2. Give the ESC pre and postcondition annotations for:

int increment(int x) { return x + 1; }

ESC expression (pragma)	Meaning
pre p;	p is a precondition for the call
post p;	p is a postcondition for the call
loop_invariant p;	p is a loop invariant
\result == e	e is the result returned by the call
(\forall int x ; range(x); p(x) )	Universal quantifier over range(x) for quantifier expression p(x)
\old( v )	The value of v prior to method call or loop.