FoVeOOS'11 Competition: challenge 1, in Why3
Maximum of an array of integers, in Why3
Auteurs: Claude Marché
Catégories: Array Data Structure
Outils: Why3
Références: The COST FoVeOOS'11 Competition
see also the index (by topic, by tool, by reference, by year)
(* COST Verification Competition. vladimir@cost-ic0701.org Challenge 1: Maximum in an array Given: A non-empty integer array a. Verify that the index returned by the method max() given below points to an element maximal in the array. *) module ArrayMax use import int.Int use import int.MinMax use import ref.Ref use import array.Array let max (a: array int) = requires { 0 < length a } ensures { 0 <= result < length a /\ forall i:int. 0 <= i < a.length -> a[i] <= a[result] } let x = ref 0 in let y = ref (length a - 1) in while !x <> !y do invariant { 0 <= !x <= !y < length a /\ forall i:int. 0 <= i < !x \/ !y < i < length a -> a[i] <= max a[!x] a[!y] } variant { !y - !x } if a[!x] <= a[!y] then x := !x+1 else y := !y-1 done; !x end