Double

ESC

• ESC attempts to find common run-time 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.

Following doubles each value of array. 
 

• Pragmas define pre and postconditions and loop-invariants.
   
  • pre - method parameter A != null

    ensures A has at least 1 element

  • post (\forall int j; 0 <= j && j < A.length; A[j] == 2 * \old( A[j] ) )

    \old( v ) refers to the value of variable v before the method call or loop.

    The postcondition ensures that all A[j] == 2 * \old( A[j] ) )

        A[0]=2*A[0], ..., A[j]=2*A[j]

  • loop-invariant - for all 0<=j && j < i the condition A[j] == 2 * \old A[j] is true.
     

    (\forall int x ;            range(x);            p(x) )

    Universal quantifier over range(x) for quantifier expression p(x)

    Means the condition is always true for all indices < i.

    Note that i is from the loop of: i=0; while( i<A.length) { ... })

    When i=0, 0<=j && j < i is false and the loop invariant is not violated.

• Initialization, Maintenance and Termination
   
  • loop_invariant (\forall int j; 0<=j && j < i; A[j] == 2 * \old( A[j] ))

    for all 0<=j && j < i the condition A[j] == 2 * \old A[j] is true. Means the condition is always true for all indices j, 0£j< i.

    Initialization: Prior to first iteration of while statement: i=0 and j<i, A[0..j] is empty.

    Maintenance: At start and end of each iteration of while statement: A[j] = 2* \old( A[j] )) for j<i.

    Termination: i=A.length, by loop invariant A[0..i-1] = 2*\old(A[0..i-1])

class Double { //@ pre A != null; //@ post (\forall int j;                           0 <= j && j < A.length;                           A[j] ==2*\old(A[j]) );    void dbl(int A[]) {       int i=0;       //@ loop_invariant                   (\forall int j;                              0<=j && j < i;                              A[j] == 2 * \old( A[j] ));          while(i < A.length) {               A[i]=2*A[i];               i = i + 1;           }    } }

Question 2.8

1. Does the postcondition:

       //@ post (\forall int j; 0 <= j && j < A.length; A[j] ==2*\old(A[j]) );

   hold when the loop is changed to:

   i=5;
   while(i < A.length) { ...

2. Does the loop invariant still hold when changed to:

   //@ loop_invariant (\forall int j; 5<=j && j < i; A[j] == 2*\old(A[j]) );

3. Does the loop invariant hold for:

   //@ loop_invariant (\forall int j; 0<=j && j < i ; j-1 <= i);

4. Does the above loop invariant serve any useful purpose?
    

Example

    Same as above but uses a for and function to perform the multiplication.

class Double { //@ pre A != null; //@ post (\forall int j; 0 <= j && j < A.length; A[j] ==twice(\old(A[j])) );    void dbl(int A[]) {       int i=0;       //@ loop_invariant (\forall int j; 0<=j && j < i; A[j] == twice(\old(A[j])) );       for(i=0; i< A.length; i++)           A[i]=twice(A[i]);    } //@ pre true; //@ post \result == 2*x;    int twice(int x) {       return 2*x;    } }