---------------------------- 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 \* Correctness is implied by the preceding invariants. THEOREM IsCorrect == Spec => []Correctness <1>1. TypeOK /\ InductiveInvariant /\ DoneIndexValue => Correctness BY DEF TypeOK, InductiveInvariant, DoneIndexValue, Correctness <1>. QED BY <1>1, TypeInvariantHolds, InductiveInvariantHolds, DoneIndexValueThm, PTL =============================================================================

LearnProofs