bench/infer/twoway.mlw

   1 (* Two Way Sort
   2
   3    The following program sorts an array of Boolean values, with False<True.
   4
   5    Questions:
   6
   7    1. Prove safety i.e. the absence of array access out of bounds.
   8
   9    2. Prove termination.
  10
  11    3. Prove that array a is sorted after execution of function two_way_sort
  12       (using the predicate sorted that is provided).
  13
  14    4. Show that after execution the array contents is a permutation of its
  15       initial contents. Use the library predicate "permut_all" to do so
  16       (the corresponding module ArrayPermut is already imported).
  17
  18       Within a postcondition, you can refer to the contents of array a
  19       at the beginning of the function with notation (old a).
  20       Within a loop invariant, you can refer to it with notation (at a 'Init).
  21
  22 *)
  23
  24 module TwoWaySort
  25
  26   use int.Int
  27   use bool.Bool
  28   use ref.Refint
  29   use array.Array
  30   use array.ArraySwap
  31   use array.ArrayPermut
  32
  33   predicate (<<) (x y: bool) = x = False \/ y = True
  34
  35   predicate sorted (a: array bool) =
  36     forall i1 i2: int. 0 <= i1 <= i2 < a.length -> a[i1] << a[i2]
  37
  38   let two_way_sort [@bddinfer] [@infer](a: array bool) : unit
  39   requires { length a >= 0 }
  40     writes { a }
  41     ensures { sorted a }
  42   =
  43     let i = ref 0 in
  44     let j = ref (length a - 1) in
  45     while !i < !j do
  46         variant { !j - !i }
  47       invariant { forall k:int. 0 <= k < !i -> not a[k] }
  48       invariant { forall k:int. !j < k < length a -> a[k] }
  49       if not a[!i] then
  50          i := !i + 1
  51       else if a[!j] then
  52         j := !j - 1
  53       else begin
  54         swap a !i !j;
  55         i := !i + 1;
  56         j := !j - 1
  57       end
  58     done
  59
  60   let two_way_sort3 [@bddinfer] [@infer:box](a: array bool) : unit
  61   requires { length a >= 0 }
  62     writes { a }
  63     ensures { sorted a }
  64   =
  65     let i = ref 0 in
  66     let j = ref (length a - 1) in
  67     while !i < !j do
  68         variant { !j - !i }
  69       invariant { forall k:int. 0 <= k < !i -> not a[k] }
  70       invariant { forall k:int. !j < k < length a -> a[k] }
  71       if not a[!i] then
  72          i := !i + 1
  73       else if a[!j] then
  74         j := !j - 1
  75       else begin
  76         swap a !i !j;
  77         i := !i + 1;
  78         j := !j - 1
  79       end
  80     done
  81
  82 end