---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/FindHighest.tla
---
------------------------------ 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 \union { - 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
================================================================================