jlamp_array.mlw 663 Bytes
Newer Older
1 2
module Array

3 4
  use int.Int
  use array.Array
5 6 7 8 9 10

  type t

  function to_int  t : int
  meta "model_projection" function to_int

11
  val function two : t
12 13
  axiom two_def : to_int two = 2

14
  val function three : t
15 16 17
  axiom three_def : to_int three = 3


18
  let f (a : array t) : unit
19 20
    requires { a[42] = three }
    writes { a }
21
    ensures { a[42] = three }
22 23
  = a[42] <- two

24
  let g (a : array t) : unit
25 26
    requires { a.length >= 43 /\ a[17] = three }
    writes { a }
27
    ensures { a[42] = three }
28 29
  = a[42] <- two

30
  let h (a : array t) : unit
31 32
    requires { a.length >= 43 /\ a[17] = three }
    writes { a }
33
    ensures { a[42] = three }
34 35 36
  = a[17] <- two

end