Common Example‎ > ‎

ArrayMax in Jahob

  • Jahob only supports arrays of references, so a dummy wrapper class B with a single integer field "data" had to be used, yielding an array of type B[]
  • ++i did not work, so it was rewritten to i=i+1
  • the precondition contains additional information: 
    • array length is non-negative
    • all array elements have to be non-null

public class B{
public int data;
} 

public class ArrayMax {

    public static int max(B[] a)
/*:
requires "a ~= null & a..Array.length >= 0 & (ALL k. k >= 0 & k < a..Array.length --> a.[k] ~= null)"
ensures "(ALL j. j>=0 & j< a..Array.length --> result >= a.[j]..data) & 
               ((a..Array.length > 0) -->
               (EX j. j >= 0 & j < a..Array.length & result = a.[j]..data))"
      */
{
if ( a.length == 0 ){ return 0;}
int max = a[0].data;
int i = 1;
while 
/*: inv "i >= 0 & i <= a..Array.length & (ALL j. (j >= 0 & j < i) --> max >= a.[j]..data)
&(EX j. j >= 0 & j < i & max = a.[j]..data)"
*/
( i < a.length ) 

{
   if ( a[i].data > max ){ max = a[i].data; }
   i=i+1;
}
return max;
    }

}



Comments