forked from tlaplus/Examples
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathFindHighest.tla
170 lines (148 loc) · 5.76 KB
/
FindHighest.tla
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
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
---------------------------- MODULE FindHighest -----------------------------
(***************************************************************************)
(* Defines a very simple algorithm that finds the largest value in a *)
(* sequence of Natural numbers. This was created as an exercise in finding *)
(* & proving type invariants, inductive invariants, and correctness. *)
(***************************************************************************)
EXTENDS Sequences, Naturals, Integers, TLAPS
(****************************************************************************
--algorithm Highest {
variables
f \in Seq(Nat);
h = -1;
i = 1;
define {
max(a, b) == IF a >= b THEN a ELSE b
} {
lb: while (i <= Len(f)) {
h := max(h, f[i]);
i := i + 1;
}
}
}
****************************************************************************)
\* BEGIN TRANSLATION (chksum(pcal) = "31f24270" /\ chksum(tla) = "819802c6")
VARIABLES f, h, i, pc
(* define statement *)
max(a, b) == IF a >= b THEN a ELSE b
vars == << f, h, i, pc >>
Init == (* Global variables *)
/\ f \in Seq(Nat)
/\ h = -1
/\ i = 1
/\ pc = "lb"
lb == /\ pc = "lb"
/\ IF i <= Len(f)
THEN /\ h' = max(h, f[i])
/\ i' = i + 1
/\ pc' = "lb"
ELSE /\ pc' = "Done"
/\ UNCHANGED << h, i >>
/\ f' = f
(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == pc = "Done" /\ UNCHANGED vars
Next == lb
\/ Terminating
Spec == Init /\ [][Next]_vars
Termination == <>(pc = "Done")
\* END TRANSLATION
\* The type invariant; the proof system likes knowing variables are in Nat.
\* It's a good idea to check these invariants with the model checker before
\* trying to prove them. To quote Leslie Lamport, it's very difficult to
\* prove something that isn't true!
TypeOK ==
/\ f \in Seq(Nat)
/\ i \in 1..(Len(f) + 1)
/\ i \in Nat
/\ h \in Nat \cup {-1}
\* It's useful to prove the type invariant first, so it can be used as an
\* assumption in further proofs to restrict variable values.
THEOREM TypeInvariantHolds == Spec => []TypeOK
\* To prove theorems like Spec => []Invariant, you have to:
\* 1. Prove Invariant holds in the initial state (usually trivial)
\* 2. Prove Invariant holds when variables are unchanged (usually trivial)
\* 3. Prove that assuming Invariant is true, a Next step implies Invariant'
\* The last one (inductive case) is usually quite difficult. It helps to
\* never forget you have an extremely powerful assumption: that Invariant is
\* true!
PROOF
\* The base case
<1>a. Init => TypeOK
BY DEFS Init, TypeOK
\* The stuttering case
<1>b. TypeOK /\ UNCHANGED vars => TypeOK'
BY DEFS TypeOK, vars
\* The inductive case; usually requires breaking down Next into disjuncts
<1>c. TypeOK /\ Next => TypeOK'
<2>a. TypeOK /\ lb => TypeOK'
BY DEFS TypeOK, lb, max
<2>b. TypeOK /\ Terminating => TypeOK'
BY DEFS TypeOK, Terminating, vars
<2> QED BY <2>a, <2>b DEF Next
<1> QED BY PTL, <1>a, <1>b, <1>c DEF Spec
\* The inductive invariant; writing these is an art. You want an invariant
\* that can be shown to be true in every state, and if it's true in all
\* states, it can be shown to imply algorithm correctness as a whole.
InductiveInvariant ==
\A idx \in 1..(i - 1) : f[idx] <= h
THEOREM InductiveInvariantHolds == Spec => []InductiveInvariant
PROOF
<1>a. Init => InductiveInvariant
BY DEFS Init, InductiveInvariant
<1>b. InductiveInvariant /\ UNCHANGED vars => InductiveInvariant'
BY DEFS InductiveInvariant, vars
<1>c. InductiveInvariant /\ TypeOK /\ TypeOK' /\ Next => InductiveInvariant'
<2>a. InductiveInvariant /\ Terminating => InductiveInvariant'
BY DEFS InductiveInvariant, Terminating, vars
<2>b. InductiveInvariant /\ TypeOK /\ lb => InductiveInvariant'
BY DEFS InductiveInvariant, TypeOK, lb, max
<2> QED BY <2>a, <2>b DEF Next
\* We need to note we made use of the type invariant theorem here
<1> QED BY PTL, <1>a, <1>b, <1>c, TypeInvariantHolds DEF Spec
\* A small sub-theorem that relates our inductive invariant to correctness
DoneIndexValue == pc = "Done" => i = Len(f) + 1
THEOREM DoneIndexValueThm == Spec => []DoneIndexValue
PROOF
<1>a. Init => DoneIndexValue
BY DEF Init, DoneIndexValue
<1>b. DoneIndexValue /\ UNCHANGED vars => DoneIndexValue'
BY DEFS DoneIndexValue, vars
<1>c. DoneIndexValue /\ TypeOK /\ Next => DoneIndexValue'
<2>a. DoneIndexValue /\ Terminating => DoneIndexValue'
BY DEFS DoneIndexValue, Terminating, vars
<2>b. DoneIndexValue /\ TypeOK /\ lb => DoneIndexValue'
BY DEFS DoneIndexValue, TypeOK, lb
<2> QED BY <2>a, <2>b DEF Next
<1> QED BY PTL, <1>a, <1>b, <1>c, TypeInvariantHolds DEF Spec
\* The main event! After the algorithm has terminated, the variable h must
\* have value greater than or equal to any element of the sequence.
Correctness ==
pc = "Done" =>
\A idx \in DOMAIN f : f[idx] <= h
THEOREM IsCorrect == Spec => []Correctness
PROOF
<1>a. Init => Correctness
BY DEF Init, Correctness
<1>b. Correctness /\ UNCHANGED vars => Correctness'
BY DEF Correctness, vars
<1>c. /\ Correctness
/\ InductiveInvariant'
/\ DoneIndexValue'
/\ Next
=> Correctness'
<2>a. Correctness /\ Terminating => Correctness'
BY DEF Correctness, Terminating, vars
<2>b.
/\ Correctness
/\ InductiveInvariant'
/\ DoneIndexValue'
/\ lb
=> Correctness'
BY DEFS Correctness, InductiveInvariant, DoneIndexValue, lb
<2> QED BY <2>a, <2>b DEF Next
<1> QED
BY
<1>a, <1>b, <1>c,
InductiveInvariantHolds, DoneIndexValueThm, PTL
DEF Spec
=============================================================================