Common Example‎ > ‎

ArrayMax in Krakatoa

  • deleted keyword public normal_behavior
  • changed syntax of quantification from \forall type c; range ; scope to \forall type c; range ==> scope
  • changed syntax of quantification from \exists type c; range ; scope to \exists type c; range && scope
  • changed decreases to loop_variant
  • no modifies clause in loop invariant
  • deleted pure from method declaration
  • turned off integer overflow checking with the //@+ CheckArithOverflow=no pragma at the beginning of document

//@+ CheckArithOverflow=no
public class ArrayMax2 {
    
    /*@
      @ requires a != null;
      @ ensures (\forall int j; (j >= 0 && j < a.length ==>
      @          \result >= a[j]))&&
      @         (a.length > 0 ==>
      @            (\exists int j; (j >= 0 && j < a.length &&
      @              \result == a[j])));
      @*/
    public static int max(int[] a) {
if ( a.length == 0 ) return 0;
        int max = a[0], i = 1; 
/*@ loop_invariant
 @  i <= a.length &&
 @  (\forall int j; j >= 0 && j < i ==> max >= a[j])
 @  &&
          @  (\exists int j; j>=0 && j<i &&  max==a[j]);
 @ 
 @ loop_variant a.length-i; 
 @*/
while ( i < a.length ) {
   if ( a[i] > max ) max = a[i];
   ++i;
}
return max;
    }

}


Comments