Maximum of an Array

Document last modified:

ESC

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.

Example - returns the maximum value in an array.

Pragmas define pre and postconditions and loop-invariants.
- pre - method parameter A.length > 0 && A != null
- post - \forall int j; 0 <= j && j <= n; A[j] <= \result
  
  that is: A[0], ..., A[n] <= Pk
Initialization, Maintainence and Termination

(\forall int x ; range(x); p(x) ) Universal quantifier over range(x) for quantifier expression p(x)
- //@ loop_invariant (\forall int j; 0 <=j && j <= i; A[j] <= Pk && i <= n);
  
  for all j the condition A[j] <= Pk is true && i <= n. Means the condition is always true for all indices <= i.
  
  \forall int j;                                       j will be a universal quantifier.
  
  0 <= j && j <= i                              j's range of values that must always be true
  
  A[j] <= Pk                                        expression that must hold for all j's in defined range.
  
  Initialization: Prior to first iteration of for statement: i=0 and j <= i, A[0] <= Pk is true.
  
  Maintenance: At beginning and end of each while iteration: A[0..i] <= Pk
  
  Termination: i = n, by loop invariant A[0..i] <= Pk

class MaxPk {

//@ pre true;
//@ post (\result >= x && \result >= y );

    	int maxOf(int x, int y) {
        		if (x > y)
            		return x;
        		else
            		return y;
	}

          int n;							// n defined globally for use in pre/post conditions

//@ pre A.length > 0 && A != null;
//@ post (\forall int j; 0 <= j && j <= n; A[j] <= \result );

	int maximum(int A[]) {

		int i=0;
		int Pk = A[i];
        		int n = A.length-1;

		//@ loop_invariant (\forall int j; 0 <=j && j <= i; A[j] <= Pk && i <= n);

		while (i < n) {
	           	Pk = maxOf(Pk, A[i+1]);
            		i = i + 1;
        		}  
	        	return Pk;
	}
}

Question 2.9.1

What is the effect of removing the precondition A != null?
What is violated by changing the postcondition to:

//@ post (\forall int j; 0 <= j && j <= n; A[j] == \result );
What would be violated by changing the loop starting point to:

i = 2;
What is violated by changing the loop-invariant to:

//@ loop_invariant (\forall int j; 0 <=j && j <= i; A[j] < Pk && i <= n);

ESCjava warning:

MaxPk.java:25: Warning: Loop invariant possibly does not hold (LoopInv)
       while (i < n) {
         ^
Associated declaration is "MaxPk.java", line 24, col 6:
      //@ loop_invariant (\forall int j; 0 <= j && j <= i; A ...
         ^

5. Why is this loop-invariant correct but not useful?

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

        while (i < n) {
           Pk = maxOf(Pk, A[i+1]);
            i = i + 1;
        }

Example - returns the index of the maximum value in an array.

Pragmas define pre and postconditions and loop-invariants.

pre - method parameter A != null
post - \forall int k; 0 <= k && k < A.length; A[\result] >= A[k]

that is: A[\result] >= A[0], ..., A[k] for 0 ≤ k<A.length

Initialization, Maintainence and Termination

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

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

loop_invariant (\forall int j;
                                    0<=j && j < i && 0 <= maxIndex && maxIndex < i;
                                    A[maxIndex] >= A[j]);
            for( i=0; i<A.length; i++)

for all j and maxIndex < i the condition A[maxIndex] >= A[j] is true. Means the condition is always true for all indices < i.

\forall int j;                                       j will be a universal quantifier.

0 <= j && j < i                                 j's range of values that must always be true

0 <= maxIndex && maxIndex < i; maxIndex's range of values that must always be true

A[maxIndex] >= A[j]                       expression that must hold for all j's and maxIndex's in defined range.

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

Maintenance: At beginning and end of each for iteration: A[maxIndex] >= A[0..j]

Termination: i=A.length, by loop invariant A[maxIndex] >= A[0..j]

class Maximum {

//@ pre A != null;
//@ post (\forall int k; 0 <= k && k < A.length; A[\result] >= A[k]);

       int maximum(int A[]) {

         int i=0;
         int maxIndex=0;

         /*@ loop_invariant
                     (\forall int j;
                                0 <= j && j < i && 0 <= maxIndex && maxIndex < i;
                                A[maxIndex] >= A[j]);
         *@/

         for( i=0; i<A.length; i++)
             if (A[i] > A[maxIndex])
                  maxIndex = i;
         return maxIndex;
     }
}

Question 2.9.2

What is the effect of removing the precondition A != null?
What is violated by changing the postcondition to:

//@ post (\forall int k; 0 <= k && k < A.length; A[\result] > A[k]);
What would be violated by changing the loop to:

for( i=5; i<A.length; i++)
What is violated by changing the loop-invariant to:

/*@ loop_invariant
               (\forall int j;
                          0<=j && j < i && 0 <= maxIndex && maxIndex < i;
                          A[maxIndex] > A[j]);
*@/

Example

ESCjava warns that the postcondition below may not be true because k quantifies non-existent elements of A when -1.

//@ post (\forall int k; -1 <= k && k < A.length; A[\result] >= A[k]);

Maximum.java:16: Warning: Postcondition possibly not established (Post)

Associated declaration is "Maximum.java", line 4, col 4:
//@ post (\forall int k; -1 <= k && k < A.length; A[\result] >= A[k]); ...
^