examples/mccarthy_vc_sp.mlw

   1
   2 (* McCarthy's ``91'' function. *)
   3
   4 module McCarthy91
   5
   6   use int.Int
   7
   8   function spec (x: int) : int = if x <= 100 then 91 else x-10
   9
  10   (* traditional recursive implementation *)
  11
  12   let rec f91 (n:int) : int variant { 101-n }
  13     ensures { result = spec n }
  14   = [@vc:sp]
  15     if n <= 100 then
  16       f91 (f91 (n + 11))
  17     else
  18       n - 10
  19
  20   (* non-recursive implementation using a while loop *)
  21
  22   use ref.Ref
  23   use int.Iter
  24
  25   let f91_nonrec (n0: int) ensures { result = spec n0 }
  26   = [@vc:sp]
  27     let e = ref 1 in
  28     let n = ref n0 in
  29     while !e > 0 do
  30       invariant { !e >= 0 /\ iter spec !e !n = spec n0 }
  31       variant   { 101 - !n + 10 * !e, !e }
  32       if !n > 100 then begin
  33         n := !n - 10;
  34         e := !e - 1
  35       end else begin
  36         n := !n + 11;
  37         e := !e + 1
  38       end
  39     done;
  40     !n
  41
  42   (* Use a 'morally' irrelevant control flow from a recursive function
  43      to ease proof (the recursive structure does not contribute to the
  44      program execution). This is a technique for proving derecursified
  45      programs. See verifythis_2016_tree_traversal for a more
  46      complex example. *)
  47
  48   exception Stop
  49
  50   let f91_pseudorec (n0:int) : int
  51     ensures { result = spec n0 }
  52   = [@vc:sp]
  53     let e = ref 1 in
  54     let n = ref n0 in
  55     let bloc () : unit
  56       requires { !e >= 0 }
  57       ensures { !(old e) > 0 }
  58       ensures { if !(old n) > 100 then !n = !(old n) - 10 /\ !e = !(old e) - 1
  59         else !n = !(old n) + 11 /\ !e = !(old e) + 1 }
  60       raises { Stop -> !e = !(old e) = 0 /\ !n = !(old n) }
  61     = if not (!e > 0) then raise Stop;
  62       if !n > 100 then begin
  63         n := !n - 10;
  64         e := !e - 1
  65       end else begin
  66         n := !n + 11;
  67         e := !e + 1
  68       end
  69     in
  70     let rec aux () : unit
  71       requires { !e > 0 }
  72       variant { 101 - !n }
  73       ensures { !e = !(old e) - 1 /\ !n = spec !(old n) }
  74       raises { Stop -> false }
  75     = let u = !n in bloc (); if u <= 100 then (aux (); aux ()) in
  76     try aux (); bloc (); absurd
  77     with Stop -> !n end
  78
  79 end
  80
  81 module McCarthy91Mach
  82
  83   use int.Int
  84   use mach.int.Int63
  85
  86   function spec (x: int) : int = if x <= 100 then 91 else x-10
  87
  88   let rec f91 (n: int63) : int63
  89     variant { 101 - n }
  90     ensures { result = spec n }
  91   = [@vc:sp]
  92     if n <= 100 then
  93       f91 (f91 (n + 11))
  94     else
  95       n - 10
  96
  97   use mach.peano.Peano
  98   use mach.int.Refint63
  99   use int.Iter
 100
 101   let f91_nonrec (n0: int63) : int63
 102     ensures { result = spec n0 }
 103   = [@vc:sp]
 104     let e = ref one in
 105     let n = ref n0 in
 106     while gt !e zero do
 107       invariant { !e >= 0 /\ iter spec !e !n = spec n0 }
 108       variant   { 101 - !n + 10 * !e, !e:int }
 109       if !n > 100 then begin
 110         n := !n - 10;
 111         e := pred !e
 112       end else begin
 113         n := !n + 11;
 114         e := succ !e
 115       end
 116     done;
 117     !n
 118
 119   exception Stop
 120
 121   let f91_pseudorec (n0: int63) : int63
 122     ensures { result = spec n0 }
 123   = [@vc:sp]
 124     let e = ref one in
 125     let n = ref n0 in
 126     let bloc () : unit
 127       requires { !e >= 0 }
 128       ensures { !(old e) > 0 }
 129       ensures { if !(old n) > 100 then !n = !(old n) - 10 /\ !e = !(old e) - 1
 130         else !n = !(old n) + 11 /\ !e = !(old e) + 1 }
 131       raises { Stop -> !e = !(old e) = 0 /\ !n = !(old n) }
 132     = if not (gt !e zero) then raise Stop;
 133       if !n > 100 then begin
 134         n := !n - 10;
 135         e := pred !e
 136       end else begin
 137         n := !n + 11;
 138         e := succ !e
 139       end
 140     in
 141     let rec aux () : unit
 142       requires { !e > 0 }
 143       variant { 101 - !n }
 144       ensures { !e = !(old e) - 1 /\ !n = spec !(old n) }
 145       raises { Stop -> false }
 146     = let u = !n in bloc (); if u <= 100 then (aux (); aux ()) in
 147     try aux (); bloc (); absurd
 148     with Stop -> !n end
 149
 150 end