swap.mlw 216 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15

module Swap

  use import int.Int
  use import ref.Ref

  let swap (a b: ref int) : unit
    writes  { a, b }
    ensures { !a = old !b /\ !b = old !a }
  =
    a := !a + !b;
    b := !a - !b;
    a := !a - !b

end