mccarthy.mlw 3.61 KB
Newer Older
1

2
3
(* McCarthy's ``91'' function. *)

4
module McCarthy91
5

6
7
  use import int.Int

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

10
  (* traditional recursive implementation *)
11

12
  let rec f91 (n:int) : int variant { 101-n }
13
    ensures { result = spec n }
14
  = if n <= 100 then
15
16
17
      f91 (f91 (n + 11))
    else
      n - 10
18

19
  (* non-recursive implementation using a while loop *)
20

21
  use import ref.Ref
22
  use import int.Iter
23

24
  let f91_nonrec (n0: int) ensures { result = spec n0 }
25
  = let e = ref 1 in
26
27
    let n = ref n0 in
    while !e > 0 do
28
      invariant { !e >= 0 /\ iter spec !e !n = spec n0 }
29
      variant   { 101 - !n + 10 * !e, !e }
30
31
32
      if !n > 100 then begin
        n := !n - 10;
        e := !e - 1
33
      end else begin
34
35
        n := !n + 11;
        e := !e + 1
36
37
      end
    done;
38
    !n
39

40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
  (* Use a 'morally' irrelevant control flow from a recursive function
     to ease proof (the recursive structure does not contribute to the
     program execution). This is a technique for proving derecursified
     programs. See verifythis_2016_tree_traversal for a more
     complex example. *)

  exception Stop

  let f91_pseudorec (n0:int) : int
    ensures { result = spec n0 }
  = let e = ref 1 in
    let n = ref n0 in
    let bloc () : unit
      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
      end else begin
        n := !n + 11;
        e := !e + 1
      end
    in
    let rec aux () : unit
      requires { !e > 0 }
      variant { 101 - !n }
      ensures { !e = !(old e) - 1 /\ !n = spec !(old n) }
      raises { Stop -> false }
    = let u = !n in bloc (); if u <= 100 then (aux (); aux ()) in
    try aux (); bloc (); absurd
    with Stop -> !n end

76
end
77
78
79
80
81
82
83
84
85
86
87

module McCarthy91Mach

  use import int.Int
  use import mach.int.Int63

  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 }
88
89
  = if n <= 100 then
      f91 (f91 (n + 11))
90
    else
91
      n - 10
92
93
94
95
96
97
98
99
100
101
102
103

  use import mach.peano.Peano
  use import mach.int.Refint63
  use import int.Iter

  let f91_nonrec (n0: int63) : int63
    ensures { result = spec n0 }
  = let e = ref one in
    let n = ref n0 in
    while gt !e zero do
      invariant { !e >= 0 /\ iter spec !e !n = spec n0 }
      variant   { 101 - !n + 10 * !e, !e:int }
104
105
      if !n > 100 then begin
        n := !n - 10;
106
107
        e := pred !e
      end else begin
108
        n := !n + 11;
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
        e := succ !e
      end
    done;
    !n

  exception Stop

  let f91_pseudorec (n0: int63) : int63
    ensures { result = spec n0 }
  = let e = ref one in
    let n = ref n0 in
    let bloc () : unit
      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;
127
128
      if !n > 100 then begin
        n := !n - 10;
129
130
        e := pred !e
      end else begin
131
        n := !n + 11;
132
133
134
135
136
137
138
139
        e := succ !e
      end
    in
    let rec aux () : unit
      requires { !e > 0 }
      variant { 101 - !n }
      ensures { !e = !(old e) - 1 /\ !n = spec !(old n) }
      raises { Stop -> false }
140
    = let u = !n in bloc (); if u <= 100 then (aux (); aux ()) in
141
142
143
    try aux (); bloc (); absurd
    with Stop -> !n end

144
end