examples/mccarthy.mlw

   1
   2 (** {1 McCarthy's "91" function}
   3
   4 authors: Jean-Christophe Filliâtre, Martin Clochard, Claude Marché
   5 witness: Andrei Paskevich
   6
   7 *)
   8
   9 module McCarthy91
  10
  11   use int.Int
  12
  13   (** {2 Specification} *)
  14
  15   function spec (x: int) : int = if x <= 100 then 91 else x-10
  16
  17   (** {2 traditional recursive implementation} *)
  18
  19   let rec f91 (n: int) : int
  20     ensures { result = spec n } variant { 101 - n }
  21   = if n <= 100 then
  22       f91 (f91 (n + 11))
  23     else
  24       n - 10
  25
  26   (** {2 manually-optimized tail call} *)
  27
  28   let rec f91_tco (n0: int) : int
  29     ensures { result = spec n0 } variant { 101 - n0 }
  30   = let ref n = n0 in
  31     while n <= 100 do
  32       invariant { n = n0 > 100 \/ n0 <= n <= 101 } variant { 101 - n }
  33       n <- f91_tco (n + 11)
  34     done;
  35     n - 10
  36
  37   (** {2 non-recursive implementation using a while loop} *)
  38
  39   use ref.Ref
  40   use int.Iter
  41
  42   let f91_nonrec (n0: int): int
  43     ensures { result = spec n0 }
  44   = let ref e = 1 in
  45     let ref n = n0 in
  46     while e > 0 do
  47       invariant { e >= 0 /\ iter spec e n = spec n0 }
  48       variant   { 101 - n + 10 * e, e }
  49       if n > 100 then begin
  50         n <- n - 10;
  51         e <- e - 1
  52       end else begin
  53         n <- n + 11;
  54         e <- e + 1
  55       end
  56     done;
  57     n
  58
  59   (** {2 irrelevance of control flow}
  60
  61      We use a 'morally' irrelevant control flow from a recursive function
  62      to ease proof (the recursive structure does not contribute to the
  63      program execution). This is a technique for proving derecursified
  64      programs. See [verifythis_2016_tree_traversal] for a more
  65      complex example. *)
  66
  67   exception Stop
  68
  69   let f91_pseudorec (n0: int) : int
  70     ensures { result = spec n0 }
  71   = let ref e = 1 in
  72     let ref n = n0 in
  73     let bloc () : unit
  74       requires { e >= 0 }
  75       ensures { (old e) > 0 }
  76       ensures { if (old n) > 100 then n = (old n) - 10 /\ e = (old e) - 1
  77         else n = (old n) + 11 /\ e = (old e) + 1 }
  78       raises { Stop -> e = (old e) = 0 /\ n = (old n) }
  79     = if not (e > 0) then raise Stop;
  80       if n > 100 then begin
  81         n <- n - 10;
  82         e <- e - 1
  83       end else begin
  84         n <- n + 11;
  85         e <- e + 1
  86       end
  87     in
  88     let rec aux () : unit
  89       requires { e > 0 }
  90       variant { 101 - n }
  91       ensures { e = (old e) - 1 /\ n = spec (old n) }
  92       raises { Stop -> false }
  93     = let u = n in bloc (); if u <= 100 then (aux (); aux ()) in
  94     try aux (); bloc (); absurd
  95     with Stop -> n end
  96
  97
  98 end
  99
 100 module McCarthyWithGhostMonitor
 101
 102
 103   use int.Int
 104   use ref.Ref
 105
 106   function spec (x: int) : int = if x <= 100 then 91 else x-10
 107
 108   (** {2 Variant using a general 'ghost coroutine' approach}
 109
 110     Assume we want to prove the imperative code:
 111 {h <pre>
 112 e <- 1; r <- n;
 113 loop
 114   if r > 100 { r <- r - 10; e <- e - 1; if e = 0 break }
 115         else { r <- r + 11; e <- e + 1 }
 116 end-loop
 117 </pre>}
 118 we annotate the various program points:
 119 {h <pre>
 120 { 0 } e <- 1;
 121 { 1 } r <- n;
 122       loop
 123 { 2 } if r > 100 then { 3 } r <- r - 10; { 4 } e <- e - 1; { 5 } if e=0 then break;
 124                  else { 6 } r <- r + 11; { 7 } e <- e + 1;
 125 end-loop
 126 { 8 }
 127 </pre>}
 128
 129 we define the small-step semantics of this code by the following [step] function
 130
 131 *)
 132
 133
 134   val ref pc : int
 135   val ref n : int
 136   val ref e : int
 137   val ref r : int
 138
 139   val step () : unit
 140     requires { 0 <= pc < 8 }
 141     writes   { pc, e, r }
 142     ensures { old pc = 0 -> pc = 1 /\ e = 1 /\ r = old r }
 143     ensures { old pc = 1 -> pc = 2 /\ e = old e /\ r = n }
 144     ensures { old pc = 2 /\ old r > 100 -> pc = 3 /\ e = old e /\ r = old r }
 145     ensures { old pc = 2 /\ old r <= 100 -> pc = 6 /\ e = old e /\ r = old r }
 146     ensures { old pc = 3 -> pc = 4 /\ e = old e /\ r = old r - 10 }
 147     ensures { old pc = 4 -> pc = 5 /\ e = old e - 1 /\ r = old r }
 148     ensures { old pc = 5 /\ old e = 0 -> pc = 8 /\ e = old e /\ r = old r }
 149     ensures { old pc = 5 /\ old e <> 0 -> pc = 2 /\ e = old e /\ r = old r }
 150     ensures { old pc = 6 -> pc = 7 /\ e = old e /\ r = old r + 11 }
 151     ensures { old pc = 7 -> pc = 2 /\ e = old e + 1 /\ r = old r }
 152
 153   let rec monitor () : unit
 154     requires { pc = 2 /\ e > 0 }
 155     variant  { 101 - r }
 156     ensures  { pc = 5 /\ r = spec(old r) /\ e = old e - 1 }
 157   = step (); (* execution of 'if r > 100' *)
 158     if pc = 3 then begin
 159        step (); (* assignment r <- r - 10 *)
 160        step (); (* assignment e <- e - 1  *)
 161        end
 162     else begin
 163        step (); (* assignment r <- r + 11 *)
 164        step (); (* assignment e <- e + 1 *)
 165        monitor ();
 166        step (); (* 'if e=0' must be false *)
 167        monitor ()
 168        end
 169
 170   let mccarthy ()
 171     requires { pc = 0 /\ n >= 0 }
 172     ensures { pc = 8 /\ r = spec n }
 173   = step (); (* assignment e <- 1 *)
 174     step (); (* assignment r <- n *)
 175     monitor (); (* loop *)
 176     step() (* loop exit *)
 177
 178 (** {2 a variant with not-so-small steps}
 179
 180 we annotate the important program points:
 181 {h <pre>
 182 { 0 } e <- 1;
 183       r <- n;
 184       loop
 185 { 1 }   if r > 100 { r <- r - 10; e <- e - 1; { 2 } if e = 0 break; }
 186               else { r <- r + 11; e <- e + 1; }
 187       end-loop
 188 end-while
 189 { 3 }
 190 return r
 191 </pre>}
 192
 193 we define the not-so-small-step semantics of this code by the following [next] function
 194
 195 *)
 196
 197   val next () : unit
 198     requires { 0 <= pc < 3 }
 199     writes   { pc, e, r }
 200     ensures { old pc = 0 -> pc = 1 /\ e = 1 /\ r = n }
 201     ensures { old pc = 1 /\ old r > 100 ->
 202               pc = 2 /\ r = old r - 10 /\ e = old e - 1 }
 203     ensures { old pc = 1 /\ old r <= 100 ->
 204               pc = 1 /\ r = old r + 11 /\ e = old e + 1 }
 205     ensures { old pc = 2 /\ old e = 0 -> pc = 3 /\ r = old r /\ e = old e }
 206     ensures { old pc = 2 /\ old e <> 0 -> pc = 1 /\ r = old r /\ e = old e }
 207
 208   (* [aux2] performs as may loop iterations as needed so as to reach program point 2
 209      from program point 1 *)
 210   let rec monitor2 () : unit
 211     requires { pc = 1 /\ e > 0 }
 212     variant  { 101 - r }
 213     ensures  { pc = 2 /\ r = spec(old r) /\ e = old e - 1 }
 214   = next ();
 215     if pc <> 2 then begin monitor2 (); next (); monitor2 () end
 216
 217
 218   let mccarthy2 ()
 219     requires { pc = 0 /\ n >= 0 }
 220     ensures { pc = 3 /\ r = spec n }
 221   = next (); (* assignments e <- 1; r <- n *)
 222     monitor2 (); (* loop *)
 223     next ()
 224
 225 end
 226
 227 module McCarthy91Mach
 228
 229   use int.Int
 230   use mach.int.Int63
 231
 232   function spec (x: int) : int = if x <= 100 then 91 else x-10
 233
 234   let rec f91 (n: int63) : int63
 235     variant { 101 - n }
 236     ensures { result = spec n }
 237   = if n <= 100 then
 238       f91 (f91 (n + 11))
 239     else
 240       n - 10
 241
 242   use mach.peano.Peano
 243   use mach.int.Refint63
 244   use int.Iter
 245
 246   let f91_nonrec (n0: int63) : int63
 247     ensures { result = spec n0 }
 248   = let ref e = one in
 249     let ref n = n0 in
 250     while gt e zero do
 251       invariant { e >= 0 /\ iter spec e n = spec n0 }
 252       variant   { 101 - n + 10 * e, e:int }
 253       if n > 100 then begin
 254         n <- n - 10;
 255         e <- pred e
 256       end else begin
 257         n <- n + 11;
 258         e <- succ e
 259       end
 260     done;
 261     n
 262
 263   exception Stop
 264
 265   let f91_pseudorec (n0: int63) : int63
 266     ensures { result = spec n0 }
 267   = let ref e = one in
 268     let ref n = n0 in
 269     let bloc () : unit
 270       requires { e >= 0 }
 271       ensures { (old e) > 0 }
 272       ensures { if (old n) > 100 then n = (old n) - 10 /\ e = (old e) - 1
 273         else n = (old n) + 11 /\ e = (old e) + 1 }
 274       raises { Stop -> e = (old e) = 0 /\ n = (old n) }
 275     = if not (gt e zero) then raise Stop;
 276       if n > 100 then begin
 277         n := n - 10;
 278         e := pred e
 279       end else begin
 280         n := n + 11;
 281         e := succ e
 282       end
 283     in
 284     let rec aux () : unit
 285       requires { e > 0 }
 286       variant { 101 - n }
 287       ensures { e = (old e) - 1 /\ n = spec (old n) }
 288       raises { Stop -> false }
 289     = let u = n in bloc (); if u <= 100 then (aux (); aux ()) in
 290     try aux (); bloc (); absurd
 291     with Stop -> n end
 292
 293 end