examples/locate_max.mlw

   1 (** Simple example to illustrate the C memory model *)
   2
   3 use int.Int
   4 use map.Map as Map
   5 use mach.c.C
   6 use mach.int.Int32
   7 use mach.int.Int64
   8
   9 function ([]) (a: ptr 'a) (i: int): 'a = Map.get a.data.Array.elts (a.offset + i)
  10
  11 let locate_max (a: ptr int64) (n: int32): int32
  12   requires { 0 < n }
  13   requires { valid a n }
  14   ensures  { 0 <= result < n }
  15   ensures  { forall i. 0 <= i < n -> a[i] <= a[result] }
  16 = let ref idx = 0 in
  17   for j = 1 to n - 1 do
  18     invariant { 0 <= idx < n }
  19     invariant { forall i. 0 <= i < j -> a[i] <= a[idx] }
  20     if get_ofs a idx < get_ofs a j then idx <- j
  21   done;
  22   idx