examples/swap.mlw

   1
   2 (** Swapping two integers in-place *)
   3
   4 module Swap
   5
   6   use int.Int
   7   use ref.Ref
   8
   9   let swap (ref a b: int) : unit
  10     writes  { a, b }
  11     ensures { a = old b /\ b = old a }
  12   =
  13     a <- a + b;
  14     b <- a - b;
  15     a <- a - b
  16
  17 end
  18
  19 (** It also works fine with machine integers, even with overflows *)
  20
  21 module SwapInt32
  22
  23   use int.Int
  24   use ref.Ref
  25
  26   (** a simple model of 32-bit integers with addition, subtraction,
  27       and possible overflows *)
  28
  29   type int32 = < range -0x8000_0000 0x7fff_ffff >
  30
  31   meta coercion function int32'int
  32
  33   constant width : int = int32'maxInt - int32'minInt + 1
  34
  35   val (+) (a: int32) (b: int32) : int32
  36     ensures { result =
  37          if a + b < int32'minInt then a + b + width
  38     else if a + b > int32'maxInt then a + b - width
  39     else    a + b }
  40
  41   val (-) (a: int32) (b: int32) : int32
  42     ensures { result =
  43          if a - b < int32'minInt then a - b + width
  44     else if a - b > int32'maxInt then a - b - width
  45     else    a - b }
  46
  47   predicate in_bounds (n: int32) = int32'minInt <= n <= int32'maxInt
  48
  49   (** purely applicative version first *)
  50
  51   let swap (a b: int32) : (x: int32, y: int32)
  52     requires { in_bounds a /\ in_bounds b }
  53     ensures  { int32'int x = b /\ int32'int y = a }
  54   =
  55     let a = a + b in
  56     let b = a - b in
  57     let a = a - b in
  58     a, b
  59
  60   (** then rephrased with mutable variables *)
  61
  62   let swap_ref (ref a b: int32) : unit
  63     requires { in_bounds a /\ in_bounds b }
  64     writes   { a, b }
  65     ensures  { int32'int a = old b /\ int32'int b = old a }
  66   =
  67     a <- a + b;
  68     b <- a - b;
  69     a <- a - b
  70
  71 end
  72
  73 (** with bitwise XOR this time *)
  74
  75 module SwapInt32xor
  76
  77   use bv.BV32
  78   use ref.Ref
  79
  80   let swap (ref a b: t) : unit
  81     writes   { a, b }
  82     ensures  { a = old b /\ b = old a }
  83   = a <- bw_xor a b;
  84     b <- bw_xor a b;
  85     a <- bw_xor a b
  86
  87 end
  88