mccarthy.mlw 7.57 KB
Newer Older
1

2
(** {1 McCarthy's "91" function}
3 4 5 6 7

authors: Jean-Christophe Filliâtre, Martin Clochard, Claude Marché
witness: Andrei Paskevich

*)
8

9
module McCarthy91
10

11
  use int.Int
12

13 14
  (** {2 Specification} *)

15 16
  function spec (x: int) : int = if x <= 100 then 91 else x-10

17
  (** {2 traditional recursive implementation} *)
18

19 20
  let rec f91 (n: int) : int
    ensures { result = spec n } variant { 101 - n }
21
  = if n <= 100 then
22 23 24
      f91 (f91 (n + 11))
    else
      n - 10
25

26 27 28 29 30 31 32 33 34 35 36
  (** {2 manually-optimized tail call} *)

  let rec f91_tco (n0: int) : int
    ensures { result = spec n0 } variant { 101 - n0 }
  = let ref n = n0 in
    while n <= 100 do
      invariant { n = n0 > 100 \/ n0 <= n <= 101 } variant { 101 - n }
      n <- f91_tco (n + 11)
    done;
    n - 10

37
  (** {2 non-recursive implementation using a while loop} *)
38

39 40
  use ref.Ref
  use int.Iter
41

42 43 44 45 46 47 48 49 50 51
  let f91_nonrec (n0: int): int
    ensures { result = spec n0 }
  = let ref e = 1 in
    let ref n = n0 in
    while e > 0 do
      invariant { e >= 0 /\ iter spec e n = spec n0 }
      variant   { 101 - n + 10 * e, e }
      if n > 100 then begin
        n <- n - 10;
        e <- e - 1
52
      end else begin
53 54
        n <- n + 11;
        e <- e + 1
55 56
      end
    done;
57
    n
58

59 60 61
  (** {2 irrelevance of control flow}

     We use a 'morally' irrelevant control flow from a recursive function
62 63
     to ease proof (the recursive structure does not contribute to the
     program execution). This is a technique for proving derecursified
64
     programs. See [verifythis_2016_tree_traversal] for a more
65 66 67 68
     complex example. *)

  exception Stop

69
  let f91_pseudorec (n0: int) : int
70
    ensures { result = spec n0 }
71 72
  = let ref e = 1 in
    let ref n = n0 in
73
    let bloc () : unit
74 75 76 77 78 79 80 81 82
      requires { e >= 0 }
      ensures { (old e) > 0 }
      ensures { if (old n) > 100 then n = (old n) - 10 /\ e = (old e) - 1
        else n = (old n) + 11 /\ e = (old e) + 1 }
      raises { Stop -> e = (old e) = 0 /\ n = (old n) }
    = if not (e > 0) then raise Stop;
      if n > 100 then begin
        n <- n - 10;
        e <- e - 1
83
      end else begin
84 85
        n <- n + 11;
        e <- e + 1
86 87 88
      end
    in
    let rec aux () : unit
89 90 91
      requires { e > 0 }
      variant { 101 - n }
      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 99

end

100
module McCarthyWithGhostMonitor
101 102


103 104
  use int.Int
  use ref.Ref
105 106 107

  function spec (x: int) : int = if x <= 100 then 91 else x-10

108 109
  (** {2 Variant using a general 'ghost coroutine' approach}

110
    Assume we want to prove the imperative code:
111
{h <pre>
112 113 114 115 116
e <- 1; r <- n;
loop
  if r > 100 { r <- r - 10; e <- e - 1; if e = 0 break }
        else { r <- r + 11; e <- e + 1 }
end-loop
117 118 119
</pre>}
we annotate the various program points:
{h <pre>
120 121 122 123 124 125
{ 0 } e <- 1;
{ 1 } r <- n;
      loop
{ 2 } if r > 100 then { 3 } r <- r - 10; { 4 } e <- e - 1; { 5 } if e=0 then break;
                 else { 6 } r <- r + 11; { 7 } e <- e + 1;
end-loop
126 127 128 129 130 131 132
{ 8 }
</pre>}

we define the small-step semantics of this code by the following [step] function

*)

133

134 135 136 137
  val ref pc : int
  val ref n : int
  val ref e : int
  val ref r : int
138 139

  val step () : unit
140
    requires { 0 <= pc < 8 }
141
    writes   { pc, e, r }
142 143 144 145 146 147 148 149 150 151
    ensures { old pc = 0 -> pc = 1 /\ e = 1 /\ r = old r }
    ensures { old pc = 1 -> pc = 2 /\ e = old e /\ r = n }
    ensures { old pc = 2 /\ old r > 100 -> pc = 3 /\ e = old e /\ r = old r }
    ensures { old pc = 2 /\ old r <= 100 -> pc = 6 /\ e = old e /\ r = old r }
    ensures { old pc = 3 -> pc = 4 /\ e = old e /\ r = old r - 10 }
    ensures { old pc = 4 -> pc = 5 /\ e = old e - 1 /\ r = old r }
    ensures { old pc = 5 /\ old e = 0 -> pc = 8 /\ e = old e /\ r = old r }
    ensures { old pc = 5 /\ old e <> 0 -> pc = 2 /\ e = old e /\ r = old r }
    ensures { old pc = 6 -> pc = 7 /\ e = old e /\ r = old r + 11 }
    ensures { old pc = 7 -> pc = 2 /\ e = old e + 1 /\ r = old r }
152

153
  let rec monitor () : unit
154 155 156
    requires { pc = 2 /\ e > 0 }
    variant  { 101 - r }
    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 160 161 162 163 164
       step (); (* assignment r <- r - 10 *)
       step (); (* assignment e <- e - 1  *)
       end
    else begin
       step (); (* assignment r <- r + 11 *)
       step (); (* assignment e <- e + 1 *)
165
       monitor ();
166
       step (); (* 'if e=0' must be false *)
167
       monitor ()
168
       end
169

170
  let mccarthy ()
171 172
    requires { pc = 0 /\ n >= 0 }
    ensures { pc = 8 /\ r = spec n }
173 174
  = step (); (* assignment e <- 1 *)
    step (); (* assignment r <- n *)
175
    monitor (); (* loop *)
176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197
    step() (* loop exit *)

(** {2 a variant with not-so-small steps}

we annotate the important program points:
{h <pre>
{ 0 } e <- 1;
      r <- n;
      loop
{ 1 }   if r > 100 { r <- r - 10; e <- e - 1; { 2 } if e = 0 break; }
              else { r <- r + 11; e <- e + 1; }
      end-loop
end-while
{ 3 }
return r
</pre>}

we define the not-so-small-step semantics of this code by the following [next] function

*)

  val next () : unit
198
    requires { 0 <= pc < 3 }
199
    writes   { pc, e, r }
200 201 202 203 204 205 206
    ensures { old pc = 0 -> pc = 1 /\ e = 1 /\ r = n }
    ensures { old pc = 1 /\ old r > 100 ->
              pc = 2 /\ r = old r - 10 /\ e = old e - 1 }
    ensures { old pc = 1 /\ old r <= 100 ->
              pc = 1 /\ r = old r + 11 /\ e = old e + 1 }
    ensures { old pc = 2 /\ old e = 0 -> pc = 3 /\ r = old r /\ e = old e }
    ensures { old pc = 2 /\ old e <> 0 -> pc = 1 /\ r = old r /\ e = old e }
207 208 209

  (* [aux2] performs as may loop iterations as needed so as to reach program point 2
     from program point 1 *)
210
  let rec monitor2 () : unit
211 212 213
    requires { pc = 1 /\ e > 0 }
    variant  { 101 - r }
    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 220
    requires { pc = 0 /\ n >= 0 }
    ensures { pc = 3 /\ r = spec n }
221
  = next (); (* assignments e <- 1; r <- n *)
222
    monitor2 (); (* loop *)
223
    next ()
224

225
end
226 227 228

module McCarthy91Mach

229 230
  use int.Int
  use mach.int.Int63
231 232 233 234 235 236

  function spec (x: int) : int = if x <= 100 then 91 else x-10

  let rec f91 (n: int63) : int63
    variant { 101 - n }
    ensures { result = spec n }
237 238
  = if n <= 100 then
      f91 (f91 (n + 11))
239
    else
240
      n - 10
241

242 243 244
  use mach.peano.Peano
  use mach.int.Refint63
  use int.Iter
245 246 247

  let f91_nonrec (n0: int63) : int63
    ensures { result = spec n0 }
248 249 250 251 252 253 254 255
  = let ref e = one in
    let ref n = n0 in
    while gt e zero do
      invariant { e >= 0 /\ iter spec e n = spec n0 }
      variant   { 101 - n + 10 * e, e:int }
      if n > 100 then begin
        n <- n - 10;
        e <- pred e
256
      end else begin
257 258
        n <- n + 11;
        e <- succ e
259 260
      end
    done;
261
    n
262 263 264 265 266

  exception Stop

  let f91_pseudorec (n0: int63) : int63
    ensures { result = spec n0 }
267 268
  = let ref e = one in
    let ref n = n0 in
269
    let bloc () : unit
270 271 272 273 274 275 276 277 278
      requires { e >= 0 }
      ensures { (old e) > 0 }
      ensures { if (old n) > 100 then n = (old n) - 10 /\ e = (old e) - 1
        else n = (old n) + 11 /\ e = (old e) + 1 }
      raises { Stop -> e = (old e) = 0 /\ n = (old n) }
    = if not (gt e zero) then raise Stop;
      if n > 100 then begin
        n := n - 10;
        e := pred e
279
      end else begin
280 281
        n := n + 11;
        e := succ e
282 283 284
      end
    in
    let rec aux () : unit
285 286 287
      requires { e > 0 }
      variant { 101 - n }
      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