Common Example‎ > ‎

ArrayMax in Boogie

The length of array is passed as parameter as all Boogie maps are unbounded.

procedure max (a:[int]int, length :int) returns (max :int)
requires length >= 0;
ensures (forall j:int :: j >= 0 && j< length ==> max >= a[j]);
ensures length > 0 ==> (exists j:int :: j >= 0 && j<length && max == a[j]);
{
var i : int;
if(length ==0) { 
max :=0;}
else {
max := a[0];
i := 1;
while(i < length)
invariant (i<=length);
invariant (forall j:int :: j >=0 && j <i ==> max >=a[j]);
invariant (exists j:int :: j>=0 && j<i && max ==a[j]);
{
if(a[i] > max){
max := a[i];
}
i:=i+1;
}
}

}

Comments