1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
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
76
77
78
79
80
81
82
|
(** Euclidean division *)
module Division
use int.Int
use ref.Refint
let division (a b: int) : int
requires { 0 <= a && 0 < b }
ensures { exists r. result * b + r = a && 0 <= r < b }
=
let ref q = 0 in
let ref r = a in
while r >= b do
invariant { q * b + r = a && 0 <= r }
variant { r }
incr q;
r -= b
done;
q
end
(** Euclidean division from Hoare's seminal paper
"An Axiomatic Basis for Computer Programming"
(Communications of the ACM 12(10), 1969).
Hoare's proof of Euclidean division is performed under the nine
axioms for arithmetic given below, which are all valid for several
models of machine arithmetic (infinite arithmetic, strict
interpretation, firm boundary, modulo arithmetic).
Notes:
- Axioms A2 and A4 (commutativity and associativity of multiplication)
are actually not needed for the proof.
- Hoare is not proving termination.
*)
module Hoare
type integer
val constant zero: integer
val constant one: integer
val function (+) (x y: integer) : integer
val function (-) (x y: integer) : integer
val function (*) (x y: integer) : integer
val predicate (<=) (x y: integer)
axiom A1: forall x y. x + y = y + x
axiom A2: forall x y. x * y = y * x
axiom A3: forall x y z. (x + y) + z = x + (y + z)
axiom A4: forall x y z. (x * y) * z = x * (y * z)
axiom A5: forall x y z. x * (y + z) = x * y + x * z
axiom A6: forall x y. y <= x -> (x - y) + y = x
axiom A7: forall x. x + zero = x
axiom A8: forall x. x * zero = zero
axiom A9: forall x. x * one = x
let division (x y: integer) : (q: integer, r: integer)
ensures { not (y <= r) }
ensures { x = r + y * q }
diverges
=
let ref r = x in
let ref q = zero in
while y <= r do
invariant { x = r + y * q }
r <- r - y;
q <- one + q
done;
q, r
end
module HoareSound
use int.Int
clone Hoare with type integer = int, val zero = zero,
val one = one, val (+) = (+), val (-) = (-), val (*) = (*),
val (<=) = (<=), lemma .
end
|
