From 1fcaf8b893b75ed40a3df0fc63b633636ba776e9 Mon Sep 17 00:00:00 2001 From: Stephan Merz Date: Sat, 6 Dec 2025 09:09:56 +0100 Subject: [PATCH] fix broken proofs in examples Signed-off-by: Stephan Merz --- examples/AtomicBakery.tla | 74 +- examples/AtomicBakeryWithoutSMT.tla | 35 +- examples/Bakery.tla | 32 +- examples/BubbleSort.tla | 10 +- examples/ByzPaxos/BPConProof.tla | 125 ++- examples/ByzPaxos/Consensus.tla | 48 +- examples/ByzPaxos/VoteProof.tla | 135 ++-- examples/Dekker/Dekker.tla | 19 +- examples/EWD840.tla | 31 +- examples/GraphTheorem.tla | 36 +- examples/LamportMutex.tla | 944 ---------------------- examples/SimpleEventuallyInt.tla | 2 +- examples/paxos/Paxos.tla | 58 +- examples_draft/FOLTL.tla | 23 +- examples_draft/quicksort/Quicksort01.tla | 121 --- examples_draft/quicksort/Quicksort02.tla | 185 ----- examples_draft/quicksort/Quicksort03.tla | 450 ----------- examples_draft/quicksort/Quicksort04.tla | 292 ------- examples_draft/quicksort/Quicksort05.tla | 361 --------- examples_draft/quicksort/Quicksort06.tla | 270 ------- examples_draft/quicksort/Quicksort07.tla | 690 ---------------- examples_draft/quicksort/Quicksort07d.tla | 662 --------------- examples_draft/quicksort/Quicksort21.tla | 380 --------- examples_draft/quicksort/Utils.tla | 237 ------ library/FiniteSetTheorems.tla | 2 +- library/FiniteSetTheorems_proofs.tla | 50 +- 26 files changed, 352 insertions(+), 4920 deletions(-) delete mode 100644 examples/LamportMutex.tla delete mode 100755 examples_draft/quicksort/Quicksort01.tla delete mode 100755 examples_draft/quicksort/Quicksort02.tla delete mode 100755 examples_draft/quicksort/Quicksort03.tla delete mode 100755 examples_draft/quicksort/Quicksort04.tla delete mode 100755 examples_draft/quicksort/Quicksort05.tla delete mode 100755 examples_draft/quicksort/Quicksort06.tla delete mode 100644 examples_draft/quicksort/Quicksort07.tla delete mode 100644 examples_draft/quicksort/Quicksort07d.tla delete mode 100644 examples_draft/quicksort/Quicksort21.tla delete mode 100644 examples_draft/quicksort/Utils.tla diff --git a/examples/AtomicBakery.tla b/examples/AtomicBakery.tla index 11f4f3962..2ad5d2004 100644 --- a/examples/AtomicBakery.tla +++ b/examples/AtomicBakery.tla @@ -27,7 +27,7 @@ EXTENDS Naturals, TLAPS (* is a natural number. *) (***************************************************************************) CONSTANT N -ASSUME N \in Nat +ASSUME NAssumption == N \in Nat (***************************************************************************) (* We define P to be the set {1, 2, ... , N} of processes. *) @@ -67,7 +67,7 @@ p4: flag[self] := FALSE; unread := P \ {self} ; p5: while (unread # {}) { with (i \in unread) { nxt := i ; }; - await ~ flag[nxt]; + await (flag[nxt] = FALSE); p6: await \/ num[nxt] = 0 \/ LL(self, nxt) ; unread := unread \ {nxt}; @@ -79,7 +79,7 @@ p7: num[self] := 0; **** this ends the comment containg the pluscal code **********) \* BEGIN TRANSLATION (this begins the translation of the PlusCal code) -VARIABLES num, flag, pc +VARIABLES pc, num, flag (* define statement *) LL(j, i) == \/ num[j] < num[i] @@ -88,7 +88,7 @@ LL(j, i) == \/ num[j] < num[i] VARIABLES unread, max, nxt -vars == << num, flag, pc, unread, max, nxt >> +vars == << pc, num, flag, unread, max, nxt >> ProcSet == (P) @@ -136,7 +136,7 @@ p5(self) == /\ pc[self] = "p5" /\ IF unread[self] # {} THEN /\ \E i \in unread[self]: nxt' = [nxt EXCEPT ![self] = i] - /\ ~ flag[nxt'[self]] + /\ (flag[nxt'[self]] = FALSE) /\ pc' = [pc EXCEPT ![self] = "p6"] ELSE /\ pc' = [pc EXCEPT ![self] = "cs"] /\ nxt' = nxt @@ -192,6 +192,13 @@ TypeOK == /\ num \in [P -> Nat] /\ pc \in [P -> {"p1", "p2", "p3", "p4", "p5", "p6", "cs", "p7"}] +THEOREM Typing == Spec => []TypeOK +<1>. USE DEF ProcSet, TypeOK +<1>1. Init => TypeOK + BY DEF Init +<1>2. TypeOK /\ [Next]_vars => TypeOK' + BY DEF Next, vars, p, p1, p2, p3, p4, p5, p6, p7, cs +<1>. QED BY <1>1, <1>2, PTL DEF Spec (***************************************************************************) (* After(i, j) is a condition that implies that num[j] > 0 and, if i is *) @@ -226,9 +233,9 @@ IInv(i) == /\ (pc[i] \in {"cs", "p7"}) => \A j \in P \ {i} : After(j, i) (***************************************************************************) -(* Inv is the complete inductive invariant. *) +(* Inv is the main inductive invariant, modulo type correctness. *) (***************************************************************************) -Inv == TypeOK /\ \A i \in P : IInv(i) +Inv == \A i \in P : IInv(i) ----------------------------------------------------------------------------- (***************************************************************************) (* Proof of Mutual Exclusion *) @@ -238,54 +245,35 @@ Inv == TypeOK /\ \A i \in P : IInv(i) (* which Inv is true leaves Inv true. Step <1>4 follows easily from *) (* <1>1-<1>3 by simple temporal reasoning. *) (***************************************************************************) -THEOREM Spec => []Inv -<1> USE DEFS TypeOK, Inv, IInv, ProcSet -<1>1. Init => Inv - BY DEFS Init, Inv -<1>2. Inv /\ [Next]_vars => Inv' - <2> SUFFICES ASSUME Inv, [Next]_vars PROVE Inv' - OBVIOUS - <2> USE DEFS After, LL +THEOREM Spec => []MutualExclusion +<1>. USE NAssumption DEFS ProcSet, TypeOK +<1>1. Init => Inv + BY DEF Init, Inv, IInv +<1>2. TypeOK /\ Inv /\ [Next]_vars => Inv' + <2>. SUFFICES ASSUME TypeOK, Inv, Next + PROVE Inv' + BY DEF Inv, IInv, After, LL, vars + <2>. USE DEFS Inv, IInv, After, LL, P <2>1. ASSUME NEW self \in P, p1(self) PROVE Inv' BY <2>1 DEF p1 <2>2. ASSUME NEW self \in P, p2(self) PROVE Inv' - <3>1. CASE unread[self] = {} - BY <2>2, <3>1 DEF p2 - <3>2. CASE unread[self] # {} - BY <2>2, <3>2 DEF p2 - <3>3. QED - BY <3>1, <3>2 + BY <2>2 DEF p2 <2>3. ASSUME NEW self \in P, p3(self) PROVE Inv' BY <2>3 DEF p3 <2>4. ASSUME NEW self \in P, p4(self) PROVE Inv' BY <2>4 DEF p4 <2>5. ASSUME NEW self \in P, p5(self) PROVE Inv' - <3>1. CASE unread[self] = {} - BY <2>5, <3>1 DEF p5 - <3>2. CASE unread[self] # {} - BY <2>5, <3>2, CVC4T(30) DEF p5 - <3>3. QED - BY <3>1, <3>2 + BY <2>5, SMTT(20) DEF p5 <2>6. ASSUME NEW self \in P, p6(self) PROVE Inv' - <3>p. P \subseteq Nat - BY N \in Nat DEF P - <3>1. CASE num[nxt[self]] = 0 - BY <2>6, <3>1 DEF p6 - <3>2. CASE LL(self, nxt[self]) - BY <2>6, <3>2, <3>p DEF p6 - <3>3. QED - BY <2>6, <3>1, <3>2 DEF p6 + BY <2>6, SMTT(20) DEF p6 <2>7. ASSUME NEW self \in P, cs(self) PROVE Inv' - BY <2>7 DEF cs + BY <2>7, SMTT(20) DEF cs <2>8. ASSUME NEW self \in P, p7(self) PROVE Inv' BY <2>8 DEF p7 - <2>9. CASE UNCHANGED vars - BY <2>9 DEF vars - <2>10. QED - BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7, <2>8, <2>9 DEF Next, p + <2>. QED BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7, <2>8 DEF Next, p <1>3. Inv => MutualExclusion - BY DEFS Inv, After, MutualExclusion -<1>4. QED - BY <1>1, <1>2, <1>3, PTL DEF Spec + BY DEF Inv, IInv, After, MutualExclusion +<1>. QED BY <1>1, <1>2, <1>3, Typing, PTL DEF Spec + ============================================================================= diff --git a/examples/AtomicBakeryWithoutSMT.tla b/examples/AtomicBakeryWithoutSMT.tla index 92785ab4f..2191f1d7d 100644 --- a/examples/AtomicBakeryWithoutSMT.tla +++ b/examples/AtomicBakeryWithoutSMT.tla @@ -198,26 +198,31 @@ Inv == TypeOK /\ \A i \in P : IInv(i) ----------------------------------------------------------------------------- THEOREM GTAxiom == \A n, m \in Nat : ~ (n > m /\ m > n) - OBVIOUS (*{ by (isabelle "(auto dest: nat_less_trans)") }*) + BY Isa THEOREM GEQAxiom == \A n, m \in Nat : (n = m) \/ n > m \/ m > n - OBVIOUS (*{ by (isabelle "(auto elim: nat_less_cases)") }*) + BY Isa THEOREM GEQTransitive == \A n, m, q \in Nat : n >= m /\ m >= q => n >= q - OBVIOUS (*{ by (isabelle "(auto dest: nat_leq_trans)") }*) + OBVIOUS (*{ by (isabelle "(auto dest: int_leq_trans)") }*) THEOREM Transitivity2 == \A n, m, q \in Nat : n > m /\ m >= q => n > q - OBVIOUS (*{ by (isabelle "(auto dest: nat_leq_less_trans)") }*) + OBVIOUS (*{ by (isabelle "(auto dest: int_leq_less_trans)") }*) THEOREM GEQorLT == \A n, m \in Nat : n >= m <=> ~(m > n) - OBVIOUS (*{ by (isabelle "(auto simp: nat_not_less[simplified])") }*) + BY Isa +\* OBVIOUS (*{ by (isabelle "(auto simp: nat_not_less[simplified])") }*) THEOREM NatGEQZero == \A n \in Nat: (n > 0) <=> (n # 0) - OBVIOUS (*{ by (isabelle "(auto simp: nat_gt0_not0)") }*) + BY Isa +\* OBVIOUS (*{ by (isabelle "(auto simp: nat_gt0_not0)") }*) THEOREM Plus1 == \A n \in Nat: n+1 \in Nat /\ n+1 # 0 BY Isa +THEOREM Plus1GT == \A n \in Nat : n+1 > n + BY Isa + THEOREM GGIrreflexive == ASSUME NEW i \in P, NEW j \in P, i # j, @@ -390,13 +395,21 @@ THEOREM InductiveInvariant == Inv /\ Next => Inv' (* We start by proving two auxiliary assertions *) <2>1. max'[self] >= max[self] /\ max'[self] >= num[k] <3>1. CASE num[k] > max[self] - BY <3>1, k \in P, SimplifyAndSolve - (* FIXME: Isabelle needs "k \in P" but doesn't find it by itself *) + <4>. /\ k \in P + /\ num[k] \in Nat + /\ max'[self] = num[k] + BY <3>1, Zenon + <4>. QED BY <3>1, Isa <3>2. CASE ~(num[k] > max[self]) + <4>. /\ max[self] \in Nat + /\ UNCHANGED max + BY <3>2, Zenon <4>1. max[self] >= num[k] BY <3>2, GEQorLT, Zenon - <4>2. QED - BY <3>2, <4>1, SimplifyAndSolve + <4>2. max[self] >= max[self] + BY Isa + <4>. QED + BY <3>2, <4>1, <4>2, Zenon <3>3. QED BY <3>1, <3>2, Zenon <2>2. After(self,i) => After(self,i)' @@ -438,7 +451,7 @@ THEOREM InductiveInvariant == Inv /\ Next => Inv' <4>1. max[j] >= num[i] BY <3>1, Zenon DEF After <4>2. num'[j] > max[j] - BY SimplifyAndSolve + BY Plus1GT, Zenon <4>3. num'[j] > num[i] BY <4>1, <4>2, Plus1, Transitivity2, Zenon <4>4. GG(i,j)' diff --git a/examples/Bakery.tla b/examples/Bakery.tla index 85794e45e..35f6accfb 100644 --- a/examples/Bakery.tla +++ b/examples/Bakery.tla @@ -111,7 +111,7 @@ p4: unread := P \ {self} ; or { flag[self] := FALSE } ; p5: while (unread # {}) { with (i \in unread) { nxt := i ; }; - await ~ flag[nxt]; + await (flag[nxt] = FALSE); p6: await \/ num[nxt] = 0 \/ LL(self, nxt) ; unread := unread \ {nxt}; @@ -127,7 +127,7 @@ p7: with (repeat \in BOOLEAN, k \in Nat) { **** this ends the comment containg the pluscal code **********) \* BEGIN TRANSLATION (this begins the translation of the PlusCal code) -VARIABLES num, flag, pc +VARIABLES pc, num, flag (* define statement *) LL(j, i) == \/ num[j] < num[i] @@ -136,7 +136,7 @@ LL(j, i) == \/ num[j] < num[i] VARIABLES unread, max, nxt -vars == << num, flag, pc, unread, max, nxt >> +vars == << pc, num, flag, unread, max, nxt >> ProcSet == (P) @@ -194,7 +194,7 @@ p5(self) == /\ pc[self] = "p5" /\ IF unread[self] # {} THEN /\ \E i \in unread[self]: nxt' = [nxt EXCEPT ![self] = i] - /\ ~ flag[nxt'[self]] + /\ (flag[nxt'[self]] = FALSE) /\ pc' = [pc EXCEPT ![self] = "p6"] ELSE /\ pc' = [pc EXCEPT ![self] = "cs"] /\ nxt' = nxt @@ -329,7 +329,11 @@ THEOREM Spec => []MutualExclusion <2>3. ASSUME NEW self \in P, p3(self) PROVE Inv' - BY <2>3, Z3T(60) DEF p3, TypeOK, IInv, After, LL + <3>1. TypeOK' + BY <2>3 DEF p3, TypeOK + <3>2. ASSUME NEW i \in P PROVE IInv(i)' + BY <2>3, SMTT(60) DEF p3, TypeOK, IInv, After, LL + <3>. QED BY <3>1, <3>2 <2>4. ASSUME NEW self \in P, p4(self) PROVE Inv' @@ -341,7 +345,21 @@ THEOREM Spec => []MutualExclusion <2>5. ASSUME NEW self \in P, p5(self) PROVE Inv' - BY <2>5, Z3T(60) DEF p5, TypeOK, IInv, After, LL + <3>1. TypeOK' + <4>1. /\ num' \in [P -> Nat] + /\ flag' \in [P -> BOOLEAN] + /\ unread' \in [P -> SUBSET P] + /\ max' \in [P -> Nat] + /\ nxt' \in [P -> P] + /\ pc' \in [P -> {"p1", "p2", "p3", "p4", "p5", "p6", "cs", "p7"}] + BY <2>5 DEF p5, TypeOK + <4>2. /\ \A i \in P : pc'[i] \in {"p2", "p5", "p6"} => i \notin unread'[i] + /\ \A i \in P : (pc'[i] = "p6") => nxt'[i] # i + BY <2>5 DEF p5, TypeOK + <4>. QED BY <4>1, <4>2 DEF TypeOK + <3>2. ASSUME NEW i \in P PROVE IInv(i)' + BY <2>5, SMTT(20) DEF p5, TypeOK, IInv, After, LL + <3>. QED BY <3>1, <3>2 <2>6. ASSUME NEW self \in P, p6(self) PROVE Inv' @@ -349,7 +367,7 @@ THEOREM Spec => []MutualExclusion <2>7. ASSUME NEW self \in P, cs(self) PROVE Inv' - BY <2>7 DEF cs, TypeOK, IInv, After, LL + BY <2>7, SMTT(20) DEF cs, TypeOK, IInv, After, LL <2>8. ASSUME NEW self \in P, p7(self) PROVE Inv' diff --git a/examples/BubbleSort.tla b/examples/BubbleSort.tla index 005fec9e2..938ace446 100644 --- a/examples/BubbleSort.tla +++ b/examples/BubbleSort.tla @@ -205,8 +205,9 @@ THEOREM Spec => [](pc = "Done" => IsSorted(A) /\ IsPermOf(A, A0)) <2> SUFFICES ASSUME Inv, Lbl_1 \/ Lbl_2 \* Next PROVE Inv' <3>1. Inv /\ UNCHANGED vars => Inv' - BY DEF vars, TypeOK, RealInv, IsSorted, IsSortedTo, - IsSortedFromTo, IsPermOf, Perms, ** + BY Zenon + DEF vars, TypeOK, RealInv, IsSorted, IsSortedTo, + IsSortedFromTo, IsPermOf, Perms, ** <3>2. QED BY <3>1 DEF Next <2>1. TypeOK' @@ -228,9 +229,4 @@ THEOREM Spec => [](pc = "Done" => IsSorted(A) /\ IsPermOf(A, A0)) (***************************************************************************) ============================================================================= \* Modification History -\* Last modified Wed Aug 28 14:03:35 CEST 2019 by merz -\* Last modified Mon Mar 17 11:17:49 CET 2014 by doligez -\* Last modified Fri Mar 07 15:24:43 CET 2014 by shaolin -\* Last modified Tue Nov 27 13:33:10 CET 2012 by doligez -\* Last modified Fri Nov 23 09:32:08 PST 2012 by lamport \* Created Wed Nov 21 11:50:58 PST 2012 by lamport diff --git a/examples/ByzPaxos/BPConProof.tla b/examples/ByzPaxos/BPConProof.tla index cd49eed44..a412f41db 100644 --- a/examples/ByzPaxos/BPConProof.tla +++ b/examples/ByzPaxos/BPConProof.tla @@ -605,7 +605,13 @@ Quorum == {S \cap Acceptor : S \in ByzQuorum} THEOREM QuorumTheorem == /\ \A Q1, Q2 \in Quorum : Q1 \cap Q2 # {} /\ \A Q \in Quorum : Q \subseteq Acceptor -BY BQA DEF Quorum +<1>1. ASSUME NEW Q1 \in Quorum, NEW Q2 \in Quorum + PROVE Q1 \cap Q2 # {} + BY BQA, ZenonT(20) DEF Quorum +<1>2. ASSUME NEW Q \in Quorum + PROVE Q \subseteq Acceptor + BY BQA DEF Quorum +<1>. QED BY <1>1, <1>2 (***************************************************************************) (* We now define refinement mapping under which our algorithm implements *) @@ -719,7 +725,7 @@ LEMMA MaxBallotLemma1 == /\ y >= MaxBallot(S) BY MaxBallotProp <1>3. MaxBallot(S) \in Int /\ y \in Int - BY <1>1, <1>2, Isa DEF Ballot + BY <1>1, <1>2 DEF Ballot <1>. QED BY <1>1, <1>2, <1>3 LEMMA MaxBallotLemma2 == @@ -844,7 +850,10 @@ bmsgsFinite == IsFiniteSet(1bOr2bMsgs) LEMMA FiniteMsgsLemma == ASSUME NEW m, bmsgsFinite, bmsgs' = bmsgs \cup {m} PROVE bmsgsFinite' -BY FS_AddElement DEF bmsgsFinite, 1bOr2bMsgs +<1>. \/ 1bOr2bMsgs' = 1bOr2bMsgs + \/ 1bOr2bMsgs' = 1bOr2bMsgs \cup {m} + BY DEF 1bOr2bMsgs +<1>. QED BY FS_AddElement DEF bmsgsFinite (***************************************************************************) (* Invariant 1bInv1 asserts that if (good) acceptor `a' has mCBal[a] # -1, *) @@ -1126,7 +1135,7 @@ TypeOK => /\ 1cmsgs' = 1cmsgs /\ 2amsgs' = 2amsgs /\ acceptorMsgsOfType("2b")' = acceptorMsgsOfType("2b") - BY <2>1 DEF msgsOfType, 1bmsgs, acceptorMsgsOfType, KnowsSafeAt, 1cmsgs, 2amsgs + BY <2>1, Isa DEF msgsOfType, 1bmsgs, acceptorMsgsOfType, KnowsSafeAt, 1cmsgs, 2amsgs <2>. QED BY <2>a DEF msgs, 1bRestrict @@ -1158,8 +1167,12 @@ TypeOK => /\ 1cmsgs' = 1cmsgs /\ acceptorMsgsOfType("2b")' = acceptorMsgsOfType("2b") BY <2>1, <3>1 DEF msgsOfType, 1bmsgs, 1bRestrict, acceptorMsgsOfType, KnowsSafeAt, 1cmsgs + <3>3. 2amsgs \subseteq 2amsgs' + BY <2>1 DEF 2amsgs, acceptorMsgsOfType, msgsOfType + <3>4. 2amsgs' \subseteq 2amsgs \cup {ma} + BY <2>1 DEF 2amsgs, acceptorMsgsOfType, msgsOfType <3>. QED - BY <3>1, <3>2, <2>1, <2>3 DEF msgs, 2amsgs, msgsOfType, acceptorMsgsOfType + BY <2>3, <3>2, <3>3, <3>4, Zenon DEF msgs <2>6. QED BY <2>4, <2>5 @@ -1190,7 +1203,7 @@ TypeOK => /\ 1cmsgs' = 1cmsgs /\ 2amsgs' = 2amsgs /\ acceptorMsgsOfType("2b")' = acceptorMsgsOfType("2b") \cup {bm} - BY <2>1 DEF msgsOfType, 1bmsgs, 1bRestrict, 1cmsgs, KnowsSafeAt, 2amsgs, acceptorMsgsOfType + BY <2>1, Isa DEF msgsOfType, 1bmsgs, 1bRestrict, 1cmsgs, KnowsSafeAt, 2amsgs, acceptorMsgsOfType <2>4. msgs' = msgs \cup {bm} BY <2>2 DEF msgs <2>. QED @@ -1212,7 +1225,16 @@ TypeOK => BY <1>4, Zenon DEF LearnsSent <3>3. ASSUME NEW m \in 1cmsgs PROVE m \in 1cmsgs' - BY <3>1, <3>2 DEF TypeOK, KnowsSafeAt, 1cmsgs, msgsOfType + <4>1. PICK a \in Acceptor : + /\ m \in msgsOfType("1c") + /\ KnowsSafeAt(a, m.bal, m.val) + BY DEF 1cmsgs + <4>2. m \in msgsOfType("1c")' + BY <3>1, <4>1 DEF msgsOfType + <4>3. KnowsSafeAt(a, m.bal, m.val)' + BY <3>2, <4>1 DEF TypeOK, KnowsSafeAt + <4>. QED + BY <4>2, <4>3 DEF 1cmsgs <3>4. ASSUME NEW m \in 1cmsgs', m \notin 1cmsgs PROVE m \in msgsOfType("1c") /\ m.bal = b <4>1. m \in msgsOfType("1c") @@ -1258,17 +1280,41 @@ TypeOK => BY <2>1, Zenon <2>2. /\ msgsOfType("1a")' = msgsOfType("1a") /\ 1bmsgs' = 1bmsgs - /\ 1cmsgs' = 1cmsgs \cup SS - /\ 2amsgs' = 2amsgs /\ acceptorMsgsOfType("2b")' = acceptorMsgsOfType("2b") - BY <2>1 DEF msgsOfType, 1bmsgs, 1bRestrict, 1cmsgs, KnowsSafeAt, 2amsgs, acceptorMsgsOfType - <2>3. QED - BY <2>2 DEF msgs + BY <2>1 DEF msgsOfType, 1bmsgs, 1bRestrict, 1cmsgs, KnowsSafeAt, 2amsgs, acceptorMsgsOfType + <2>3. \A a,b,v : KnowsSafeAt(a,b,v)' <=> KnowsSafeAt(a,b,v) + BY <2>1 DEF KnowsSafeAt + <2>4. 1cmsgs' = 1cmsgs \cup SS + BY <2>1, <2>3 DEF 1cmsgs, msgsOfType + <2>5. acceptorMsgsOfType("2av")' = acceptorMsgsOfType("2av") + BY <2>1 DEF acceptorMsgsOfType, msgsOfType + <2>6. 2amsgs' = 2amsgs + BY <2>5 DEF 2amsgs + <2>. QED + BY <2>2, <2>4, <2>6 DEF msgs <1>7. ASSUME NEW self \in FakeAcceptor, FakingAcceptor(self) PROVE msgs' = msgs - BY <1>7, BQA DEF FakingAcceptor, msgs, 1bMessage, 2avMessage, 2bMessage, - msgsOfType, 1cmsgs, KnowsSafeAt, 1bmsgs, 2amsgs, acceptorMsgsOfType, msgsOfType + <2>1. PICK m \in 1bMessage \cup 2avMessage \cup 2bMessage : + /\ m.acc = self + /\ bmsgs' = bmsgs \cup {m} + /\ knowsSent' = knowsSent + BY <1>7 DEF FakingAcceptor + <2>2. \A a,b,v : KnowsSafeAt(a,b,v)' <=> KnowsSafeAt(a,b,v) + BY <2>1 DEF KnowsSafeAt + <2>3. /\ msgsOfType("1a")' = msgsOfType("1a") + /\ 1cmsgs' = 1cmsgs + BY <2>1, <2>2 DEF msgsOfType, 1cmsgs, 1bMessage, 2avMessage, 2bMessage + <2>4. 1bmsgs' = 1bmsgs + BY <2>1, BQA DEF 1bmsgs, acceptorMsgsOfType, msgsOfType, 1bRestrict, 1bMessage, 2avMessage, 2bMessage + <2>5. acceptorMsgsOfType("2av")' = acceptorMsgsOfType("2av") + BY <2>1, BQA DEF acceptorMsgsOfType, msgsOfType, 1bMessage, 2avMessage, 2bMessage + <2>6. 2amsgs' = 2amsgs + BY <2>1, <2>5 DEF 2amsgs + <2>7. acceptorMsgsOfType("2b")' = acceptorMsgsOfType("2b") + BY <2>1, BQA DEF acceptorMsgsOfType, msgsOfType, 1bMessage, 2avMessage, 2bMessage + <2>. QED + BY <2>3, <2>4, <2>6, <2>7 DEF msgs <1>9. QED BY <1>1, <1>2, <1>3, <1>4, <1>5, <1>6, <1>7, Zenon @@ -1302,7 +1348,21 @@ THEOREM Invariance == Spec => []Inv <4>1. msgs' = msgs \cup {mc} BY <3>1, MsgsLemma DEF Inv <4>2. TypeOK' - BY <3>1 DEF Inv, TypeOK, BMessage, 1bMessage, ByzAcceptor, Phase1b + <5>1. /\ maxBal' \in [Acceptor -> Ballot \cup {-1}] + /\ 2avSent' \in [Acceptor -> SUBSET [val : Value, bal : Ballot]] + /\ maxVBal' \in [Acceptor -> Ballot \cup {-1}] + /\ maxVVal' \in [Acceptor -> Value \cup {None}] + /\ knowsSent' \in [Acceptor -> SUBSET 1bMessage] + BY <3>1 DEF Inv, TypeOK, Phase1b + <5>2. bmsgs' = bmsgs \cup {mb} + BY <3>1 DEF Phase1b + <5>3. mb \in BMessage + BY Zenon DEF Inv, TypeOK, BMessage, 1bMessage, ByzAcceptor + <5>4. bmsgs' \subseteq BMessage + BY <5>2, <5>3 DEF Inv, TypeOK + <5>. QED + BY <5>1, <5>4 DEF TypeOK + \* BY <3>1 DEF Inv, TypeOK, BMessage, 1bMessage, ByzAcceptor, Phase1b <4>3. bmsgsFinite' BY <3>1, FiniteMsgsLemma, Zenon DEF Inv, bmsgsFinite, Phase1b <4>4. 1bInv1' @@ -1343,7 +1403,7 @@ THEOREM Invariance == Spec => []Inv ![self] = {r \in 2avSent[self] : r.val # mc.val} \cup {[val |-> mc.val, bal |-> b]}] BY <3>2, Zenon DEF Phase2av - <4>2. mc = [type |-> "1c", bal |-> mc.bal, val |-> mc.val] + <4>2. mc = [type |-> "1c", bal |-> b, val |-> mc.val] BY <4>1, BMessageLemma DEF sentMsgs, Inv, TypeOK, 1cMessage <4> DEFINE mb == [type |-> "2av", bal |-> b, val |-> mc.val, acc |-> self] @@ -1415,8 +1475,18 @@ THEOREM Invariance == Spec => []Inv <5>2. CASE r \in 2avSent[a] BY <5>2, <4>4, <4>5, <3>2 DEF Phase2av, Inv, TypeOK, accInv, Ballot <5>3. CASE r \notin 2avSent[a] - BY <5>3, <3>2, <4>1, <4>2, <4>4 - DEF Phase2av, Inv, TypeOK, sentMsgs, msgsOfType, msgs, 1cmsgs, Ballot + <6>1. /\ a = self + /\ r = [val |-> mc.val, bal |-> b] + BY <4>1, <5>1, <5>3 DEF Inv, TypeOK + <6>2. /\ \A r \in 2avSent[self] : r.bal < b + /\ maxBal' = [maxBal EXCEPT ![self] = b] + BY <3>2 DEF Phase2av + <6>3. r.bal =< maxBal'[a] + BY <6>1, <6>2 DEF Inv, TypeOK, Ballot + <6>4. mc \in msgs + BY <4>1, <4>2 DEF sentMsgs, msgs, 1cmsgs, msgsOfType + <6>. QED + BY <4>2, <4>4, <6>1, <6>3, <6>4 <5>4. QED BY <5>2, <5>3 <4>14. knowsSentInv' @@ -1544,7 +1614,7 @@ THEOREM Invariance == Spec => []Inv <4>3. TypeOK' BY <3>2, <4>1 DEF Phase1c, Inv, TypeOK, BMessage, 1cMessage <4>4. bmsgsFinite' - BY <4>1 DEF Inv, bmsgsFinite, 1bOr2bMsgs + BY <4>1, Zenon DEF Inv, bmsgsFinite, 1bOr2bMsgs <4>5. 1bInv1' BY <3>2, <4>2, Zenon DEF Phase1c, Inv, 1bInv1 <4>6. 1bInv2' @@ -1600,7 +1670,7 @@ THEOREM Invariance == Spec => []Inv PROVE Inv' <3> USE UNCHANGED vars DEF Inv, vars <3> msgs = msgs' - BY DEF msgs, msgsOfType, 1bmsgs, 1bRestrict, acceptorMsgsOfType, 1cmsgs, + BY Isa DEF msgs, msgsOfType, 1bmsgs, 1bRestrict, acceptorMsgsOfType, 1cmsgs, KnowsSafeAt, 2amsgs <3> QED BY DEF TypeOK, bmsgsFinite, 1bOr2bMsgs, 1bInv1, 1bInv2, @@ -1623,9 +1693,9 @@ THEOREM Spec => P!Spec <2>1. MaxBallot({}) = -1 BY MaxBallotProp, FS_EmptySet <2>2. P!Init!1 /\ P!Init!2 /\ P!Init!3 - BY <2>1 DEF Init, PmaxBal, 1bOr2bMsgs, None, P!None + BY <2>1, Zenon DEF Init, PmaxBal, 1bOr2bMsgs, None, P!None <2>3. msgs = {} - BY BQA DEF Init, msgsOfType, acceptorMsgsOfType, 1bmsgs, 1cmsgs, 2amsgs, Quorum, msgs + BY QuorumTheorem, Zenon DEF Init, msgsOfType, acceptorMsgsOfType, 1bmsgs, 1cmsgs, 2amsgs, msgs <2>4. QED BY <2>2, <2>3 DEF P!Init @@ -1634,8 +1704,8 @@ THEOREM Spec => P!Spec <2> SUFFICES ASSUME Inv, InvP, Next PROVE P!TLANext \/ P!vars' = P!vars <3> UNCHANGED vars => UNCHANGED P!vars - BY DEF vars, P!vars, PmaxBal, 1bOr2bMsgs, msgs, msgsOfType, acceptorMsgsOfType, - 1bmsgs, 2amsgs, 1cmsgs, KnowsSafeAt + BY Isa DEF vars, P!vars, PmaxBal, 1bOr2bMsgs, msgs, msgsOfType, acceptorMsgsOfType, + 1bmsgs, 2amsgs, 1cmsgs, KnowsSafeAt <3> QED BY PNextDef DEF Inv, P!ProcSet, P!Init, Ballot, P!Ballot <2> HIDE DEF InvP @@ -1819,7 +1889,7 @@ THEOREM Spec => P!Spec <6> MaxBallot({b}) = b BY FS_Singleton, MaxBallotLemma1, Isa DEF Ballot <6> QED - BY <5>4, <5>5 + BY <5>4, <5>5, Zenon <5>6. CASE S # {} <6> \A bb \in T : b >= bb BY <3>1, <5>1, <5>3, MaxBallotProp, PmaxBalLemma5 DEF Inv, Ballot @@ -2118,9 +2188,4 @@ BY Isa DEF chosen, P!chosen, Quorum, Ballot, P!Ballot ============================================================================== \* Modification History -\* Last modified Fri Jul 24 17:51:34 CEST 2020 by merz -\* Last modified Wed Apr 15 15:16:26 CEST 2020 by doligez -\* Last modified Mon Aug 18 14:57:27 CEST 2014 by tomer -\* Last modified Mon Mar 04 17:24:05 CET 2013 by doligez -\* Last modified Wed Nov 30 15:47:26 PST 2011 by lamport \* Last modified Wed Dec 01 11:35:29 PST 2010 by lamport diff --git a/examples/ByzPaxos/Consensus.tla b/examples/ByzPaxos/Consensus.tla index cb51516c7..f34dc3a1e 100644 --- a/examples/ByzPaxos/Consensus.tla +++ b/examples/ByzPaxos/Consensus.tla @@ -147,7 +147,7 @@ LEMMA InductiveInvariance == OBVIOUS <1>1. CASE Next \* In the following BY proof, <1>1 denotes the case assumption Next - BY <1>1, FS_EmptySet, FS_AddElement DEF Inv, TypeOK, Next + BY <1>1, FS_Singleton DEF Inv, TypeOK, Next <1>2. CASE vars' = vars BY <1>2 DEF Inv, TypeOK, vars <1>3. QED @@ -177,43 +177,15 @@ Success == <>(chosen # {}) ASSUME ValueNonempty == Value # {} (***************************************************************************) -(* TLAPS does not yet reason about ENABLED. Therefore, we must omit all *) -(* proofs that involve ENABLED formulas. To perform as much of the proof *) -(* as possible, as much as possible we restrict the use of an ENABLED *) -(* expression to a step asserting that it equals its definition. ENABLED *) -(* A is true of a state s iff there is a state t such that the step s -> t *) -(* satisfies A. It follows from this semantic definition that ENABLED A *) -(* equals the formula obtained by *) -(* *) -(* 1. Expanding all definitions of defined symbols in A until all primes *) -(* are priming variables. *) -(* *) -(* 2. For each primed variable, replacing every instance of that primed *) -(* variable by a new symbol (the same symbol for each primed *) -(* variable). *) -(* *) -(* 3. Existentially quantifying over those new symbols. *) +(* We start by reducing the enabledness condition to a simple state *) +(* predicate. For this specification, the proof is so simple that it *) +(* could simply be done in the proof of the liveness condition. For larger *) +(* specifications, it is good practice to state an extra lemma. *) (***************************************************************************) LEMMA EnabledDef == - TypeOK => - ((ENABLED <>_vars) <=> (chosen = {})) -<1> DEFINE E == - \E chosenp : - /\ /\ chosen = {} - /\ \E v \in Value: chosenp = {v} - /\ ~ (<> = <>) -<1>1. E = ENABLED <>_vars - \* BY DEF Next, vars (* and def of ENABLED *) - PROOF OMITTED -<1>2. SUFFICES ASSUME TypeOK - PROVE E = (chosen = {}) - BY <1>1, Zenon -<1>3. E = \E chosenp : E!(chosenp)!1 - BY <1>2, Isa DEF TypeOK -<1>4. @ = (chosen = {}) - BY <1>2, ValueNonempty, Zenon DEF TypeOK -<1>5. QED - BY <1>3, <1>4, Zenon + (ENABLED <>_vars) <=> (chosen = {}) +BY ValueNonempty, ExpandENABLED DEF Next, vars + (***************************************************************************) (* Here is our proof that Livespec implies Success. It uses the standard *) @@ -271,8 +243,4 @@ THEOREM LiveSpecEquals == BY <1>1, <1>3, PTL DEF LiveSpec ============================================================================= \* Modification History -\* Last modified Mon May 11 18:36:27 CEST 2020 by merz -\* Last modified Mon Aug 18 15:00:45 CEST 2014 by tomer -\* Last modified Mon Aug 18 14:58:57 CEST 2014 by tomer -\* Last modified Tue Feb 14 13:35:49 PST 2012 by lamport \* Last modified Mon Feb 07 14:46:59 PST 2011 by lamport diff --git a/examples/ByzPaxos/VoteProof.tla b/examples/ByzPaxos/VoteProof.tla index a33bb534f..743817020 100644 --- a/examples/ByzPaxos/VoteProof.tla +++ b/examples/ByzPaxos/VoteProof.tla @@ -400,7 +400,11 @@ LEMMA SafeLemma == <3>5. QED BY <3>3, <3>4 <2>8. CASE c < cc - BY <2>8, <1>2, <2>5 + <3>1. /\ SafeAt(cc, v) + /\ c \in 0 .. cc-1 + BY <2>5, <2>8 + <3>. QED + BY <1>2, <3>1 <2>9. QED BY <2>6, <2>7, <2>8 <1>3. \A b \in Ballot : P(b) @@ -491,7 +495,11 @@ LEMMA VT0 == /\ TypeOK <3> PICK aa \in QQ \cap Q : TRUE BY QA <3>4. c \leq d - BY <3>1, <3>2, <3>3 DEF DidNotVoteIn + <4>1. CASE d = -1 + BY <3>1, <3>2, <3>3, <4>1 DEF DidNotVoteIn + <4>2. CASE d \in 0 .. (b-1) + BY <3>1, <3>2, <3>3, <4>2 DEF DidNotVoteIn + <4>. QED BY <4>1, <4>2 <3>5. CASE c = d BY <3>2, <3>3, <3>4, <3>5 <3>6. CASE d > c @@ -786,7 +794,7 @@ THEOREM InductiveInvariance == VInv /\ [Next]_vars => VInv' <7>1. CASE VotedFor(ax, cc, z) BY <6>1, <7>1 <7>2. CASE ~ VotedFor(ax, cc, z) - BY <7>2, <6>3, <5>1, <5>3 + BY <7>2, <6>3, <5>1, <5>3, cc=-1 \/ cc \in 0 .. e-1 <7>3. QED BY <7>1, <7>2 <6>4. QED @@ -1015,16 +1023,17 @@ ASSUME ValueNonempty == Value # {} LEMMA FiniteSetHasMax == ASSUME NEW S \in SUBSET Int, IsFiniteSet(S), S # {} PROVE \E max \in S : \A x \in S : max >= x -<1>. DEFINE P(T) == T \in SUBSET Int /\ T # {} => \E max \in T : \A x \in T : max >= x +<1>. DEFINE P(T) == T # {} => \E max \in T : \A x \in T : max >= x <1>1. P({}) OBVIOUS -<1>2. ASSUME NEW T, NEW x, P(T), x \notin T +<1>2. ASSUME NEW T \in SUBSET S, P(T), NEW x \in S \ T PROVE P(T \cup {x}) BY <1>2 -<1>3. \A T : IsFiniteSet(T) => P(T) +<1>3. P(S) <2>. HIDE DEF P <2>. QED BY <1>1, <1>2, FS_Induction, IsaM("blast") -<1>. QED BY <1>3, Zenon +<1>. QED BY <1>3 + ----------------------------------------------------------------------------- (***************************************************************************) @@ -1056,7 +1065,13 @@ THEOREM VT4 == TypeOK /\ VInv2 /\ VInv3 => /\ \A d \in (c+1)..(b-1), a \in Q : DidNotVoteIn(a, d) BY <1>1, <1>2, SafeAtProp <1>5. CASE \A a \in Q, c \in 0..(b-1) : DidNotVoteIn(a, c) - BY <1>5, ValueNonempty + <2>1. PICK v \in Value : TRUE + BY ValueNonempty + <2>2. /\ -1 = -1 + /\ \A d \in (-1+1) .. (b-1), a \in Q : DidNotVoteIn(a, d) + BY <1>5 + <2>. QED + BY <2>1, <2>2 <1>6. CASE \E a \in Q, c \in 0..(b-1) : ~DidNotVoteIn(a, c) <2>1. PICK c \in 0..(b-1) : /\ \E a \in Q : ~DidNotVoteIn(a, c) @@ -1069,8 +1084,16 @@ THEOREM VT4 == TypeOK /\ VInv2 /\ VInv3 => BY FS_Interval, FS_Subset, 0 \in Int, b-1 \in Int, Zenon <4>3. QED BY <3>1, <4>2, FiniteSetHasMax + <3>3. \E a \in Q : ~DidNotVoteIn(a, c) + BY <3>2 + <3>4. ASSUME NEW d \in (c+1) .. (b-1), NEW a \in Q, ~DidNotVoteIn(a,d) + PROVE FALSE + <4>1. c >= d + BY <3>2, <3>4 + <4>. QED + BY <4>1 DEF Ballot <3>. QED - BY <3>2 DEF Ballot + BY <3>3, <3>4 <2>4. PICK a0 \in Q, v \in Value : VotedFor(a0, c, v) BY <2>1 DEF DidNotVoteIn <2>5. \A a \in Q : \A w \in Value : @@ -1170,13 +1193,11 @@ LEMMA EventuallyAlwaysForall == BY <2>4, PTL <2>. QED BY <2>1, <2>2, <2>3, <2>5 -<1>. HIDE DEF Q -<1>3. \A T : IsFiniteSet(T) => Q(T) - BY <1>1, <1>2, FS_Induction, IsaM("blast") -<1>4. Q(S) - BY <1>3 -<1>. QED - BY <1>4 DEF Q +<1>3. Q(S) + <2>. HIDE DEF Q + <2>. QED BY <1>1, <1>2, FS_Induction, IsaM("blast") +<1>. QED BY <1>3 + ----------------------------------------------------------------------------- (***************************************************************************) (* Here is our proof that LiveSpec implements the specification LiveSpec *) @@ -1263,33 +1284,14 @@ THEOREM Liveness == LiveSpec => C!LiveSpec <4>5. QED BY <4>1, <4>3, <4>4 DEF BallotAction <3>3. P => ENABLED <>_vars - <4>1. (ENABLED <>_vars) <=> - \E votesp, maxBalp: - /\ \/ /\ b > maxBal[self] - /\ maxBalp = [maxBal EXCEPT ![self] = b] - /\ votesp = votes - \/ \E v \in Value : - /\ maxBal[self] \leq b - /\ DidNotVoteIn(self, b) - /\ \A p \in Acceptor \ {self} : - \A w \in Value : VotedFor(p, b, w) => (w = v) - /\ SafeAt(b, v) - /\ votesp = [votes EXCEPT ![self] = votes[self] - \cup {<>}] - /\ maxBalp = [maxBal EXCEPT ![self] = b] - /\ <> # <> -\* BY DEF BallotAction, IncreaseMaxBal, VoteFor, vars, SafeAt, -\* DidNotVoteIn, VotedFor - PROOF OMITTED - <4>. SUFFICES ASSUME P - PROVE \E votesp, maxBalp: - /\ b > maxBal[self] - /\ maxBalp = [maxBal EXCEPT ![self] = b] - /\ votesp = votes - /\ <> # <> - BY <4>1 - <4> WITNESS votes, [maxBal EXCEPT ![self] = b] - <4>. QED BY QA DEF VInv, TypeOK, Ballot + <4>1. <>_vars => <>_vars + BY DEF A, BallotAction + <4>2. (ENABLED <>_vars) => (ENABLED <>_vars) + PROOF OMITTED \* BY <4>1, ENABLEDaxioms + <4>3. TypeOK => + ((ENABLED <>_vars) <=> b > maxBal[self]) + BY ExpandENABLED, QA DEF TypeOK, IncreaseMaxBal, vars + <4>. QED BY <4>2, <4>3 DEF VInv <3>. QED BY <3>1, <3>2, <3>3, PTL <2>3. QQ /\ [][LNext]_vars => []QQ <3>1. QQ /\ [LNext]_vars => QQ' @@ -1362,29 +1364,12 @@ THEOREM Liveness == LiveSpec => C!LiveSpec <6>4. QED BY <6>1, <6>2, <6>3 DEF BallotAction <5>3. P => ENABLED <>_vars - <6>1. SUFFICES ASSUME P - PROVE ENABLED <>_vars - OBVIOUS - <6>2. (ENABLED <>_vars) <=> - \E votesp, maxBalp : - /\ \/ /\ b > maxBal[self] - /\ maxBalp = [maxBal EXCEPT ![self] = b] - /\ votesp = votes - \/ \E v \in Value : - /\ maxBal[self] \leq b - /\ DidNotVoteIn(self, b) - /\ \A p \in Acceptor \ {self} : - \A w \in Value : VotedFor(p, b, w) => (w = v) - /\ SafeAt(b, v) - /\ votesp = [votes EXCEPT ![self] = votes[self] - \cup {<>}] - /\ maxBalp = [maxBal EXCEPT ![self] = b] - /\ <> # <> -\* BY DEF BallotAction, IncreaseMaxBal, VoteFor, vars, SafeAt, -\* DidNotVoteIn, VotedFor - PROOF OMITTED - <6> SUFFICES - \E votesp, maxBalp: + <6>1. <<\E v \in Value : VoteFor(self, b, v)>>_vars => <>_vars + BY DEF BallotAction + <6>2. (ENABLED <<\E v \in Value : VoteFor(self, b, v)>>_vars) => (ENABLED <>_vars) + PROOF OMITTED \* BY <6>1, ENABLEDaxioms + <6>a. (ENABLED <<\E v \in Value : VoteFor(self, b, v)>>_vars) <=> + \E votesp, maxBalp : /\ \E v \in Value : /\ maxBal[self] \leq b /\ DidNotVoteIn(self, b) @@ -1395,7 +1380,21 @@ THEOREM Liveness == LiveSpec => C!LiveSpec \cup {<>}] /\ maxBalp = [maxBal EXCEPT ![self] = b] /\ <> # <> - BY <6>2 + BY ExpandENABLED, Isa DEF VoteFor, DidNotVoteIn, VotedFor, SafeAt, vars + <6> SUFFICES + ASSUME P + PROVE \E votesp, maxBalp : + /\ \E v \in Value : + /\ maxBal[self] \leq b + /\ DidNotVoteIn(self, b) + /\ \A p \in Acceptor \ {self} : + \A w \in Value : VotedFor(p, b, w) => (w = v) + /\ SafeAt(b, v) + /\ votesp = [votes EXCEPT ![self] = votes[self] + \cup {<>}] + /\ maxBalp = [maxBal EXCEPT ![self] = b] + /\ <> # <> + BY <6>2, <6>a <6> DEFINE someVoted == \E p \in Acceptor \ {self} : \E w \in Value : VotedFor(p, b, w) vp == CHOOSE p \in Acceptor \ {self} : @@ -1488,8 +1487,6 @@ THEOREM Liveness == LiveSpec => C!LiveSpec =============================================================================== \* Modification History -\* Last modified Fri Jul 24 18:20:31 CEST 2020 by merz -\* Last modified Wed Apr 29 12:24:23 CEST 2020 by merz \* Last modified Mon May 28 08:53:38 PDT 2012 by lamport diff --git a/examples/Dekker/Dekker.tla b/examples/Dekker/Dekker.tla index 4bfca3fda..d1702dabe 100644 --- a/examples/Dekker/Dekker.tla +++ b/examples/Dekker/Dekker.tla @@ -207,8 +207,23 @@ PROOF BY <2>1, <2>2, PTL DEF Sys <1>2. ASSUME IndInv PROVE Enabledness - BY <1>2, ExpandENABLED DEF IndInv, Enabledness, - Next, Next1, Next2, vars + <2>1. CASE pc1 # 5 \/ turn # 2 + <3>1. Next1 /\ UNCHANGED <> => <>_vars + BY <2>1 DEF Next, Next1, Next2, vars + <3>2. (ENABLED (Next1 /\ UNCHANGED <>)) => (ENABLED <>_vars) + OMITTED \* BY <3>1, ENABLEDaxioms + <3>3. ENABLED (Next1 /\ UNCHANGED <>) + BY <1>2, ExpandENABLED DEF Next1, IndInv + <3>. QED BY <3>2, <3>3 DEF Enabledness + <2>2. CASE pc2 # 5 \/ turn # 1 + <3>1. Next2 /\ UNCHANGED <> => <>_vars + BY <2>2 DEF Next, Next1, Next2, vars + <3>2. (ENABLED (Next2 /\ UNCHANGED <>)) => (ENABLED <>_vars) + OMITTED \* BY <3>1, ENABLEDaxioms + <3>3. ENABLED (Next2 /\ UNCHANGED <>) + BY <1>2, ExpandENABLED DEF Next2, IndInv + <3>. QED BY <3>2, <3>3 DEF Enabledness + <2>. QED BY <2>1, <2>2 <1> QED BY <1>1, <1>2, PTL diff --git a/examples/EWD840.tla b/examples/EWD840.tla index 8647e3acd..0f843f576 100644 --- a/examples/EWD840.tla +++ b/examples/EWD840.tla @@ -135,33 +135,7 @@ LEMMA TypeOK_inv == Spec => []TypeOK <1>1. Init => TypeOK BY DEF Init <1>2. TypeOK /\ [Next]_vars => TypeOK' -(* FIXME: Although each of the steps below is proved instantly, - the attempt to prove the assertion all at once fails?? - BY NAssumption DEF Next, vars, TypeOK, Nodes, Color, Controlled, Environment, - InitiateProbe, PassToken, SendMsg, Deactivate -*) - <2> SUFFICES ASSUME TypeOK, - [Next]_vars - PROVE TypeOK' - OBVIOUS - <2>1. CASE InitiateProbe - BY <2>1 DEF InitiateProbe - <2>2. ASSUME NEW i \in Nodes \ {0}, - PassToken(i) - PROVE TypeOK' - BY <2>2 DEF PassToken - <2>3. ASSUME NEW i \in Nodes, - Deactivate(i) - PROVE TypeOK' - BY <2>3 DEF Deactivate - <2>4. ASSUME NEW i \in Nodes, - SendMsg(i) - PROVE TypeOK' - BY <2>4 DEF SendMsg - <2>5. CASE UNCHANGED vars - BY <2>5 DEF vars - <2>6. QED - BY <2>1, <2>2, <2>3, <2>4, <2>5 DEF Controlled, Environment, Next + BY DEFS Next, vars, InitiateProbe, PassToken, Deactivate, SendMsg, Controlled, Environment <1>3. QED BY <1>1, <1>2, PTL DEF Spec @@ -222,7 +196,4 @@ LEMMA Inv_implies_Termination == Inv => TerminationDetection ============================================================================= \* Modification History -\* Last modified Wed Jan 08 15:06:01 CET 2020 by merz -\* Last modified Fri May 30 23:04:12 CEST 2014 by shaolin -\* Last modified Wed May 21 11:36:56 CEST 2014 by jael \* Created Mon Sep 09 11:33:10 CEST 2013 by merz diff --git a/examples/GraphTheorem.tla b/examples/GraphTheorem.tla index 4dda43238..b636d4a5d 100644 --- a/examples/GraphTheorem.tla +++ b/examples/GraphTheorem.tla @@ -1,5 +1,5 @@ ---------------------------- MODULE GraphTheorem ---------------------------- -EXTENDS FiniteSetTheorems, FunctionTheorems, TLAPS +EXTENDS FiniteSetTheorems, FunctionForkTheorems, TLAPS Edges(Nodes) == { {m[1], m[2]} : m \in Nodes \X Nodes } (*************************************************************************) @@ -10,11 +10,17 @@ Edges(Nodes) == { {m[1], m[2]} : m \in Nodes \X Nodes } (* However, this construct isn't supported by TLAPS yet. *) (*************************************************************************) -LEMMA EdgesAxiom == \A Nodes : - /\ \A m, n \in Nodes : {m, n} \in Edges(Nodes) - /\ \A e \in Edges(Nodes) : - \E m, n \in Nodes : e = {m, n} -BY IsaM("force") DEF Edges +LEMMA EdgesAxiom == + ASSUME NEW Nodes + PROVE /\ \A m, n \in Nodes : {m, n} \in Edges(Nodes) + /\ \A e \in Edges(Nodes) : \E m, n \in Nodes : e = {m, n} +<1>1. ASSUME NEW m \in Nodes, NEW n \in Nodes + PROVE {m, n} \in Edges(Nodes) + BY DEF Edges +<1>2. ASSUME NEW e \in Edges(Nodes) + PROVE \E m,n \in Nodes : e = {m,n} + BY DEF Edges +<1>. QED BY <1>1, <1>2 ------------------------------------------------------- LEMMA EdgesFinite == @@ -39,7 +45,7 @@ LEMMA NLEdgeElements == <1>. SUFFICES ASSUME m = n PROVE FALSE OBVIOUS <1>. QED - BY FS_Singleton, Isa DEF NonLoopEdges + BY FS_Singleton DEF NonLoopEdges ------------------------------------------------------------------ (***************************************************************************) @@ -97,10 +103,16 @@ THEOREM <3>1. IsFiniteSet(Isolated) /\ Cardinality(Isolated) \in Nat BY FS_Subset, FS_CardinalityType <3>2. CASE Cardinality(Isolated) > 1 - <4>1. PICK x \in Isolated, y \in Isolated : x # y - BY <3>1, <3>2, FS_CardinalityType, CVC4 DEF ExistsBijection, Bijection, Injection + <4>1. PICK x \in Isolated : TRUE + BY <3>1, <3>2, FS_EmptySet + <4>. DEFINE IX == Isolated \ {x} + <4>2. /\ IsFiniteSet(IX) + /\ Cardinality(IX) > 0 + BY <3>1, <3>2, FS_RemoveElement + <4>3. PICK y \in IX : TRUE + BY <4>2, FS_EmptySet <4>. QED - BY <1>3, <4>1 + BY <1>3, <4>3 <3>3. QED BY <3>1, <3>2 <2>4. Cardinality(Connected) \geq 1 @@ -125,7 +137,9 @@ THEOREM <3>2. ASSUME NEW e \in G, NEW n \in e PROVE \E m \in Connected : n # m /\ e = {m, n} - BY <2>5, NLEdgeElements DEF SimpleGraphs + <4>. PICK m, n \in Nodes : m # n /\ e = {m,n} + BY NLEdgeElements DEF SimpleGraphs + <4>. QED BY <2>5 <3>3. SUFFICES ASSUME NEW n \in Connected PROVE Cardinality({e \in G : n \in e}) < Cardinality(Connected) BY <3>1, <3>3 DEF Degree diff --git a/examples/LamportMutex.tla b/examples/LamportMutex.tla deleted file mode 100644 index 7a3ea49cb..000000000 --- a/examples/LamportMutex.tla +++ /dev/null @@ -1,944 +0,0 @@ ---------------------------- MODULE LamportMutex ---------------------------- -(***************************************************************************) -(* TLA+ specification and proof of Lamport's distributed mutual-exclusion *) -(* algorithm that appeared as an example in *) -(* L. Lamport: Time, Clocks and the Ordering of Events in a Distributed *) -(* System. CACM 21(7):558-565, 1978. *) -(***************************************************************************) -EXTENDS Naturals, SequenceTheorems, TLAPS - -(***************************************************************************) -(* The parameter N represents the number of processes. *) -(* The parameter maxClock is used only for model checking in order to *) -(* keep the state space finite. *) -(***************************************************************************) -CONSTANT N, maxClock - -ASSUME NType == N \in Nat -ASSUME maxClockType == maxClock \in Nat - -Proc == 1 .. N -Clock == Nat \ {0} -USE DEF Clock -(***************************************************************************) -(* For model checking, add ClockConstraint as a state constraint to ensure *) -(* a finite state space and override the definition of Clock by *) -(* 1 .. maxClock+1 so that TLC can evaluate the definition of Message. *) -(***************************************************************************) - -VARIABLES - clock, \* local clock of each process - req, \* requests received from processes (clock transmitted with request) - ack, \* acknowledgements received from processes - network, \* messages sent but not yet received - crit \* set of processes in critical section - -(***************************************************************************) -(* Messages used in the algorithm. *) -(***************************************************************************) -ReqMessage(c) == [type |-> "req", clock |-> c] -AckMessage == [type |-> "ack", clock |-> 0] -RelMessage == [type |-> "rel", clock |-> 0] - -Message == {AckMessage, RelMessage} \union {ReqMessage(c) : c \in Clock} - -(***************************************************************************) -(* The type correctness predicate. *) -(***************************************************************************) -TypeOK == - (* clock[p] is the local clock of process p *) - /\ clock \in [Proc -> Clock] - (* req[p][q] stores the clock associated with request from q received by p, 0 if none *) - /\ req \in [Proc -> [Proc -> Nat]] - (* ack[p] stores the processes that have ack'ed p's request *) - /\ ack \in [Proc -> SUBSET Proc] - (* network[p][q]: queue of messages from p to q -- pairwise FIFO communication *) - /\ network \in [Proc -> [Proc -> Seq(Message)]] - (* set of processes in critical section: should be empty or singleton *) - /\ crit \in SUBSET Proc - - -(***************************************************************************) -(* The initial state predicate. *) -(***************************************************************************) - -Init == - /\ clock = [p \in Proc |-> 1] - /\ req = [p \in Proc |-> [q \in Proc |-> 0]] - /\ ack = [p \in Proc |-> {}] - /\ network = [p \in Proc |-> [q \in Proc |-> <<>> ]] - /\ crit = {} - - -(***************************************************************************) -(* beats(p,q) is true if process p believes that its request has higher *) -(* priority than q's request. This is true if either p has not received a *) -(* request from q or p's request has a smaller clock value than q's. *) -(* If there is a tie, the numerical process ID decides. *) -(***************************************************************************) -beats(p,q) == - \/ req[p][q] = 0 - \/ req[p][p] < req[p][q] - \/ req[p][p] = req[p][q] /\ p < q - -(***************************************************************************) -(* Broadcast a message: send it to all processes except the sender. *) -(***************************************************************************) -Broadcast(s, m) == - [r \in Proc |-> IF s=r THEN network[s][r] ELSE Append(network[s][r], m)] - -(***************************************************************************) -(* Process p requests access to critical section. *) -(***************************************************************************) -Request(p) == - /\ req[p][p] = 0 - /\ req'= [req EXCEPT ![p][p] = clock[p]] - /\ network' = [network EXCEPT ![p] = Broadcast(p, ReqMessage(clock[p]))] - /\ ack' = [ack EXCEPT ![p] = {p}] - /\ UNCHANGED <> - -(***************************************************************************) -(* Process p receives a request from q and acknowledges it. *) -(***************************************************************************) -ReceiveRequest(p,q) == - /\ network[q][p] # << >> - /\ LET m == Head(network[q][p]) - c == m.clock - IN /\ m.type = "req" - /\ req' = [req EXCEPT ![p][q] = c] - /\ clock' = [clock EXCEPT ![p] = IF c > clock[p] THEN c + 1 ELSE @ + 1] - /\ network' = [a \in Proc |-> [b \in Proc |-> - IF a=q /\ b=p THEN Tail(network[q][p]) - ELSE IF a=p /\ b=q THEN Append(network[p][q], AckMessage) - ELSE network[a][b]]] -(* - /\ network' = [network EXCEPT ![q][p] = Tail(@), - ![p][q] = Append(@, AckMessage)] -*) - /\ UNCHANGED <> - -(***************************************************************************) -(* Process p receives an acknowledgement from q. *) -(***************************************************************************) -ReceiveAck(p,q) == - /\ network[q][p] # << >> - /\ LET m == Head(network[q][p]) - IN /\ m.type = "ack" - /\ ack' = [ack EXCEPT ![p] = @ \union {q}] - /\ network' = [network EXCEPT ![q][p] = Tail(@)] - /\ UNCHANGED <> - -(**************************************************************************) -(* Process p enters the critical section. *) -(**************************************************************************) -Enter(p) == - /\ ack[p] = Proc - /\ \A q \in Proc \ {p} : beats(p,q) - /\ crit' = crit \union {p} - /\ UNCHANGED <> - -(***************************************************************************) -(* Process p exits the critical section and notifies other processes. *) -(***************************************************************************) -Exit(p) == - /\ p \in crit - /\ crit' = crit \ {p} - /\ network' = [network EXCEPT ![p] = Broadcast(p, RelMessage)] - /\ req' = [req EXCEPT ![p][p] = 0] - /\ ack' = [ack EXCEPT ![p] = {}] - /\ UNCHANGED clock - -(***************************************************************************) -(* Process p receives a release notification from q. *) -(***************************************************************************) -ReceiveRelease(p,q) == - /\ network[q][p] # << >> - /\ LET m == Head(network[q][p]) - IN /\ m.type = "rel" - /\ req' = [req EXCEPT ![p][q] = 0] - /\ network' = [network EXCEPT ![q][p] = Tail(@)] - /\ UNCHANGED <> - -(***************************************************************************) -(* Next-state relation. *) -(***************************************************************************) - -Next == - \/ \E p \in Proc : Request(p) \/ Enter(p) \/ Exit(p) - \/ \E p \in Proc : \E q \in Proc \ {p} : - ReceiveRequest(p,q) \/ ReceiveAck(p,q) \/ ReceiveRelease(p,q) - -vars == <> - -Spec == Init /\ [][Next]_vars - ------------------------------------------------------------------------------ -(***************************************************************************) -(* A state constraint that is useful for validating the specification *) -(* using finite-state model checking. *) -(***************************************************************************) -ClockConstraint == \A p \in Proc : clock[p] <= maxClock - -(***************************************************************************) -(* No channel ever contains more than three messages. In fact, no channel *) -(* ever contains more than one message of the same type, as proved below. *) -(***************************************************************************) -BoundedNetwork == \A p,q \in Proc : Len(network[p][q]) <= 3 - -(***************************************************************************) -(* The main safety property of mutual exclusion. *) -(***************************************************************************) -Mutex == \A p,q \in crit : p = q - ------------------------------------------------------------------------------ -(***************************************************************************) -(* Proof of type correctness. *) -(***************************************************************************) -LEMMA BroadcastType == - ASSUME network \in [Proc -> [Proc -> Seq(Message)]], - NEW s \in Proc, NEW m \in Message - PROVE Broadcast(s,m) \in [Proc -> Seq(Message)] -BY AppendProperties DEF Broadcast - -LEMMA TypeCorrect == Spec => []TypeOK -<1>1. Init => TypeOK - BY DEF Init, TypeOK -<1>2. TypeOK /\ [Next]_vars => TypeOK' - <2> SUFFICES ASSUME TypeOK, - [Next]_vars - PROVE TypeOK' - OBVIOUS - <2>. USE DEF TypeOK, Message - <2>1. ASSUME NEW p \in Proc, - Request(p) - PROVE TypeOK' - BY <2>1, BroadcastType, Zenon DEF Request - <2>2. ASSUME NEW p \in Proc, - Enter(p) - PROVE TypeOK' - BY <2>2 DEF Enter - <2>3. ASSUME NEW p \in Proc, - Exit(p) - PROVE TypeOK' - BY <2>3, BroadcastType, Zenon DEF Exit - <2>4. ASSUME NEW p \in Proc, - NEW q \in Proc \ {p}, - ReceiveRequest(p,q) - PROVE TypeOK' - <3>1. /\ network[q][p] \in Seq(Message) \ { << >> } - /\ Head(network[q][p]) \in Message - /\ Tail(network[q][p]) \in Seq(Message) - /\ Head(network[q][p]) \in {ReqMessage(c) : c \in Clock} - /\ Head(network[q][p]).clock \in Clock - /\ clock[p]+1 \in Clock - /\ Append(network[p][q], AckMessage) \in Seq(Message) - /\ UNCHANGED <> - BY <2>4, HeadTailProperties DEF ReceiveRequest, AckMessage, RelMessage, ReqMessage - <3>2. clock' \in [Proc -> Clock] - BY <2>4, <3>1 DEF ReceiveRequest - <3>3. req' \in [Proc -> [Proc -> Nat]] - BY <2>4, <3>1 DEF ReceiveRequest - <3>4. network' \in [Proc -> [Proc -> Seq(Message)]] - BY <3>1, <2>4, Zenon DEF ReceiveRequest - <3>. QED BY <3>1, <3>2, <3>3, <3>4 - <2>5. ASSUME NEW p \in Proc, - NEW q \in Proc \ {p}, - ReceiveAck(p,q) - PROVE TypeOK' - <3>. HIDE DEF Message - <3>. QED BY <2>5 DEF ReceiveAck - <2>6. ASSUME NEW p \in Proc, - NEW q \in Proc \ {p}, - ReceiveRelease(p,q) - PROVE TypeOK' - BY <2>6, CVC4 DEF ReceiveRelease - <2>7. CASE UNCHANGED vars - BY <2>7 DEF vars - <2>8. QED BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7 DEF Next -<1>. QED BY <1>1, <1>2, PTL DEF Spec - ------------------------------------------------------------------------------ -(***************************************************************************) -(* Inductive invariants for the algorithm. *) -(***************************************************************************) - -(***************************************************************************) -(* We start the proof of safety by defining some auxiliary predicates: *) -(* - Contains(s,mt) holds if channel s contains a message of type mt. *) -(* - AtMostOne(s,mt) holds if channel s holds zero or one messages of *) -(* type mtype. *) -(* - Precedes(s,mt1,mt2) holds if in channel s, any message of type mt1 *) -(* precedes any message of type mt2. *) -(***************************************************************************) -Contains(s,mtype) == \E i \in 1 .. Len(s) : s[i].type = mtype -AtMostOne(s,mtype) == \A i,j \in 1 .. Len(s) : - s[i].type = mtype /\ s[j].type = mtype => i = j -Precedes(s,mt1,mt2) == \A i,j \in 1 .. Len(s) : - s[i].type = mt1 /\ s[j].type = mt2 => i < j - -LEMMA NotContainsAtMostOne == - ASSUME NEW s \in Seq(Message), NEW mtype, ~ Contains(s,mtype) - PROVE AtMostOne(s, mtype) -BY DEF Contains, AtMostOne - -LEMMA NotContainsPrecedes == - ASSUME NEW s \in Seq(Message), NEW mt1, NEW mt2, ~ Contains(s, mt2) - PROVE /\ Precedes(s, mt1, mt2) - /\ Precedes(s, mt2, mt1) -BY DEF Contains, Precedes - -LEMMA PrecedesHead == - ASSUME NEW s \in Seq(Message), NEW mt1, NEW mt2, - s # << >>, - Precedes(s,mt1,mt2), Head(s).type = mt2 - PROVE ~ Contains(s,mt1) -BY DEF Precedes, Contains - -LEMMA AtMostOneTail == - ASSUME NEW s \in Seq(Message), NEW mtype, - s # << >>, AtMostOne(s, mtype) - PROVE AtMostOne(Tail(s), mtype) -BY DEF AtMostOne - -LEMMA ContainsTail == - ASSUME NEW s \in Seq(Message), s # << >>, - NEW mtype, AtMostOne(s, mtype) - PROVE Contains(Tail(s), mtype) <=> Contains(s, mtype) /\ Head(s).type # mtype -BY DEF Contains, AtMostOne - -LEMMA AtMostOneHead == - ASSUME NEW s \in Seq(Message), NEW mtype, - AtMostOne(s,mtype), s # << >>, Head(s).type = mtype - PROVE ~ Contains(Tail(s), mtype) -<1>. SUFFICES ASSUME NEW i \in 1 .. Len(Tail(s)), Tail(s)[i].type = mtype - PROVE FALSE - BY Tail(s) \in Seq(Message), Isa DEF Contains -<1>. QED BY HeadTailProperties DEF AtMostOne - -LEMMA ContainsSend == - ASSUME NEW s \in Seq(Message), NEW mtype, NEW m \in Message - PROVE Contains(Append(s,m), mtype) <=> m.type = mtype \/ Contains(s, mtype) -BY DEF Contains - -LEMMA NotContainsSend == - ASSUME NEW s \in Seq(Message), NEW mtype, ~ Contains(s, mtype), NEW m \in Message - PROVE /\ AtMostOne(Append(s,m), mtype) - /\ m.type # mtype => ~ Contains(Append(s,m), mtype) -BY DEF Contains, AtMostOne - -LEMMA AtMostOneSend == - ASSUME NEW s \in Seq(Message), NEW mtype, AtMostOne(s, mtype), - NEW m \in Message, m.type # mtype - PROVE AtMostOne(Append(s,m), mtype) -BY DEF AtMostOne - -LEMMA PrecedesSend == - ASSUME NEW s \in Seq(Message), NEW mt1, NEW mt2, - NEW m \in Message, m.type # mt1 - PROVE Precedes(Append(s,m), mt1, mt2) <=> Precedes(s, mt1, mt2) -BY DEF Precedes - -LEMMA PrecedesTail == - ASSUME NEW s \in Seq(Message), NEW mt1, NEW mt2, Precedes(s, mt1, mt2) - PROVE Precedes(Tail(s), mt1, mt2) -BY DEF Precedes - -LEMMA PrecedesInTail == - ASSUME NEW s \in Seq(Message), s # << >>, - NEW mt1, NEW mt2, mt1 # mt2, - Head(s).type = mt1 \/ Head(s).type \notin {mt1, mt2}, - Precedes(Tail(s), mt1, mt2) - PROVE Precedes(s, mt1, mt2) -BY DEF Precedes - ------------------------------------------------------------------------------ -(***************************************************************************) -(* In order to prove the safety property of the algorithm, we prove two *) -(* inductive invariants. Our first invariant is itself a conjunction of *) -(* two predicates: *) -(* - The first one states that each channel holds at most one message of *) -(* each type. Moreover, no process ever sends a message to itself. *) -(* - The second predicate describes how request, acknowledgement, and *) -(* release messages are exchanged among processes, but does not refer to *) -(* clock values held in the clock and req variables. *) -(***************************************************************************) - -NetworkInv(p,q) == - LET s == network[p][q] - IN /\ AtMostOne(s,"req") - /\ AtMostOne(s,"ack") - /\ AtMostOne(s,"rel") - /\ network[p][p] = << >> - -CommInv(p) == - \/ /\ req[p][p] = 0 /\ ack[p] = {} /\ p \notin crit - /\ \A q \in Proc : ~ Contains(network[p][q],"req") /\ ~ Contains(network[q][p],"ack") - \/ /\ req[p][p] > 0 /\ p \in ack[p] - /\ p \in crit => ack[p] = Proc - /\ \A q \in Proc : - LET pq == network[p][q] - qp == network[q][p] - IN \/ /\ q \in ack[p] - /\ ~ Contains(pq,"req") /\ ~ Contains(qp,"ack") /\ ~ Contains(pq,"rel") - \/ /\ q \notin ack[p] /\ Contains(qp,"ack") - /\ ~ Contains(pq,"req") /\ ~ Contains(pq,"rel") - \/ /\ q \notin ack[p] /\ Contains(pq,"req") - /\ ~ Contains(qp,"ack") /\ Precedes(pq,"rel","req") - -BasicInv == - /\ \A p,q \in Proc : NetworkInv(p,q) - /\ \A p \in Proc : CommInv(p) - -THEOREM BasicInvariant == Spec => []BasicInv -<1>1. Init => BasicInv - BY DEF Init, BasicInv, CommInv, NetworkInv, Contains, AtMostOne -<1>2. TypeOK /\ BasicInv /\ [Next]_vars => BasicInv' - <2> SUFFICES ASSUME TypeOK, BasicInv, [Next]_vars - PROVE BasicInv' - OBVIOUS - <2>. USE DEF TypeOK - <2>1. ASSUME NEW n \in Proc, Request(n) - PROVE BasicInv' - <3>1. /\ req[n][n] = 0 - /\ req' = [req EXCEPT ![n][n] = clock[n]] - /\ network' = [network EXCEPT ![n] = Broadcast(n, ReqMessage(clock[n]))] - /\ ack' = [ack EXCEPT ![n] = {n}] - /\ crit' = crit - BY <2>1 DEF Request - <3>. /\ ReqMessage(clock[n]) \in Message - /\ ReqMessage(clock[n]).type = "req" - BY DEF ReqMessage, Message - <3>2. /\ n \notin crit - /\ \A q \in Proc : ~ Contains(network[n][q], "req") /\ ~ Contains(network[q][n], "ack") - BY <3>1, ~(req[n][n] > 0), Zenon DEF BasicInv, CommInv - <3>3. ASSUME NEW p \in Proc, NEW q \in Proc - PROVE NetworkInv(p,q)' - BY <3>1, <3>2, <3>3, NotContainsSend, AtMostOneSend DEF Broadcast, BasicInv, NetworkInv - <3>4. ASSUME NEW p \in Proc - PROVE CommInv(p)' - <4>1. CASE p = n - <5>. /\ req'[p][p] > 0 /\ p \in ack'[p] - /\ p \notin crit' - BY <3>1, <3>2, <4>1 - <5>. /\ ~ Contains(network'[p][n], "req") - /\ ~ Contains(network'[n][p], "ack") - /\ ~ Contains(network'[p][n], "rel") - BY <3>3, <4>1 DEF NetworkInv, Contains - <5>. ASSUME NEW q \in Proc \ {n} - PROVE /\ q \notin ack'[p] - /\ Contains(network'[p][q], "req") - /\ ~ Contains(network'[q][p], "ack") - /\ Precedes(network'[p][q], "rel", "req") - BY <3>1, <3>2, <4>1, ContainsSend, NotContainsPrecedes, PrecedesSend, CVC4 - DEF Broadcast - <5>. QED BY DEF CommInv - <4>2. CASE p # n - <5>. CommInv(p) - BY DEF BasicInv - <5>. UNCHANGED << req[p][p], ack[p], crit >> - BY <3>1, <4>2 - <5>. \A q \in Proc : UNCHANGED network[p][q] - BY <3>1, <4>2 - <5>. /\ \A q \in Proc \ {n} : UNCHANGED network[q][p] - /\ p = n => UNCHANGED network[n][p] - BY <3>1, <4>2 DEF Broadcast - <5>. n # p => Contains(network'[n][p], "ack") <=> Contains(network[n][p], "ack") - BY <3>1, <4>2, ContainsSend DEF Broadcast - <5>. QED BY Zenon DEF CommInv - <4>. QED BY <4>1, <4>2 - <3>. QED BY <3>3, <3>4 DEF BasicInv - <2>2. ASSUME NEW n \in Proc, Enter(n) - PROVE BasicInv' - BY <2>2 DEF Enter, BasicInv, NetworkInv, CommInv - <2>3. ASSUME NEW n \in Proc, Exit(n) - PROVE BasicInv' - <3>1. /\ req[n][n] > 0 - /\ ack[n] = Proc - /\ \A q \in Proc : /\ ~ Contains(network[n][q], "req") - /\ ~ Contains(network[q][n], "ack") - /\ ~ Contains(network[n][q], "rel") - /\ network' = [network EXCEPT ![n] = - [q \in Proc |-> IF n=q THEN network[n][q] ELSE Append(network[n][q], RelMessage)]] - /\ crit' = crit \ {n} - /\ req' = [req EXCEPT ![n][n] = 0] - /\ ack' = [ack EXCEPT ![n] = {}] - /\ clock' = clock - BY <2>3 DEF Exit, Broadcast, BasicInv, CommInv - <3>. /\ RelMessage \in Message - /\ RelMessage.type = "rel" - BY DEF RelMessage, Message - <3>2. ASSUME NEW p \in Proc, NEW q \in Proc - PROVE NetworkInv(p,q)' - <4>1. CASE p = n - <5>. /\ AtMostOne(network'[p][q], "req") - /\ AtMostOne(network'[p][q], "rel") - BY <3>1, <4>1, NotContainsAtMostOne, NotContainsSend - <5>. AtMostOne(network[p][q], "ack") - BY DEF BasicInv, NetworkInv - <5>. AtMostOne(network'[p][q], "ack") - BY <3>1, <4>1, AtMostOneSend - <5>. network'[p][p] = << >> - BY <3>1, <4>1 DEF BasicInv, NetworkInv - <5>. QED BY DEF NetworkInv - <4>2. CASE p # n - <5>. /\ network'[p][p] = network[p][p] - /\ network'[p][q] = network[p][q] - BY <3>1, <4>2 - <5>. QED BY DEF BasicInv, NetworkInv - <4>. QED BY <4>1, <4>2 - <3>3. ASSUME NEW p \in Proc - PROVE CommInv(p)' - <4>1. CASE p = n - BY <3>1, <4>1, NotContainsSend DEF CommInv - <4>2. CASE p # n - <5>. /\ req'[p][p] = req[p][p] - /\ ack'[p] = ack[p] - /\ (p \in crit') <=> (p \in crit) - /\ \A q \in Proc : network'[p][q] = network[p][q] - BY <3>1, <4>2 - <5>. ASSUME NEW q \in Proc - PROVE Contains(network'[q][p], "ack") <=> Contains(network[q][p], "ack") - <6>1. CASE n = q - <7>. network'[q][p] = Append(network[q][p], RelMessage) - BY <3>1, <4>2, <6>1 - <7>. QED BY ContainsSend - <6>2. CASE n # q - BY <3>1, <6>2 - <6>. QED BY <6>1, <6>2 - <5>. QED BY DEF BasicInv, CommInv - <4>. QED BY <4>1, <4>2 - <3>. QED BY <3>2, <3>3 DEF BasicInv - <2>4. ASSUME NEW n \in Proc, NEW k \in Proc \ {n}, ReceiveRequest(n,k) - PROVE BasicInv' - <3>1. /\ network[k][n] # << >> - /\ LET m == Head(network[k][n]) - IN /\ m.type = "req" - /\ \A p \in Proc : req'[p][p] = req[p][p] - /\ network' = [p \in Proc |-> [q \in Proc |-> - IF p=k /\ q=n THEN Tail(network[k][n]) - ELSE IF p=n /\ q=k THEN Append(network[n][k], AckMessage) - ELSE network[p][q]]] - /\ UNCHANGED <> - BY <2>4 DEF ReceiveRequest - <3>2. Contains(network[k][n], "req") - BY <3>1 DEF Contains - <3>3. /\ req[k][k] > 0 /\ k \in ack[k] - /\ k \in crit => ack[k] = Proc - /\ n \notin ack[k] - /\ ~ Contains(network[n][k], "ack") /\ ~ Contains(network[k][n], "rel") - BY <3>1, <3>2, PrecedesHead DEF BasicInv, CommInv - <3>. /\ AckMessage \in Message - /\ AckMessage.type = "ack" - BY DEF AckMessage, Message - <3>4. ASSUME NEW p \in Proc, NEW q \in Proc - PROVE NetworkInv(p,q)' - BY <3>1, <3>3, AtMostOneTail, AtMostOneSend, NotContainsSend DEF BasicInv, NetworkInv - <3>5. ASSUME NEW p \in Proc - PROVE CommInv(p)' - <4>1. CASE p = k - <5>. SUFFICES ASSUME NEW q \in Proc - PROVE CommInv(p)!2!3!(q)' - BY <3>1, <3>3, <4>1 DEF CommInv - <5>. DEFINE pq == network[p][q] - qp == network[q][p] - <5>1. CASE q = n - <6>. q \notin ack'[p] - BY <3>1, <3>3, <4>1, <5>1 - <6>. /\ pq # << >> /\ pq' = Tail(pq) - /\ qp' = Append(qp, AckMessage) - /\ AtMostOne(pq, "req") /\ Head(pq).type = "req" - /\ ~ Contains(pq, "rel") - BY <3>1, <3>3, <4>1, <5>1 DEF BasicInv, NetworkInv - <6>. /\ Contains(qp', "ack") - /\ ~ Contains(pq', "req") - /\ ~ Contains(pq', "rel") - BY ContainsSend, AtMostOneHead, ContainsTail DEF BasicInv, NetworkInv - <6>. QED OBVIOUS - <5>2. CASE q # n - <6>. pq' = pq /\ qp' = qp /\ ack'[p] = ack[p] - BY <3>1, <3>3, <4>1, <5>2 - <6>. CommInv(p)!2!3!(q) - BY <3>3, <4>1, Zenon DEF BasicInv, CommInv - <6>. QED OBVIOUS - <5>. QED BY <5>1, <5>2 - <4>2. CASE p = n - <5>. UNCHANGED << req[p][p], ack[p], crit >> BY <3>1 - <5>. ASSUME NEW q \in Proc - PROVE /\ Contains(network'[p][q], "req") <=> Contains(network[p][q], "req") - /\ Contains(network'[p][q], "rel") <=> Contains(network[p][q], "rel") - /\ Contains(network'[q][p], "ack") <=> Contains(network[q][p], "ack") - /\ Precedes(network'[p][q], "rel", "req") <=> Precedes(network[p][q], "rel", "req") - <6>1. CASE q = k - <7>. /\ network'[p][q] = Append(network[p][q], AckMessage) - /\ network[q][p] # << >> /\ Head(network[q][p]).type = "req" - /\ network'[q][p] = Tail(network[q][p]) - BY <3>1, <4>2, <6>1 - <7>. QED BY ContainsSend, ContainsTail, PrecedesSend DEF BasicInv, NetworkInv - <6>2. CASE q # k - BY <3>1, <4>2, <6>2 - <6>. QED BY <6>1, <6>2 - <5>. QED BY DEF BasicInv, CommInv - <4>3. CASE p \notin {k,n} \* all relevant variables are unchanged - BY <3>1, <4>3 DEF BasicInv, CommInv - <4>. QED BY <4>1, <4>2, <4>3 - <3>. QED BY <3>4, <3>5 DEF BasicInv - <2>5. ASSUME NEW n \in Proc, NEW k \in Proc \ {n}, ReceiveAck(n,k) - PROVE BasicInv' - <3>1. /\ network[k][n] # << >> - /\ Head(network[k][n]).type = "ack" - /\ ack' = [ack EXCEPT ![n] = @ \union {k}] - /\ network' = [network EXCEPT ![k][n] = Tail(@)] - /\ UNCHANGED <> - BY <2>5 DEF ReceiveAck - <3>2. Contains(network[k][n], "ack") - BY <3>1 DEF Contains - <3>3. /\ req[n][n] > 0 /\ n \in ack[n] - /\ n \in crit => ack[n] = Proc - /\ k \notin ack[n] - /\ ~ Contains(network[n][k], "req") /\ ~ Contains(network[n][k], "rel") - BY <3>2 DEF BasicInv, CommInv - <3>4. ASSUME NEW p \in Proc, NEW q \in Proc - PROVE NetworkInv(p,q)' - BY <3>1, AtMostOneTail DEF BasicInv, NetworkInv - <3>5. ASSUME NEW p \in Proc - PROVE CommInv(p)' - <4>1. CASE p = n - <5>. SUFFICES ASSUME NEW q \in Proc, CommInv(p)!2!3!(q) - PROVE CommInv(p)!2!3!(q)' - BY <3>1, <3>3, <4>1, CVC4 DEF BasicInv, CommInv - <5>1. CASE q = k - <6>. /\ q \in ack'[p] - /\ ~ Contains(network'[p][q], "req") - /\ ~ Contains(network'[q][p], "ack") - /\ ~ Contains(network'[p][q], "rel") - BY <3>1, <3>3, <4>1, <5>1, AtMostOneHead, CVC4 DEF BasicInv, NetworkInv - <6>. QED OBVIOUS - <5>2. CASE q # k - BY <3>1, <3>3, <4>1, <5>2 - <5>. QED BY <5>1, <5>2 - <4>2. CASE p = k - <5>. ASSUME NEW q \in Proc - PROVE /\ Contains(network'[p][q], "req") <=> Contains(network[p][q], "req") - /\ Contains(network'[p][q], "rel") <=> Contains(network[p][q], "rel") - /\ Precedes(network[p][q], "rel", "req") => Precedes(network'[p][q], "rel", "req") - BY <3>1, <4>2, ContainsTail, PrecedesTail DEF BasicInv, NetworkInv - <5>. QED BY <3>1, <4>2 DEF BasicInv, CommInv - <4>3. CASE p \notin {n,k} - BY <3>1, <4>3 DEF BasicInv, CommInv - <4>. QED BY <4>1, <4>2, <4>3 - <3>. QED BY <3>4, <3>5 DEF BasicInv - <2>6. ASSUME NEW n \in Proc, NEW k \in Proc \ {n}, ReceiveRelease(n,k) - PROVE BasicInv' - <3>1. /\ network[k][n] # << >> - /\ Head(network[k][n]).type = "rel" - /\ req' = [req EXCEPT ![n][k] = 0] - /\ network' = [network EXCEPT ![k][n] = Tail(@)] - /\ UNCHANGED <> - BY <2>6 DEF ReceiveRelease - <3>2. ASSUME NEW p \in Proc, NEW q \in Proc - PROVE NetworkInv(p,q)' - BY <3>1, AtMostOneTail DEF BasicInv, NetworkInv - <3>3. ASSUME NEW p \in Proc, CommInv(p) - PROVE CommInv(p)' - <4>. ASSUME NEW q \in Proc - PROVE /\ Contains(network'[p][q], "req") <=> Contains(network[p][q], "req") - /\ Contains(network'[q][p], "ack") <=> Contains(network[q][p], "ack") - /\ Precedes(network[p][q], "rel", "req") => Precedes(network'[p][q], "rel", "req") - BY <3>1, ContainsTail, PrecedesTail DEF BasicInv, NetworkInv - <4>. Contains(network[k][n], "rel") - BY <3>1 DEF Contains - <4>. ASSUME NEW q \in Proc, p # k \/ q # n - PROVE Contains(network'[p][q], "rel") <=> Contains(network[p][q], "rel") - BY <3>1 - <4>. QED BY <3>1, <3>3 DEF CommInv - <3>. QED BY <3>2, <3>3 DEF BasicInv - <2>7. CASE UNCHANGED vars - BY <2>7 DEF vars, BasicInv, CommInv, NetworkInv - <2>8. QED BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7 DEF Next -<1>. QED BY TypeCorrect, <1>1, <1>2, PTL DEF Spec - ------------------------------------------------------------------------------ -(***************************************************************************) -(* The second invariant relates the clock values stored in the clock and *) -(* req variables, as well as in request messages. Its proof relies on the *) -(* "basic" invariant proved previously. *) -(***************************************************************************) - -ClockInvInner(p,q) == - LET pq == network[p][q] - qp == network[q][p] - IN /\ \A i \in 1 .. Len(pq) : pq[i].type = "req" => pq[i].clock = req[p][p] - /\ Contains(qp, "ack") \/ q \in ack[p] => - /\ req[q][p] = req[p][p] - /\ clock[q] > req[p][p] - /\ Precedes(qp, "ack", "req") => - \A i \in 1 .. Len(qp) : qp[i].type = "req" => qp[i].clock > req[p][p] - /\ p \in crit => beats(p,q) - -ClockInv == \A p \in Proc : \A q \in Proc \ {p} : ClockInvInner(p,q) - -THEOREM ClockInvariant == Spec => []ClockInv -<1>1. Init => ClockInv - BY DEF Init, ClockInv, ClockInvInner, Contains -<1>2. TypeOK /\ BasicInv /\ ClockInv /\ [Next]_vars => ClockInv' - <2> SUFFICES ASSUME TypeOK, BasicInv, ClockInv, [Next]_vars - PROVE ClockInv' - OBVIOUS - <2>. USE DEF TypeOK - <2>1. ASSUME NEW n \in Proc, Request(n) - PROVE ClockInv' - <3>1. /\ req[n][n] = 0 - /\ req' = [req EXCEPT ![n][n] = clock[n]] - /\ network' = [network EXCEPT ![n] = Broadcast(n, ReqMessage(clock[n]))] - /\ ack' = [ack EXCEPT ![n] = {n}] - /\ UNCHANGED <> - /\ n \notin crit - /\ \A q \in Proc : ~ Contains(network[n][q], "req") /\ ~ Contains(network[q][n], "ack") - BY <2>1, ~(req[n][n] > 0), Zenon DEF Request, BasicInv, CommInv - <3>. /\ ReqMessage(clock[n]) \in Message - /\ ReqMessage(clock[n]).type = "req" - /\ ReqMessage(clock[n]).clock = req'[n][n] - BY <3>1, Zenon DEF ReqMessage, Message - <3>2. ASSUME NEW p \in Proc, NEW q \in Proc \ {p} - PROVE ClockInvInner(p,q)' - <4>1. CASE p = n - <5>1. ASSUME NEW i \in 1 .. Len(network'[p][q]), network'[p][q][i].type = "req" - PROVE network'[p][q][i].clock = req'[p][p] - BY <3>1, <4>1, <5>1 DEF Broadcast, Contains - <5>2. ~ Contains(network'[q][p], "ack") /\ q \notin ack'[p] - BY <3>1, <4>1 DEF Broadcast - <5>3. p \notin crit' - BY <3>1, <4>1 - <5>. QED BY <5>1, <5>2, <5>3 DEF ClockInvInner - <4>2. CASE q = n - <5>1. ClockInvInner(p,q) - BY DEF ClockInv - <5>2. UNCHANGED << network[p][q], req[p][p], req[p][q], req[q][p], ack[p], crit >> - BY <3>1, <4>2 - <5>. DEFINE qp == network[q][p] - <5>3. ASSUME Contains(qp', "ack") \/ q \in ack'[p] - PROVE /\ req'[q][p] = req[p][p] - /\ clock'[q] > req'[p][p] - /\ Precedes(qp', "ack", "req") => - \A i \in 1 .. Len(qp') : qp'[i].type = "req" => qp'[i].clock > req'[p][p] - <6>. Contains(qp, "ack") \/ q \in ack[p] - BY <3>1, <4>2, <5>3, ContainsSend DEF Broadcast - <6>. QED - BY <3>1, <4>2, <5>1 DEF ClockInvInner, Broadcast, Contains - <5>. QED BY <5>1, <5>2, <5>3 DEF ClockInvInner, beats - <4>3. CASE n \notin {p,q} \* all relevant variables unchanged - <5>1. /\ ClockInvInner(p,q) - /\ UNCHANGED <> - BY <3>1, <4>3 DEF ClockInv - <5>. QED BY ONLY <5>1 DEF ClockInvInner, beats - <4>. QED BY <4>1, <4>2, <4>3 - <3>. QED BY <3>2 DEF ClockInv - <2>2. ASSUME NEW n \in Proc, Enter(n) - PROVE ClockInv' - BY <2>2 DEF Enter, ClockInv, ClockInvInner, beats - <2>3. ASSUME NEW n \in Proc, Exit(n) - PROVE ClockInv' - <3>1. /\ n \in crit - /\ crit' = crit \ {n} - /\ network' = [network EXCEPT ![n] = Broadcast(n, RelMessage)] - /\ req' = [req EXCEPT ![n][n] = 0] - /\ ack' = [ack EXCEPT ![n] = {}] - /\ clock' = clock - /\ \A q \in Proc : /\ ~ Contains(network[n][q], "req") - /\ ~ Contains(network[q][n], "ack") - BY <2>3, Zenon DEF Exit, BasicInv, CommInv - <3>. RelMessage \in Message /\ RelMessage.type = "rel" - BY DEF RelMessage, Message - <3>2. ASSUME NEW p \in Proc, NEW q \in Proc \ {p} - PROVE ClockInvInner(p,q)' - <4>1. CASE n = p - BY <3>1, <4>1 DEF Broadcast, ClockInvInner, Contains - <4>2. CASE n # p - <5>1. /\ UNCHANGED << network[p][q], req[p][p], req[q][p], req[p][q], ack[p], clock >> - /\ p \in crit' <=> p \in crit - BY <3>1, <4>2 - <5>2. n # q => network'[q][p] = network[q][p] - BY <3>1 DEF Broadcast - <5>3. /\ Contains(network'[n][p], "ack") <=> Contains(network[n][p], "ack") - /\ Precedes(network'[n][p], "ack", "req") <=> Precedes(network[n][p], "ack", "req") - BY <3>1, <4>2, ContainsSend, PrecedesSend DEF Broadcast - <5>4. \A i \in 1 .. Len(network'[n][p]) : network'[n][p][i].type # "req" - BY <3>1 DEF Broadcast, Contains - <5>. QED BY <5>1, <5>2, <5>3, <5>4 DEF ClockInv, ClockInvInner, beats - <4>. QED BY <4>1, <4>2 - <3>. QED BY <3>2 DEF ClockInv - <2>4. ASSUME NEW n \in Proc, NEW k \in Proc \ {n}, ReceiveRequest(n,k) - PROVE ClockInv' - <3>. DEFINE m == Head(network[k][n]) - <3>1. /\ network[k][n] # << >> - /\ m.type = "req" - /\ req' = [req EXCEPT ![n][k] = m.clock] - /\ clock' = [clock EXCEPT ![n] = IF m.clock > clock[n] THEN m.clock + 1 - ELSE clock[n]+1] - /\ network' = [a \in Proc |-> [b \in Proc |-> - IF a=k /\ b=n THEN Tail(network[k][n]) - ELSE IF a=n /\ b=k THEN Append(network[n][k], AckMessage) - ELSE network[a][b]]] - /\ UNCHANGED <> - /\ m.clock = req[k][k] - /\ Contains(network[k][n], "req") - BY <2>4 DEF ReceiveRequest, ClockInv, ClockInvInner, Contains - <3>2. /\ req[k][k] > 0 - /\ n \notin ack[k] /\ k \notin crit - BY <3>1 DEF BasicInv, CommInv - <3>. AckMessage \in Message /\ AckMessage.type = "ack" - BY DEF AckMessage, Message - <3>3. ASSUME NEW p \in Proc, NEW q \in Proc \ {p} - PROVE ClockInvInner(p,q)' - <4>. DEFINE pq == network[p][q] - qp == network[q][p] - <4>. /\ ClockInvInner(p,q) - /\ UNCHANGED req[p][p] - BY <3>1 DEF ClockInv - <4>0. /\ network[k][n] \in Seq(Message) \ { <<>> } - /\ AtMostOne(network[k][n], "req") - /\ Head(network[k][n]).type = "req" - /\ network[k][n]' = Tail(network[k][n]) - BY <3>1 DEF BasicInv, NetworkInv - <4>1. CASE p = k /\ q = n - <5>2. ~(\E i \in 1 .. Len(pq') : pq'[i].type = "req") - BY <4>0, <4>1, ContainsTail, Isa DEF Contains - <5>3. clock'[q] > req'[p][p] - BY <3>1, <3>2, <4>1, Z3 - <5>4. /\ req'[q][p] = req'[p][p] - /\ q \notin ack'[p] - /\ p \notin crit' - BY <3>1, <3>2, <4>1 - <5>5. ASSUME Precedes(qp', "ack", "req"), - NEW i \in 1 .. Len(qp'), qp'[i].type = "req" - PROVE FALSE - BY <3>1, <4>1, <5>5, CVC4 DEF Precedes - <5>. QED BY <5>2, <5>3, <5>4, <5>5 DEF ClockInvInner - <4>2. CASE p = n /\ q = k - <5>1. UNCHANGED << req[q][p], clock[q], ack >> - BY <3>1, <4>2 - <5>2. ASSUME NEW i \in 1 .. Len(pq'), pq'[i].type = "req" - PROVE i \in 1 .. Len(pq) /\ pq'[i] = pq[i] - BY <3>1, <4>2, <5>2 - <5>3. Contains(qp', "ack") <=> Contains(qp, "ack") - BY <3>1, <4>2, ContainsTail, CVC4 DEF BasicInv, NetworkInv - <5>4. ~(\E i \in 1 .. Len(qp') : qp'[i].type = "req") - BY <4>0, <4>2, ContainsTail, Isa DEF Contains - <5>5. ASSUME p \in crit' - PROVE beats(p,q)' - <6>. /\ p \in crit - /\ q \in ack[p] - /\ ~ Contains(qp, "ack") - BY <3>1, <4>2, <5>5 DEF BasicInv, CommInv - <6>. Precedes(qp, "ack", "req") - BY NotContainsPrecedes - <6>. req'[p][q] > req[p][p] - BY <3>1, <4>2 DEF ClockInvInner - <6>. QED BY DEF beats - <5>. QED BY <5>1, <5>2, <5>3, <5>4, <5>5 DEF ClockInvInner - <4>3. CASE {p,q} \cap {n,k} = {} - BY <3>1, <4>3, ZenonT(10) DEF ClockInv, ClockInvInner, beats - <4>. QED BY <4>1, <4>2, <4>3 - <3>. QED BY <3>3 DEF ClockInv - <2>5. ASSUME NEW n \in Proc, NEW k \in Proc \ {n}, ReceiveAck(n,k) - PROVE ClockInv' - <3>1. /\ network[k][n] # << >> - /\ Head(network[k][n]).type = "ack" - /\ ack' = [ack EXCEPT ![n] = @ \union {k}] - /\ network' = [network EXCEPT ![k][n] = Tail(@)] - /\ UNCHANGED <> - /\ Contains(network[k][n], "ack") - BY <2>5 DEF ReceiveAck, BasicInv, CommInv, Contains - <3>2. ASSUME NEW p \in Proc , NEW q \in Proc \ {p}, ClockInvInner(p,q) - PROVE ClockInvInner(p,q)' - <4>. DEFINE pq == network[p][q] - qp == network[q][p] - <4>1. CASE p = n /\ q = k - <5>1. /\ Contains(qp, "ack") - /\ UNCHANGED << pq, clock, req, crit >> - BY <3>1, <4>1 - <5>2. ASSUME Precedes(qp', "ack", "req"), - NEW i \in 1 .. Len(qp'), qp'[i].type = "req" - PROVE /\ Precedes(qp, "ack", "req") - /\ i+1 \in 1 .. Len(qp) /\ qp'[i] = qp[i+1] - BY <3>1, <4>1, <5>2, PrecedesInTail, CVC4 - <5>. QED BY <3>2, <5>1, <5>2 DEF ClockInvInner, beats - <4>2. CASE p = k /\ q = n - <5>1. UNCHANGED << qp, ack[p], clock, req, crit >> - BY <3>1, <4>2 - <5>2. ASSUME NEW i \in 1 .. Len(pq') - PROVE i+1 \in 1 .. Len(pq) /\ pq'[i] = pq[i+1] - BY <3>1, <4>2 - <5>. QED BY <3>2, <5>1, <5>2 DEF ClockInvInner, beats - <4>3. CASE {p,q} # {n,k} - BY <3>1, <3>2, <4>3 DEF ClockInvInner, beats - <4>. QED BY <4>1, <4>2, <4>3, Zenon - <3>. QED BY <3>2 DEF ClockInv - <2>6. ASSUME NEW n \in Proc, NEW k \in Proc \ {n}, ReceiveRelease(n,k) - PROVE ClockInv' - <3>1. /\ network[k][n] # << >> - /\ Head(network[k][n]).type = "rel" - /\ req' = [req EXCEPT ![n][k] = 0] - /\ network' = [network EXCEPT ![k][n] = Tail(@)] - /\ UNCHANGED << clock, ack, crit >> - BY <2>6 DEF ReceiveRelease - <3>2. Contains(network[k][n], "rel") - BY <3>1 DEF Contains - <3>3. /\ ~ Contains(network[n][k], "ack") - /\ n \notin ack[k] - BY <3>2 DEF BasicInv, CommInv - <3>4. ASSUME NEW p \in Proc, NEW q \in Proc, ClockInvInner(p,q) - PROVE ClockInvInner(p,q)' - <4>. DEFINE pq == network[p][q] - qp == network[q][p] - <4>1. CASE p = n /\ q = k - <5>. /\ UNCHANGED << pq, ack, req[p][p], req[q][p], clock >> - /\ beats(p,q)' - /\ \A i \in 1 .. Len(qp') : i+1 \in 1 .. Len(qp) /\ qp'[i] = qp[i+1] - BY <3>1, <4>1 DEF beats - <5>. /\ Contains(qp', "ack") <=> Contains(qp, "ack") - /\ Precedes(qp', "ack", "req") => Precedes(qp, "ack", "req") - BY <3>1, <4>1, ContainsTail, PrecedesInTail DEF BasicInv, NetworkInv - <5>. QED BY <3>4 DEF ClockInvInner - <4>2. CASE p = k /\ q = n - <5>. /\ UNCHANGED << qp, ack, req[p][p], req[p][q], crit, clock >> - /\ ~ Contains(qp', "ack") /\ q \notin ack'[p] - /\ \A i \in 1 .. Len(pq') : i+1 \in 1 .. Len(pq) /\ pq'[i] = pq[i+1] - BY <3>1, <3>3, <4>2 - <5>. QED BY <3>4 DEF ClockInvInner, beats - <4>3. CASE {p,q} # {k,n} - BY <3>1, <3>4, <4>3 DEF ClockInvInner, beats - <4>. QED BY <4>1, <4>2, <4>3, Zenon - <3>. QED BY <3>4 DEF ClockInv - <2>7. CASE UNCHANGED vars - BY <2>7 DEF ClockInv, ClockInvInner, beats, vars - <2>8. QED BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7 DEF Next -<1>. QED BY <1>1, <1>2, TypeCorrect, BasicInvariant, PTL DEF Spec - ------------------------------------------------------------------------------ -(***************************************************************************) -(* Mutual exclusion is a simple consequence of the above invariants. *) -(* In particular, if two distinct processes p and q were ever in the *) -(* critical section at the same instant, then beats(p,q) and beats(q,p) *) -(* would both have to hold, but this is impossible. *) -(***************************************************************************) -THEOREM Safety == Spec => []Mutex -<1>1. TypeOK /\ BasicInv /\ ClockInv => Mutex -\* BY NType DEF Proc, TypeOK, BasicInv, CommInv, ClockInv, ClockInvInner, Mutex, beats - <2>. SUFFICES ASSUME TypeOK, BasicInv, ClockInv, NEW p \in crit, NEW q \in crit, p # q - PROVE FALSE - BY DEF Mutex - <2>. p \in Proc /\ q \in Proc - BY DEF TypeOK - <2>1. /\ req[p][p] > 0 /\ q \in ack[p] - /\ req[q][q] > 0 /\ p \in ack[q] - BY DEF BasicInv, CommInv - <2>2. /\ req[q][p] = req[p][p] - /\ req[p][q] = req[q][q] - /\ beats(p,q) /\ beats(q,p) - BY <2>1, Zenon DEF ClockInv, ClockInvInner - <2>. QED BY NType, <2>1, <2>2 DEF beats, TypeOK, Proc -<1>. QED BY TypeCorrect, BasicInvariant, ClockInvariant, <1>1, PTL - -============================================================================== diff --git a/examples/SimpleEventuallyInt.tla b/examples/SimpleEventuallyInt.tla index 5dc7ca425..a6faa03eb 100644 --- a/examples/SimpleEventuallyInt.tla +++ b/examples/SimpleEventuallyInt.tla @@ -69,7 +69,7 @@ PROOF <3> QED BY <1>1, <3>2, <3>3, <3>4, <3>5, <3>6, <3>7, <3>8, PTL DEF System <2> QED - BY <2>1, <2>2, NatInduction + BY <2>1, <2>2, NatInduction, Isa <1>3. P(20) BY <1>2 <1> QED diff --git a/examples/paxos/Paxos.tla b/examples/paxos/Paxos.tla index 8449d3429..de5a22265 100644 --- a/examples/paxos/Paxos.tla +++ b/examples/paxos/Paxos.tla @@ -282,7 +282,7 @@ LEMMA SafeAtStable == Inv /\ Next /\ TypeOK' => THEOREM Invariant == Spec => []Inv <1> USE DEF Ballots <1>1. Init => Inv - BY Isa DEF Init, Inv, TypeOK, AccInv, MsgInv, VotedForIn + BY DEF Init, Inv, TypeOK, AccInv, MsgInv, VotedForIn <1>2. Inv /\ [Next]_vars => Inv' <2> SUFFICES ASSUME Inv, Next @@ -324,7 +324,7 @@ THEOREM Invariant == Spec => []Inv BY <2>1, <4>1, NoneNotAValue DEF AccInv, TypeOK, Messages <4>3. \A aa,vv,bb : VotedForIn(aa,vv,bb)' <=> VotedForIn(aa,vv,bb) \/ (aa = a /\ vv = maxVal'[a] /\ bb = maxVBal'[a]) - BY <4>1, Isa DEF VotedForIn, Send, TypeOK, Messages + BY <4>1 DEF VotedForIn, Send, TypeOK, Messages <4>4. ASSUME NEW acc \in Acceptors, maxVBal'[acc] >= 0 PROVE VotedForIn(acc, maxVal[acc], maxVBal[acc])' BY <4>1, <4>3, <4>4 DEF AccInv, TypeOK @@ -386,7 +386,7 @@ THEOREM Invariant == Spec => []Inv BY <4>3 DEF VotedForIn <4>6. \A m,ma \in msgs' : m.type = "2a" /\ ma.type = "2a" /\ ma.bal = m.bal => ma = m - BY <4>1, <4>3, Isa DEF MsgInv + BY <4>1, <4>3 DEF MsgInv <4>10. SafeAt(v,b) <5>0. PICK Q \in Quorums, S \in SUBSET {m \in msgs : (m.type = "1b") /\ (m.bal = b)} : @@ -400,7 +400,17 @@ THEOREM Invariant == Spec => []Inv <5>1. CASE \A m \in S : m.maxVBal = -1 \* In that case, no acceptor in Q voted in any ballot less than b, \* by the last conjunct of MsgInv for type "1b" messages, and that's enough - BY <5>1, <5>0 DEF TypeOK, MsgInv, SafeAt, WontVoteIn, Messages + <6>1. \A m \in S : + /\ m.bal =< maxBal[m.acc] + /\ \A c \in (m.maxVBal+1) .. (m.bal-1) : + ~ \E v \in Values : VotedForIn(m.acc, v, c) + BY DEF MsgInv + <6>2. \A c \in 0..(b-1) : \A a \in Q : \A v \in Values : + ~ VotedForIn(a, v, c) + BY <5>0, <5>1, <6>1 + <6>3. \A c \in 0..(b-1) : \A a \in Q : maxBal[a] > c + BY <5>0, <6>1, QuorumAssumption DEF TypeOK + <6>. QED BY <6>2, <6>3 DEF SafeAt, WontVoteIn <5>2. ASSUME NEW c \in 0 .. (b-1), \A m \in S : m.maxVBal =< c, NEW ma \in S, ma.maxVBal = c, ma.maxVal = v @@ -464,15 +474,13 @@ THEOREM Consistent == Spec => []Consistency PROVE v1 = v2 BY DEF Consistency, Chosen <2>1. CASE b1 = b2 - BY <2>1, VotedOnce, QuorumAssumption DEF ChosenIn, Inv -(* +\* BY <2>1, VotedOnce, QuorumAssumption DEF ChosenIn, Inv <3>1. PICK a1 \in Acceptors : VotedForIn(a1, v1, b1) - BY QuorumAssumption DEF ChosenIn + BY QuorumAssumption, Zenon DEF ChosenIn <3>2. PICK a2 \in Acceptors : VotedForIn(a2, v2, b2) - BY QuorumAssumption DEF ChosenIn + BY QuorumAssumption, Zenon DEF ChosenIn <3>. QED BY <3>1, <3>2, <2>1, VotedOnce DEF Inv -*) <2>2. CASE b1 < b2 <3>1. SafeAt(v2, b2) BY VotedInv, QuorumNonEmpty, QuorumAssumption DEF ChosenIn, Inv @@ -500,29 +508,23 @@ THEOREM Refinement == Spec => C!Spec BY QuorumNonEmpty, Zenon DEF Init, C!Init, chosenBar, Chosen, ChosenIn, VotedForIn <1>2. TypeOK' /\ Consistency' /\ [Next]_vars => [C!Next]_chosenBar - <2> SUFFICES ASSUME TypeOK', Consistency', Next, chosenBar' # chosenBar - PROVE C!Next - BY DEF vars, chosenBar, Chosen, ChosenIn, VotedForIn - <2>1. chosenBar \subseteq chosenBar' - BY DEF Send, chosenBar, Chosen, ChosenIn, VotedForIn, Next, Phase1a, Phase1b, Phase2a, Phase2b - <2>2. \A v, w \in chosenBar': v = w - BY DEF Consistency, chosenBar, ChosenIn, TypeOK - <2>3. chosenBar = {} - BY <2>1, <2>2\*, SetExtensionality - <2>. QED - BY <2>1, <2>2, <2>3 DEF C!Next, chosenBar + <2> SUFFICES ASSUME TypeOK', Consistency', [Next]_vars + PROVE [C!Next]_chosenBar + OBVIOUS + <2>1. CASE Next + <3>1. chosenBar \subseteq chosenBar' + BY <2>1 DEF Send, chosenBar, Chosen, ChosenIn, VotedForIn, Next, Phase1a, Phase1b, Phase2a, Phase2b + <3>2. \A v, w \in chosenBar': v = w + BY DEF Consistency, chosenBar, ChosenIn, TypeOK + <3>. QED + BY <3>1, <3>2 DEF C!Next, chosenBar + <2>2. CASE UNCHANGED vars + BY <2>2 DEF vars, chosenBar, Chosen, ChosenIn, VotedForIn + <2>. QED BY <2>1, <2>2 <1>3. QED BY <1>1, <1>2, Invariant, Consistent, PTL DEF Spec, C!Spec, Inv ============================================================================= \* Modification History -\* Last modified Fri Jan 10 17:34:42 CET 2020 by merz -\* Last modified Sun Oct 20 18:25:27 CEST 2019 by merz -\* Last modified Fri Nov 28 10:39:17 PST 2014 by lamport -\* Last modified Sun Nov 23 14:45:09 PST 2014 by lamport -\* Last modified Sat Nov 22 12:04:19 CET 2014 by merz -\* Last modified Fri Nov 21 17:40:41 PST 2014 by lamport -\* Last modified Tue Mar 18 11:37:57 CET 2014 by doligez -\* Last modified Sat Nov 24 18:53:09 GMT-03:00 2012 by merz \* Created Sat Nov 17 16:02:06 PST 2012 by lamport diff --git a/examples_draft/FOLTL.tla b/examples_draft/FOLTL.tla index 3137b2851..d8804ffd0 100644 --- a/examples_draft/FOLTL.tla +++ b/examples_draft/FOLTL.tla @@ -29,16 +29,6 @@ THEOREM ASSUME NEW n \in Nat, STATE x PROVE (\A i \in 1..n : []<>(x=i)) <=> [](\A i \in 1..n : <>(x=i)) OBVIOUS -(***************************************************************************) -(* Attempting to prove the above theorem for a non-constant set S fails, *) -(* as it should. However, the proof obligation sent to the backend provers *) -(* LOOKS WRONG because the universal quantifier on the right-hand side is *) -(* moved out of the scope of the [] formula. *) -(***************************************************************************) -THEOREM ASSUME TEMPORAL A(_), STATE S - PROVE (\A x \in S : []A(x)) <=> [](\A x \in S : A(x)) -OBVIOUS - ----------------------------------------------------------------------------- (***************************************************************************) @@ -71,12 +61,9 @@ THEOREM STL6_gen == OBVIOUS <3>. QED BY <3>1, PTL <2>. QED BY <2>1, <2>2, <2>3 -<1>. QED - <2>. HIDE DEF G - <2>1. ASSUME NEW T, IsFiniteSet(T) PROVE G(T) - BY <1>1, <1>2, IsFiniteSet(T), FS_Induction, IsaM("blast") - <2>2.G(S) BY <2>1 \* why does the proof fail without this step? - <2>. QED BY <2>2 DEF G +<1>. HIDE DEF G +<1>3. G(S) BY <1>1, <1>2, FS_Induction, IsaM("blast") +<1>. QED BY <1>3 DEF G ----------------------------------------------------------------------------- @@ -139,8 +126,4 @@ THEOREM Barcan == <1>. QED BY <1>3, <1>4, <1>6 ============================================================================= -\* Modification History -\* Last modified Sun Apr 12 09:34:48 CEST 2020 by merz -\* Last modified Tue Nov 05 18:40:17 CET 2019 by merz -\* Last modified Tue Nov 05 05:30:04 PST 2019 by lamport \* Created Wed Mar 15 11:46:27 PDT 2017 by lamport diff --git a/examples_draft/quicksort/Quicksort01.tla b/examples_draft/quicksort/Quicksort01.tla deleted file mode 100755 index 0a84848f4..000000000 --- a/examples_draft/quicksort/Quicksort01.tla +++ /dev/null @@ -1,121 +0,0 @@ ------------------------------ MODULE Quicksort01 ----------------------------- -(***************************************************************************) -(* This module specifies a Quicksort algorithm for sorting a sequence A of *) -(* length N of integers. *) -(***************************************************************************) -EXTENDS Integers, TLAPS - -CONSTANT A0, N - -ASSUME ConstantAssump == /\ N \in Nat \ {0} - /\ A0 \in [1..N -> Int] - -IsSorted(B) == \A i, j \in 1..N : (i < j) => (B[i] =< B[j]) - -PermsOf(Arr) == - LET Automorphisms(S) == { f \in [S -> S] : - \A y \in S : \E x \in S : f[x] = y } - f ** g == [x \in DOMAIN g |-> f[g[x]]] - IN { Arr ** f : f \in Automorphisms(DOMAIN Arr) } - -Partitions(B, pivot, lo, hi) == - {C \in PermsOf(B) : - /\ \A i \in 1..(lo-1) \cup (hi+1)..N : C[i] = B[i] - /\ \A i \in lo..pivot, j \in (pivot+1)..hi : C[i] =< C[j] } - -VARIABLES A, U - -TypeOK == /\ A \in [1..N -> Int] - /\ U \in SUBSET ((1..N) \X (1..N)) - -vars == <> - -Init == /\ A = A0 - /\ U = { <<1, N>> } - -Next == /\ U # {} - /\ \E b \in 1..N, t \in 1..N : - /\ <> \in U - /\ IF b # t - THEN \E p \in b..(t-1) : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \cup {<>, <>} - ELSE /\ U' = U \ {<>} - /\ A' = A - -Spec == Init /\ [][Next]_vars /\ WF_vars(Next) ------------------------------------------------------------------------------ -Safety == (U = {}) => (A \in PermsOf(A0)) /\ IsSorted(A) - -THEOREM Spec => []Safety -(* OK, how does one proof anything? -> go to online tutorial to look up basic proof structure - - actually, I was hoping for something like "A TLA+ Proof looks like this:... - a little higher level than the "A simple proof" section on the TLA+ Proos System website -------------------------------------------------------------------------------------------- - - attempt 1: - Let's just try writing OBVIOUS and see what happens... - - notes: - - it took Damien to explain to me that I can't write anything under the `=========================` -++++++++++ -OBVIOUS -*) - - -(* - attempt 2: - Attempt 1 didn't get us far, we'll have to be more sophisticated than that, so I'm scrolling down the online tutorial - - - OK, it took me a while to find the "the general form af a BY proof is : ...." on the - website, but now I found it, so I'll use it... - - notes: - - I find it un-intuitive, that I can't unfold WF_(vars) or WF like Spec etc... -+++++++++++ -BY ConstantAssump DEF Spec, Safety - *) - -(* attempt 3: - Attempt 2 got me in an interactive mindset: I can see that I can interact with the proof state by looking and changing these obligations - I played around with adding "Next" and "Init" to the list after "DEF". - - But logically it didn't get me anywhere, so I'll try something else: - - Ok, now I'm on the "Hierarchical proofs" section on the website, and it seems to tell me how to do an - an implication elimination, which is a relief. It seems to be done by "suffices [..] assume [..] proof" - - notes: - - I started out with the following code: - <1> SUFFICES ASSUME Speck - PROVE []Safety - - I got a cryptic error message, it took Damien to explain that every step of a hierarchical proof needs to be closed by a "QED"-step with the same level - - I think the underlying problem there may be that in the online tutorial there are partial bits of code, which when copied and pasted give syntax errors. - - - Damien also pointed out I should be using the hyperbook ... That is referenced in the preamble to the online tutorial, but I skipped the preamble. - I think there is a deeper problem there: all the documentation is very example-driven and very holistic in the sense that there is a lot of text and a lot of explaining. - I'm in a goal-oriented mindest: I have a theorem, I want to prove it. What I'm really looking for are answers to - questions like "How do I do implication elimination?" "How do I prove a box?" "What does the most basic syntactically correct hierarchical proof look like?", etc. - So some sort of documentation that can be accesses in a demand-driven way, or a cheat-sheet with the most basic proof structures. - - - The way "QED" steps work is not intuitive, at least not yet... - - *) -<1> SUFFICES ASSUME Spec - PROVE []Safety -<1>1 []Safety -<1> QED - BY <1>1, LS4 - - (* Side Notes: - - it is annoying that the parser errors don't wrap around lines and I don't seem to be able to sort windows in the toolbox, so I can have them below the obligations... *) - - - - -============================================================================= - diff --git a/examples_draft/quicksort/Quicksort02.tla b/examples_draft/quicksort/Quicksort02.tla deleted file mode 100755 index 56ed67d03..000000000 --- a/examples_draft/quicksort/Quicksort02.tla +++ /dev/null @@ -1,185 +0,0 @@ ------------------------------ MODULE Quicksort02 ----------------------------- -(***************************************************************************) -(* This module specifies a Quicksort algorithm for sorting a sequence A of *) -(* length N of integers. *) -(***************************************************************************) -EXTENDS Integers, TLAPS - -CONSTANT A0, N - -ASSUME ConstantAssump == /\ N \in Nat \ {0} - /\ A0 \in [1..N -> Int] - -IsSorted(B) == \A i, j \in 1..N : (i < j) => (B[i] =< B[j]) - -PermsOf(Arr) == - LET Automorphisms(S) == { f \in [S -> S] : - \A y \in S : \E x \in S : f[x] = y } - f ** g == [x \in DOMAIN g |-> f[g[x]]] - IN { Arr ** f : f \in Automorphisms(DOMAIN Arr) } - -Partitions(B, pivot, lo, hi) == - {C \in PermsOf(B) : - /\ \A i \in 1..(lo-1) \cup (hi+1)..N : C[i] = B[i] - /\ \A i \in lo..pivot, j \in (pivot+1)..hi : C[i] =< C[j] } - -VARIABLES A, U - -TypeOK == /\ A \in [1..N -> Int] - /\ U \in SUBSET ((1..N) \X (1..N)) - -vars == <> - -Init == /\ A = A0 - /\ U = { <<1, N>> } - -Next == /\ U # {} - /\ \E b \in 1..N, t \in 1..N : - /\ <> \in U - /\ IF b # t - THEN \E p \in b..(t-1) : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \cup {<>, <>} - ELSE /\ U' = U \ {<>} - /\ A' = A - -Spec == Init /\ [][Next]_vars /\ WF_vars(Next) ------------------------------------------------------------------------------ -Safety == (U = {}) => (A \in PermsOf(A0)) /\ IsSorted(A) -Inv == TypeOK /\ Safety - - -THEOREM Spec => []Safety - - -(* attempt 5: - Right, how does one proof a box? - - Hypterbook 11.1 is very useful! it's a pity that it isn't self contained: I don't know what `Inv' is... - I'll just try adding it as an undefined symbol and see what happens... - -<1>1 Init => Inv -<1>2 Inv /\ [Next]_vars => Inv' -<1>3 Inv => Safety - -<1>4 QED - *) - -(* attempt 6: - right, that didn't work: now I'll have to go chase references in the hyperbook... - - reading Sec. 4.9.1 is helpful, let's try find an inductive invariant... - - It seems like Safety itself is a reasonable working hypothesis for an invariant for now... - Let's try that plus TypeOK -- - can I define things in the middle of proofs? - Inv == /\ TypeOK /\ Safety - apparently not... - - Ok, now it's just under the definition of 'Safety'. - Now when I go C-g C-g everything is yellow, but I get no interesting obligations... ? - - I'll try and get the QED green first... - -+++++++++++++++++++ -<1>1 Init => Inv -<1>2 Inv /\ [Next]_vars => Inv' -<1>3 Inv => Safety -<1>4 QED - BY LS4, <1>1, <1>2, <1>3 DEF Inv, Spec (* AHA!! my first very own green `QED' ! celebratory cup of tea! *) - -( attempt 7: - now for the steps in between: - - <1>1: - I'm getting a syntax error for this: why?!? -++++++++++++++++++ -<1>1 Init => Inv - PROOF - <2>1 ASSUME Init - PROVE Inv - <2>2 BY <2>1 DEF Init, Inv, TypeOK, Safety - -<1>2 Inv /\ [Next]_vars => Inv' -<1>3 Inv => Safety - -<1>4 QED - BY LS4, <1>1, <1>2, <1>3 DEF Inv, Spec -++++++++++++++++++++ -*) - - -(* attempt 8: - aha, always put the `QED' ! - - - *) - -<1>1 Init => Inv - PROOF - <2>1 ASSUME Init - PROVE U # {} - BY <2>1 DEF Init - (* getting the syntax right here took me a long time: I'm not sure what the `BY' is proving: - If it's the `ASSUME-PROVE' then why does it need not be tols to use <2>1 ? - If its something else, then why does putting a label like <2>2 in front of it result in a syntax error? *) - <2>2 SUFFICES (Init => U # {}) /\ (Init => TypeOK) - BY DEF Inv, Safety, TypeOK - <2>3 Init => U # {} - BY DEF Init - <2>4 Init => TypeOK - BY Z3, ConstantAssump DEF Init, TypeOK, ConstantAssump - <2> QED - BY <2>2, <2>3, <2>4 - (* The `QED' referrs to <1>1 ? Why is it still red? *) - -<1>2 Inv /\ [Next]_vars => Inv' - PROOF - <2>1 SUFFICES (TypeOK /\ [Next]_vars => TypeOK') /\ (Inv /\ [Next]_vars => Safety') - BY DEF Inv - <2>2 ASSUME TypeOK, [Next]_vars - PROVE TypeOK' - (* right-clicking on this and then clicking `Decompose Proof' gives me an error message - "Spec status must be `parsed' to execute this command" -- but my spec status is `parsed' !!? *) - - - <3>1 SUFFICES (A \in [1 .. N -> Int] /\ [Next]_vars => A' \in [1..N -> Int]) - /\ ( (U \in SUBSET ((1 .. N) \X (1 .. N))) /\ [Next]_vars => U' \in SUBSET ((1 .. N) \X (1 .. N))) - BY <3>1 DEF TypeOK - (* It seems to me that this is just reordering the conjunctions (conjunction elimination + weakening on the left-side and conjunction introduction on the right)? - why doesn't it work? *) - <3> QED - - <2> QED - BY <2>1 DEF Inv -<1>3 Inv => Safety - <2> QED - BY DEF Inv - -<1>4 QED - BY LS4, <1>1, <1>2, <1>3 DEF Inv, Spec - - - (* Side Notes: - - It is annoying that the parser errors don't wrap around lines and I don't seem to be able to sort windows in the toolbox, so I can have them below the obligations... - - - I typed Ctrl-w (emacs-person that I am) and lost the text window somehow... - - - Why do I not get any interesting obligations, when typing C-g C-g in the following state: -++++++++++ -THEOREM Spec => []Safety - -<1> SUFFICES ASSUME Spec - PROVE []Safety -<1>1 []Safety - -<1> QED - BY <1>1, LS4" -+++++++++++ - ?? - - *) - - -============================================================================= - diff --git a/examples_draft/quicksort/Quicksort03.tla b/examples_draft/quicksort/Quicksort03.tla deleted file mode 100755 index 33a184d31..000000000 --- a/examples_draft/quicksort/Quicksort03.tla +++ /dev/null @@ -1,450 +0,0 @@ ------------------------------ MODULE Quicksort03 ----------------------------- -(***************************************************************************) -(* This module specifies a Quicksort algorithm for sorting a sequence A of *) -(* length N of integers. *) -(***************************************************************************) -EXTENDS Integers, TLAPS - -CONSTANT A0, N - -ASSUME ConstantAssump == /\ N \in Nat \ {0} - /\ A0 \in [1..N -> Int] - -IsSorted(B) == \A i, j \in 1..N : (i < j) => (B[i] =< B[j]) - -PermsOf(Arr) == - LET Automorphisms(S) == { f \in [S -> S] : - \A y \in S : \E x \in S : f[x] = y } - f ** g == [x \in DOMAIN g |-> f[g[x]]] - IN { Arr ** f : f \in Automorphisms(DOMAIN Arr) } - -Partitions(B, pivot, lo, hi) == - {C \in PermsOf(B) : - /\ \A i \in 1..(lo-1) \cup (hi+1)..N : C[i] = B[i] - /\ \A i \in lo..pivot, j \in (pivot+1)..hi : C[i] =< C[j] } - -VARIABLES A, U - -TypeOK == /\ A \in [1..N -> Int] - /\ U \in SUBSET ((1..N) \X (1..N)) - -vars == <> - -Init == /\ A = A0 - /\ U = { <<1, N>> } - -Next == /\ U # {} - /\ \E b \in 1..N, t \in 1..N : - /\ <> \in U - /\ IF b # t - THEN \E p \in b..(t-1) : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \cup {<>, <>} - ELSE /\ U' = U \ {<>} - /\ A' = A - -Spec == Init /\ [][Next]_vars /\ WF_vars(Next) ------------------------------------------------------------------------------ -Safety == (U = {}) => (A \in PermsOf(A0)) /\ IsSorted(A) -Inv == TypeOK /\ Safety - - -THEOREM Spec => []Safety -(* attempt 9: - right, now I'll have to get stuff in and out of []_vars and primes... - - - ok, putting `PTL' adds the annotation (* non-[]*) in the obligation -- - the scope of the annotation is not clear to me... also, I think it is unhappy that the square brackets are used - in a second way there... - - - so there seems to be something going on witht things being in the []-context or not, so I'll try putting boxes in places ... - starting with the `ASSUME-PROVE': - ++++++++++++++ - <2>2 ASSUME [] (TypeOK, [Next]_vars) - PROVE [](TypeOK') - ++++++++++++++ - clearly that's not the right syntax... where do I look this up? - - - hyperbook section 11 doesn't seem to have anything, neither does the webpage, - so I'm forgettinga bout []-contexts for the moment, and and am just going to prove the two conjuncts and worry about the `SUFFICES' later when people are around... - *) - - -(* attempt 10: - - - the following gives a syntax error "Was expecting "Step number" on the `<3> QED' line, that I find very puzzling: - -++++++++++++++++++++++++ -<1>1 Init => Inv - PROOF - <2>1 ASSUME Init - PROVE U # {} - BY <2>1 DEF Init - <2>2 SUFFICES (Init => U # {}) /\ (Init => TypeOK) - BY DEF Inv, Safety, TypeOK - <2>3 Init => U # {} - BY DEF Init - <2>4 Init => TypeOK - BY Z3, ConstantAssump DEF Init, TypeOK, ConstantAssump - <2> QED - BY <2>2, <2>3, <2>4 - (* The `QED' referrs to <1>1 ? Why is it still red? *) - -<1>2 Inv /\ [Next]_vars => Inv' - PROOF - <2>1 SUFFICES (TypeOK /\ [Next]_vars => TypeOK') /\ (Inv /\ [Next]_vars => Safety') - BY DEF Inv - <2>2 ASSUME TypeOK, [Next]_vars - PROVE TypeOK' - <3>1 (A \in [1 .. N -> Int] /\[Next]_vars) => A' \in [1..N -> Int] - <4>1 HAVE A \in [1..N -> Int] - <4>2 HAVE [Next]_vars - - (* <3>2 SUFFICES - /\ ( (A \in [1 .. N -> Int] /\ [Next]_vars) => A' \in [1..N -> Int] ) - /\ ( (U \in SUBSET ((1 .. N) \X (1 .. N)) /\ [Next]_vars) => U' \in SUBSET ((1 .. N) \X (1 .. N))) - BY PTL DEF TypeOK *) - <3> QED - - <2> QED - BY <2>1 DEF Inv -<1>3 Inv => Safety - <2> QED - BY DEF Inv - -<1>4 QED - BY LS4, <1>1, <1>2, <1>3 DEF Inv, Spec -+++++++++++++++++++++++++ - -- aha, again I was missing a `QED'-step... - - -*) - -(* attempt 11: - - - there is something puzzling going on with `HAVE': - - in the subproof under `<3>1 (A \in [1 .. N -> Int] /\[Next]_vars) => A' \in [1..N -> Int]' - the following code gets the following colours and obligation: - +++++++++++++ - PROOF - green <4>1 HAVE A \in [1..N -> Int] - red <4>2 HAVE [Next]_vars - yellow <4> QED - ++++++++++++++++ - Error: this HAVE step is applied to the following goal, -which is not an implication: - A' \in [1 .. N -> Int] - - Deleting the stepnumber before the second `HAVE' gives a syntax error; - so does contracting the two `HAVE's into one and putting a `,' between the two antecedents I want to "have". - - When proving an implication with a conjunction for an antecedent, I can't `HAVE' each conjunct separately?? - - - - right, now I'm `HAVE'-ing the conjunction and I'm trying to take apart the [Next]_vars - so I'm `PICK'-ing a b and a t, and I'd like to do a case-analysis on the `IF-THEN-ELSE', - it took me a long time to find some syntax for that. The obivous place to look is in the online tutorial where `SUFFICES' and `PICK' and similar - proof constructs are explained, but it's not there... - - I found it under `non-QED steps' at the bottom of the hieararchical proofs page: - again, some sort of cheat-sheet with correct sytnax for all proof constructs would be appreciated! - - -<1>1 Init => Inv - PROOF - <2>1 ASSUME Init - PROVE U # {} - BY <2>1 DEF Init - <2>2 SUFFICES (Init => U # {}) /\ (Init => TypeOK) - BY DEF Inv, Safety, TypeOK - <2>3 Init => U # {} - BY DEF Init - <2>4 Init => TypeOK - BY Z3, ConstantAssump DEF Init, TypeOK, ConstantAssump - <2> QED - BY <2>2, <2>3, <2>4 - -<1>2 Inv /\ [Next]_vars => Inv' - PROOF - <2>1 SUFFICES (TypeOK /\ [Next]_vars => TypeOK') /\ (Inv /\ [Next]_vars => Safety') - BY DEF Inv - <2>2 ASSUME TypeOK, [Next]_vars - PROVE TypeOK' - <3>1 (A \in [1 .. N -> Int] /\[Next]_vars) => A' \in [1..N -> Int] - PROOF - <4>1 HAVE A \in [1..N -> Int] /\ [Next]_vars - <4>2 PICK b : b \in 1..N - <4>3 PICK t : t \in 1..N - <4>4 CASE b = t - <5> QED - BY <4>1 DEF Next - - <4> QED - - <3>2 SUFFICES - /\ ( (A \in [1 .. N -> Int] /\ [Next]_vars) => A' \in [1..N -> Int] ) - /\ ( (U \in SUBSET ((1 .. N) \X (1 .. N)) /\ [Next]_vars) => U' \in SUBSET ((1 .. N) \X (1 .. N))) - BY PTL DEF TypeOK - <3> QED - - <2> QED - BY <2>1 DEF Inv -<1>3 Inv => Safety - <2> QED - BY DEF Inv - -<1>4 QED - BY LS4, <1>1, <1>2, <1>3 DEF Inv, Spec -*) - -(* attempt 12: - - - I couldn't find any documentation on how to use `\E' statements, - but on the bright side, wild clicking finally got me in a `DECOMPOSE-PROOF'-menu, - so I'll try that... - It seems I always get the "spec status must be `parsed'" error message the first time I try triggering `DECOMPOSE PROOF', - and if I then click at the same place again, I get the menu... ?? - - Also: why can I decompose a proof in a state where I can't click the `P' button that prints the structure?!? - - - Right, I'm giving up on decomposing <4>2 into something useful... - - - I've been loking for documentation on how to use the existential in the antecedent, but can't seem to find anything. - It seems to be something like `NEW ... ' I'll just go trying things... - -*) - - -<1>1 Init => Inv - PROOF - <2>1 ASSUME Init - PROVE U # {} - BY <2>1 DEF Init - <2>2 SUFFICES (Init => U # {}) /\ (Init => TypeOK) - BY DEF Inv, Safety, TypeOK - <2>3 Init => U # {} - BY DEF Init - <2>4 Init => TypeOK - BY Z3, ConstantAssump DEF Init, TypeOK, ConstantAssump - <2> QED - BY <2>2, <2>3, <2>4 - -<1>2 Inv /\ [Next]_vars => Inv' - <2>1 SUFFICES (TypeOK /\ [Next]_vars => TypeOK') /\ (Inv /\ [Next]_vars => Safety') - BY DEF Inv - <2>2 ASSUME TypeOK, [Next]_vars - PROVE TypeOK' - <3>1. CASE Next (* here I'm trying to decompose and it just quietly does nothing... *) - <4>1 SUFFICES ASSUME TypeOK, - U # {}, - \E b \in 1 .. N, t \in 1 .. N : - /\ <> \in U - /\ IF b # t - THEN \E p \in b .. t - 1 : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \union {<>, <

>} - ELSE /\ U' = U \ {<>} - /\ A' = A - PROVE TypeOK' - BY <2>2, <3>1 DEF Next - <4>2 ASSUME TypeOK, - U # {}, - NEW b \in 1 .. N, - NEW t \in 1 .. N, - /\ <> \in U - /\ IF b # t - THEN \E p \in b .. t - 1 : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \union {<>, <

>} - ELSE /\ U' = U \ {<>} - /\ A' = A - PROVE TypeOK' - <5>1 CASE b # t - <6>1 SUFFICES ASSUME TypeOK, - U # {}, - \E p \in b .. t - 1 : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \union {<>, <

>} - PROVE TypeOK' - BY <4>2, <5>1 - <6>2 ASSUME TypeOK, U # {}, - NEW p \in b .. t - 1, - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \union {<>, <

>} - PROVE TypeOK' - <7>1. (A \in [1..N -> Int])' - BY Z3, <6>2 DEF TypeOK, Partitions, PermsOf - <7>2. (U \in SUBSET ((1..N) \X (1..N)))' - BY Z3, <6>2 DEF TypeOK - <7>q QED - (* Why doesn't Z3 prove this?? Surely I don't have to do anything about this? *) - BY <6>2, <7>1, <7>2 - <6>q QED - BY <5>1, <6>1, <6>2 - <5>2 CASE b = t - <6>1 SUFFICES ASSUME TypeOK, U # {}, b = t, - U' = U \ {<>}, - A' = A - PROVE TypeOK' - BY <4>2, <5>2 - <6>2 ASSUME TypeOK, U # {}, b = t, - U' = U \ {<>}, - A' = A - PROVE TypeOK' - <7>1. (A \in [1..N -> Int])' - BY Z3, <6>2 DEF TypeOK - <7>2. (U \in SUBSET ((1..N) \X (1..N)))' - BY Z3, <6>2 DEF TypeOK - <7>q QED - BY <7>1, <7>2 DEF TypeOK - <6>q QED - BY <6>1, <6>2 - <5>q QED - BY <4>2, <5>1, <5>2 - <4>q QED - BY <4>1, <4>2 DEF Next - - <3>2. CASE UNCHANGED vars - <4>q QED - BY <2>2, <3>2 DEF TypeOK, vars - <3>q QED - BY <3>1, <3>2, <2>2 - - <2>3 ASSUME Inv, [Next]_vars - PROVE Safety' - <3>1 CASE UNCHANGED vars - <4>q QED - BY <3>1, <2>3 DEF Inv, vars, Safety - <3>2 CASE Next - <4>1 SUFFICES ASSUME Safety, - U # {}, - \E b \in 1 .. N, t \in 1 .. N : - /\ <> \in U - /\ IF b # t - THEN \E p \in b .. t - 1 : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \union {<>, <

>} - ELSE /\ U' = U \ {<>} - /\ A' = A - PROVE Safety' - BY <2>3, <3>2 DEF Next, Inv - <4>2 ASSUME Safety, - U # {}, - NEW b \in 1 .. N, - NEW t \in 1 .. N, - /\ <> \in U - /\ IF b # t - THEN \E p \in b .. t - 1 : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \union {<>, <

>} - ELSE /\ U' = U \ {<>} - /\ A' = A - PROVE Safety' - <5>1 CASE b # t -(* <6>1 SUFFICES ASSUME TypeOK, - U # {}, - \E p \in b .. t - 1 : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \union {<>, <

>} - PROVE TypeOK' - BY <4>2, <5>1 -*) - - <5>2 CASE b = t - <6>1 SUFFICES ASSUME Safety, - U # {}, - U' = U \ {<>}, - A' = A - PROVE Safety' - BY <4>2, <5>2 DEF Next - - <6>2 ASSUME Safety, - U # {}, - U' = U \ {<>}, - A' = A - PROVE Safety' - <7>1 SUFFICES - /\ ( (A' = A /\ IsSorted(A)) => IsSorted(A') ) - /\ ( ( /\ Safety - /\ U # {} - /\ U' = U \ {<>} - /\ A' = A ) - => (U' = {} => A' \in PermsOf(A0) /\ IsSorted(A') ) - ) - BY DEF Safety - - <7>2 (A' = A /\ IsSorted(A)) => IsSorted(A') - OBVIOUS - <7>3 ( /\ Safety - /\ U # {} - /\ U' = U \ {<>} - /\ A' = A ) - => (U' = {} => A' \in PermsOf(A0) /\ IsSorted(A') ) - BY DEF Safety - - <7>q QED - BY <6>2, <7>1, <7>2, <7>3 - <6>q QED - BY <5>2, <6>1, <6>2 - <5>q QED - <4>q QED - BY <3>2, <2>3 DEF Inv, Safety, Next - <3>q QED - BY <3>1, <3>2, <2>3 - <2>q QED - BY <2>1, <2>2, <2>3 DEF Inv -<1>3 Inv => Safety - <2> QED - BY DEF Inv - -<1>4 QED - BY LS4, <1>1, <1>2, <1>3 DEF Inv, Spec - - - - - - - - - - - - - - - - - - (* Side Notes: - - It is annoying that the parser errors don't wrap around lines and I don't seem to be able to sort windows in the toolbox, so I can have them below the obligations... - - - I typed Ctrl-w (emacs-person that I am) and lost the text window somehow... - - - Why do I not get any interesting obligations, when typing C-g C-g in the following state: -++++++++++ -THEOREM Spec => []Safety - -<1> SUFFICES ASSUME Spec - PROVE []Safety -<1>1 []Safety - -<1> QED - BY <1>1, LS4" -+++++++++++ - ?? - - - The fact that the prover sometimes doesn't launch on C-g C-g is very annoying... - - - Highlighting matching parantheses would be helpful... - - - For some reason my touchpad's righ mouse button doesn't open the menu; - given that the key shortcuts are very unstable, it would be good to - be able to get at things from the main menu - *) - - -============================================================================= - diff --git a/examples_draft/quicksort/Quicksort04.tla b/examples_draft/quicksort/Quicksort04.tla deleted file mode 100755 index a55d04251..000000000 --- a/examples_draft/quicksort/Quicksort04.tla +++ /dev/null @@ -1,292 +0,0 @@ ------------------------------ MODULE Quicksort04 ----------------------------- -(***************************************************************************) -(* This module specifies a Quicksort algorithm for sorting a sequence A of *) -(* length N of integers. *) -(***************************************************************************) -EXTENDS Integers, TLAPS - -CONSTANT A0, N - -ASSUME ConstantAssump == /\ N \in Nat \ {0} - /\ A0 \in [1..N -> Int] - -IsSorted(B) == \A i, j \in 1..N : (i < j) => (B[i] =< B[j]) - -PermsOf(Arr) == - LET Automorphisms(S) == { f \in [S -> S] : - \A y \in S : \E x \in S : f[x] = y } - f ** g == [x \in DOMAIN g |-> f[g[x]]] - IN { Arr ** f : f \in Automorphisms(DOMAIN Arr) } - -Partitions(B, pivot, lo, hi) == - {C \in PermsOf(B) : - /\ \A i \in 1..(lo-1) \cup (hi+1)..N : C[i] = B[i] - /\ \A i \in lo..pivot, j \in (pivot+1)..hi : C[i] =< C[j] } - -VARIABLES A, U - -TypeOK == /\ A \in [1..N -> Int] - /\ U \in SUBSET ((1..N) \X (1..N)) - -vars == <> - -Init == /\ A = A0 - /\ U = { <<1, N>> } - -Next == /\ U # {} - /\ \E b \in 1..N, t \in 1..N : - /\ <> \in U - /\ IF b # t - THEN \E p \in b..(t-1) : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \cup {<>, <>} - ELSE /\ U' = U \ {<>} - /\ A' = A - -Spec == Init /\ [][Next]_vars /\ WF_vars(Next) ------------------------------------------------------------------------------ -Safety == (U = {}) => (A \in PermsOf(A0)) /\ IsSorted(A) -Inv == TypeOK /\ Safety - -(* Ok, I think I got the hang of basic proof structures, - now let's do some logic... - - -*) - -THEOREM Spec => []Safety -<1>1 Init => Inv - PROOF - <2>1 ASSUME Init - PROVE U # {} - BY <2>1 DEF Init - <2>2 SUFFICES (Init => U # {}) /\ (Init => TypeOK) - BY DEF Inv, Safety, TypeOK - <2>3 Init => U # {} - BY DEF Init - <2>4 Init => TypeOK - BY Z3, ConstantAssump DEF Init, TypeOK, ConstantAssump - <2> QED - BY <2>2, <2>3, <2>4 - -<1>2 Inv /\ [Next]_vars => Inv' - <2>1 SUFFICES (TypeOK /\ [Next]_vars => TypeOK') /\ (Inv /\ [Next]_vars => Safety') - BY DEF Inv - <2>2 ASSUME TypeOK, [Next]_vars - PROVE TypeOK' - <3>1. CASE Next (* here I'm trying to decompose and it just quietly does nothing... *) - <4>1 SUFFICES ASSUME TypeOK, - U # {}, - \E b \in 1 .. N, t \in 1 .. N : - /\ <> \in U - /\ IF b # t - THEN \E p \in b .. t - 1 : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \union {<>, <

>} - ELSE /\ U' = U \ {<>} - /\ A' = A - PROVE TypeOK' - BY <2>2, <3>1 DEF Next - <4>2 ASSUME TypeOK, - U # {}, - NEW b \in 1 .. N, - NEW t \in 1 .. N, - /\ <> \in U - /\ IF b # t - THEN \E p \in b .. t - 1 : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \union {<>, <

>} - ELSE /\ U' = U \ {<>} - /\ A' = A - PROVE TypeOK' - <5>1 CASE b # t - <6>1 SUFFICES ASSUME TypeOK, - U # {}, - \E p \in b .. t - 1 : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \union {<>, <

>} - PROVE TypeOK' - BY <4>2, <5>1 - <6>2 ASSUME TypeOK, U # {}, - NEW p \in b .. t - 1, - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \union {<>, <

>} - PROVE TypeOK' - <7>1. (A \in [1..N -> Int])' - BY Z3, <6>2 DEF TypeOK, Partitions, PermsOf - <7>2. (U \in SUBSET ((1..N) \X (1..N)))' - BY Z3, <6>2 DEF TypeOK - <7>q QED - (* Why doesn't Z3 prove this?? Surely I don't have to do anything about this? *) - BY <6>2, <7>1, <7>2 - <6>q QED - BY <5>1, <6>1, <6>2 - <5>2 CASE b = t - <6>1 SUFFICES ASSUME TypeOK, U # {}, b = t, - U' = U \ {<>}, - A' = A - PROVE TypeOK' - BY <4>2, <5>2 - <6>2 ASSUME TypeOK, U # {}, b = t, - U' = U \ {<>}, - A' = A - PROVE TypeOK' - <7>1. (A \in [1..N -> Int])' - BY Z3, <6>2 DEF TypeOK - <7>2. (U \in SUBSET ((1..N) \X (1..N)))' - BY Z3, <6>2 DEF TypeOK - <7>q QED - BY <7>1, <7>2 DEF TypeOK - <6>q QED - BY <6>1, <6>2 - <5>q QED - BY <4>2, <5>1, <5>2 - <4>q QED - BY <4>1, <4>2 DEF Next - - <3>2. CASE UNCHANGED vars - <4>q QED - BY <2>2, <3>2 DEF TypeOK, vars - <3>q QED - BY <3>1, <3>2, <2>2 - - <2>3 ASSUME Inv, [Next]_vars - PROVE Safety' - <3>1 CASE UNCHANGED vars - <4>q QED - BY <3>1, <2>3 DEF Inv, vars, Safety - <3>2 CASE Next - <4>1 SUFFICES ASSUME Inv, - U # {}, - \E b \in 1 .. N, t \in 1 .. N : - /\ <> \in U - /\ IF b # t - THEN \E p \in b .. t - 1 : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \union {<>, <

>} - ELSE /\ U' = U \ {<>} - /\ A' = A - PROVE Safety' - BY <2>3, <3>2 DEF Next, Inv - <4>2 ASSUME Inv, - U # {}, - NEW b \in 1 .. N, - NEW t \in 1 .. N, - /\ <> \in U - /\ IF b # t - THEN \E p \in b .. t - 1 : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \union {<>, <

>} - ELSE /\ U' = U \ {<>} - /\ A' = A - PROVE Safety' - <5>1 CASE b # t -(* <6>1 SUFFICES ASSUME TypeOK, - U # {}, - \E p \in b .. t - 1 : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \union {<>, <

>} - PROVE TypeOK' - BY <4>2, <5>1 -*) - - <5>2 CASE b = t - <6>1 SUFFICES ASSUME Safety, - U # {}, - U' = U \ {<>}, - A' = A - PROVE Safety' - BY <4>2, <5>2 DEF Next, Safety - - <6>2 ASSUME Safety, - U # {}, - U' = U \ {<>}, - A' = A - PROVE Safety' - <7>1 SUFFICES - /\ ( (A' = A /\ IsSorted(A)) => IsSorted(A') ) - /\ ( ( /\ U # {} - /\ U' = U \ {<>} - /\ A' = A ) - => (U' = {} => A' \in PermsOf(A0) /\ IsSorted(A') ) - ) - BY <6>2 DEF Safety - - <7>2 (A' = A /\ IsSorted(A)) => IsSorted(A') - OBVIOUS - <7>3 ( /\ U # {} - /\ U' = U \ {<>} - /\ A' = A ) - => (U' = {} => A' \in PermsOf(A0) /\ IsSorted(A') ) - PROOF - <8>1 CASE U' = {} - <8>2 CASE U' # {} - OBVIOUS (* how is this not obvious ??? *) - <8>q QED - BY <8>1, <8>2 (* putting `<7>3' here give an error "<7>3 used in its own proof..." usually the QED needs to mention its object under a BY?? *) - <7>q QED - BY <6>2, <7>1, <7>2, <7>3 - <6>q QED - BY <5>2, <6>1, <6>2 - <5>q QED - <4>q QED - BY <3>2, <2>3 DEF Inv, Safety, Next - <3>q QED - BY <3>1, <3>2, <2>3 - <2>q QED - BY <2>1, <2>2, <2>3 DEF Inv -<1>3 Inv => Safety - <2> QED - BY DEF Inv - -<1>4 QED - BY LS4, <1>1, <1>2, <1>3 DEF Inv, Spec - - - - - - - - - - - - - - - - - - (* Side Notes: - - It is annoying that the parser errors don't wrap around lines and I don't seem to be able to sort windows in the toolbox, so I can have them below the obligations... - - - I typed Ctrl-w (emacs-person that I am) and lost the text window somehow... - - - Why do I not get any interesting obligations, when typing C-g C-g in the following state: -++++++++++ -THEOREM Spec => []Safety - -<1> SUFFICES ASSUME Spec - PROVE []Safety -<1>1 []Safety - -<1> QED - BY <1>1, LS4" -+++++++++++ - ?? - - - The fact that the prover sometimes doesn't launch on C-g C-g is very annoying... - - - Highlighting matching parantheses would be helpful... - - - For some reason my touchpad's righ mouse button doesn't open the menu; - given that the key shortcuts are very unstable, it would be good to - be able to get at things from the main menu - - - It would be useful to be able to `print' definitions like Safety -- scolling back and forth in the middle of a long proof takes time... - *) - - -============================================================================= - diff --git a/examples_draft/quicksort/Quicksort05.tla b/examples_draft/quicksort/Quicksort05.tla deleted file mode 100755 index 6dbb0d056..000000000 --- a/examples_draft/quicksort/Quicksort05.tla +++ /dev/null @@ -1,361 +0,0 @@ ------------------------------ MODULE Quicksort05 ----------------------------- -(***************************************************************************) -(* This module specifies a Quicksort algorithm for sorting a sequence A of *) -(* length N of integers. *) -(***************************************************************************) -EXTENDS Integers, TLAPS - -CONSTANT A0, N - -ASSUME ConstantAssump == /\ N \in Nat \ {0} - /\ A0 \in [1..N -> Int] - -IsSorted(B) == \A i, j \in 1..N : (i < j) => (B[i] =< B[j]) - -PermsOf(Arr) == - LET Automorphisms(S) == { f \in [S -> S] : - \A y \in S : \E x \in S : f[x] = y } - f ** g == [x \in DOMAIN g |-> f[g[x]]] - IN { Arr ** f : f \in Automorphisms(DOMAIN Arr) } - -Partitions(B, pivot, lo, hi) == - {C \in PermsOf(B) : - /\ \A i \in 1..(lo-1) \cup (hi+1)..N : C[i] = B[i] - /\ \A i \in lo..pivot, j \in (pivot+1)..hi : C[i] =< C[j] } - -VARIABLES A, U - -TypeOK == /\ A \in [1..N -> Int] - /\ U \in SUBSET ((1..N) \X (1..N)) - -vars == <> - -Init == /\ A = A0 - /\ U = { <<1, N>> } - -Next == /\ U # {} - /\ \E b \in 1..N, t \in 1..N : - /\ <> \in U - /\ IF b # t - THEN \E p \in b..(t-1) : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \cup {<>, <>} - ELSE /\ U' = U \ {<>} - /\ A' = A - -Spec == Init /\ [][Next]_vars /\ WF_vars(Next) ------------------------------------------------------------------------------ -Safety == (U = {}) => (A \in PermsOf(A0)) /\ IsSorted(A) -(*Inv == TypeOK /\ Safety *) - -(* Ok, I think I got the hang of basic proof structures, - now let's do some logic... - clearly Safety is not the right invariant, since it is vacuously true as long as U is not empty... - - let's try this instead, which says intuitively "if there are two values in A in the wrong order, - then there is a segment of A which they are both in and which is still on the stack to be sorted": -*) -Inv == /\ TypeOK - /\ A \in PermsOf(A0) - /\ \A i, j \in 1..N : (i < j /\ A[j] < A[i]) - => \E b, t \in 1..N : <> \in U /\ b <= i /\ j <= t - -(* The documentation of WITNESS is very minimal, and the error messages are confusing: - -In the following state, checking step <3>1 generates an obligation -asking me to prove that 1 \in 1..N, under the assumption that - \E t \in 1 .. N : <<1, t>> \in U /\ 1 \leq i /\ j \leq t ?? - - Adding `OBVIOUS' under step <3>1 generates a syntax error ?? - -++++++++++++++++++++++++++++ -THEOREM Spec => []Safety -<1>1 Init => Inv - PROOF - <2>2 SUFFICES (Init => \A i, j \in 1..N : \E b, t \in 1..N : <> \in U /\ b <= i /\ j <= t) - /\ (Init => TypeOK) - BY DEF Inv, TypeOK - <2>3 ASSUME Init, - NEW i \in 1.. N, - NEW j \in 1 .. N - PROVE \E b, t \in 1..N: <> \in U /\ b <= i /\ j <= t - <3>1 WITNESS 1 \in 1..N - <3>2 WITNESS N \in 1..N - <3>q QED - BY <3>1, <3>2, Z3, <2>3 DEF Init - <2>4 Init => TypeOK - BY Z3, ConstantAssump DEF Init, TypeOK, ConstantAssump - <2> QED - BY <2>2, <2>3, <2>4 -... -+++++++++++++++++++++++++ - - -I'm moving to <1>3 for now: - -- This example-oriented documenation is getting cumbersome: If I want to know how to use something I always have to find - and example that uses it. - Right now, for instance, I'd like to know how to prove something by contradiction. - I can either state everything and hope that isabelle finds the contradiction automatically, - however, seeing that that doesn't work with vacuously true implications I'm skeptical... - - what I really want is: - - A list of all proof structures in alphabetical order, with a minimal syntactically correct example of their use. - - A list of all tactics in alphabetical order annotated with the kinds of facts they can prove. - -Right, <1>3 discharged, I'm moving to <1>2: - -- I'll need transitivity of PermsOf.... - -- I'll also restructure the proof so that the case distinction can be shared between <2>2, <2>3, and <2>4 - - -*) - -PermsOf_trans == \A a, b, c \in [1..N -> Int] : (c \in PermsOf(b) /\ b \in PermsOf(a)) => c \in PermsOf(a) -LEMMA PermsOf_trans -<1> ASSUME NEW a\in [1..N -> Int], - NEW b\in [1..N -> Int], - NEW c\in [1..N -> Int], - c \in PermsOf(b), - b \in PermsOf(a) - PROVE c \in PermsOf(a) -<1>q QED - BY DEF PermsOf_trans - -THEOREM Spec => []Safety -<1>1 Init => Inv - PROOF - <2>2 SUFFICES (Init => \A i, j \in 1..N : \E b, t \in 1..N : <> \in U /\ b <= i /\ j <= t) - /\ (Init => TypeOK) - BY DEF Inv, TypeOK - <2>3 ASSUME Init, - NEW i \in 1.. N, - NEW j \in 1 .. N - PROVE \E b, t \in 1..N: <> \in U /\ b <= i /\ j <= t - <3>1 WITNESS 1 \in 1 .. N - <3>2 WITNESS N \in 1..N - <3>q QED - BY <3>1, <3>2, Z3, <2>3 DEF Init - <2>4 Init => TypeOK - BY Z3, ConstantAssump DEF Init, TypeOK, ConstantAssump - <2> QED - BY <2>2, <2>3, <2>4 - -<1>2 Inv /\ [Next]_vars => Inv' - <2>1 SUFFICES (TypeOK /\ [Next]_vars => TypeOK') - /\ (A \in PermsOf(A0) /\ [Next]_vars => A' \in PermsOf(A0)) - /\ (Inv /\ [Next]_vars - => \A i, j \in 1..N : (i < j /\ A'[j] < A'[i]) - => \E b, t \in 1..N : <> \in U' /\ b <= i /\ j <= t) - BY DEF Inv - <2>2 ASSUME TypeOK, [Next]_vars - PROVE TypeOK' - <3>1 CASE UNCHANGED vars - BY <3>1, <2>2 DEF TypeOK, vars (* yet another one where I must mention <2>1 in its own proof... ? *) - <3>2 CASE Next - <4>1 SUFFICES ASSUME TypeOK, U#{}, - NEW b \in 1 .. N, - NEW t \in 1 .. N, - <> \in U, - IF b # t - THEN \E p \in b .. t - 1 : - /\ A' \in Partitions(A, p, b, t) - /\ U'= (U \ {<>}) \union {<>, <

>} - ELSE /\ U' = U \ {<>} - /\ A' = A - PROVE TypeOK' - BY <2>2, <3>1, <4>1 DEF Next (* again, this only goes through when I put <2>2 -- which I'm proving here... ?? *) - <4>2 ASSUME TypeOK, U # {}, -(* For some reason I can't assume NEW b and t here? But the only other place where they are introduced is <4>1? - There is something I'm not getting about scopes of variables... - NEW b \in 1 .. N, - NEW t \in 1 .. N, -*) <> \in U, - IF b # t - THEN \E p \in b .. t - 1 : - /\ A' \in Partitions(A, p, b, t) - /\ U'= (U \ {<>}) \union {<>, <

>} - ELSE /\ U' = U \ {<>} - /\ A' = A - PROVE TypeOK' - <5>1 CASE b = t - BY Z3, <4>2, <5>1 DEF TypeOK - <5>2 CASE b # t - (* this seems like it should be good enough here... ? : BY Z3, <4>2, <5>1 DEF TypeOK *) - <6>1 SUFFICES ASSUME TypeOK, - NEW p \in b .. t-1, - A' \in Partitions(A, p, b, t), - U'= (U \ {<>}) \union {<>, <

>} - PROVE A' \in [1..N-> Int] /\ U' \in SUBSET ((1..N) \X (1..N)) - BY <4>2, <5>2 DEF TypeOK - <6>2 A' \in [1..N -> Int] - BY <6>1, Z3 DEF TypeOK, Partitions, PermsOf (* aha, Z3 can prove this!! *) - <6>3 U' \in SUBSET ((1..N) \X (1..N)) -(* BY <6>1, Z3 DEF TypeOK (* then why can't it prove this ?!? *) *) - <7>1 SUFFICES {<>, <>} \in SUBSET ((1..N) \X (1..N)) - BY <6>1 DEF TypeOK - <7>2 {<>, <>} \in SUBSET ((1..N) \X (1..N)) - (* And why doesn't Z3 prove this one ... ?*) - <8>1 SUFFICES <> \in (1..N) \X (1..N) - /\ <> \in (1..N) \X (1..N) - OBVIOUS - (* How is this not obvious when the above is ????? - <8>1 SUFFICES b \in 1.. N - /\ p \in 1..N - /\ p+1 \in 1..N - /\ t \in 1..N - OBVIOUS - *) - (* Now this gives me a Parse Error: "Encountered "<8>3" at line ... in moduel Quicksort05" ??? - <8>2 < \in (1..N) \X (1..N) - <8>3 <> \in (1..N) \X (1..N) - *) - <8>2 <> \in (1..N) \X (1..N) - <9>1 SUFFICES b \in 1..N /\ p \in 1..N - OBVIOUS - <9>2 b \in 1..N - OBVIOUS - <9>3 p \in 1..N - (* BY Z3 Honestly, this is not clear ??? *) - <10>1 SUFFICES 1 <= b /\ t - 1 <= N - BY Z3 (* I Give Up *) - <10>2 1 <= b - BY Z3 - <10>3 t-1 <= N (* again, I think this should just be `BY Z3' ?? *) - <11>1 SUFFICES t <= N - BY Z3 (* ??? *) - <11>2 t <= N - BY Z3 - <11>q QED - BY <11>1, <11>2 - <10>q QED - BY <10>1, <10>2, <10>3 - <9>q QED - BY <9>1, <9>2, <9>3 - <8>3 <> \in (1..N) \X (1..N) - <9>1 SUFFICES p+1 \in 1..N /\ t \in 1..N - OBVIOUS - <9>2 t \in 1..N - OBVIOUS - <9>3 p+1 \in 1..N (* when <8>2 is solved, copy, paste & tweak... *) - <9>q QED - BY <9>1, <9>2, <9>3 - <8>q QED - BY <8>1, <8>2, <8>3 - <7>q QED - BY <7>1, <7>2 - <6>q QED - BY <6>1, <6>2, <6>3 - <5>q QED - BY <5>1, <5>2 - <4>q QED - BY <4>1, <4>2 - <3>q QED - BY <3>1, <3>2, <2>2 (* this is a case where I must mention <2>2 in its own proof... ?? *) - <2>3 ASSUME A \in PermsOf(A0), [Next]_vars - PROVE A' \in PermsOf(A0) - <3>1 CASE UNCHANGED vars - BY <2>3 DEF vars (* what is the tactic that will get this done ? (I'm assuming there is one...?) *) - <3>2 CASE Next - - - - - - - BY PermsOf_trans, <2>3, <3>2 DEF vars, PermsOf_trans, Next - - <3>q QED - BY <3>1, <3>2, <2>3 - <2>4 ASSUME Inv, [Next]_vars - PROVE \A i, j \in 1..N : (i < j /\ A'[j] < A'[i]) - => \E b, t \in 1..N : <> \in U' /\ b <= i /\ j <= t - <2>q QED - BY <2>1, <2>2, <2>3, <2>4 - -<1>3 Inv => Safety - <2>1 SUFFICES ASSUME Inv, U = {} - PROVE A \in PermsOf(A0) /\ IsSorted(A) - BY DEF Safety - <2>2 ASSUME Inv - PROVE A \in PermsOf(A0) - BY <2>2 DEF Inv - <2>3 ASSUME Inv, - U = {}, - NEW i \in 1..N, - NEW j \in 1..N, - i < j - PROVE A[i] \leq A [j] - <3>1 ~ (A[j] < A[i]) \/ \E b, t \in N : <> \in U /\ b <= i /\ j <= t - BY <2>3 DEF Inv - <3>2 ~ \E b, t \in N : <> \in U /\ b <= i /\ j <= t - BY <2>3 - <3>3 ~(A[j] < A[i]) => A[i] \leq A[j] - BY Z3 - <3>4 ~(A[j] < A[i]) - BY <3>1, <3>2 - <3>q QED - BY <2>2, <3>3, <3>4 DEF Inv, IsSorted - <2>q QED - BY <2>1, <2>2, <2>3 DEF IsSorted - - -<1>4 QED - BY LS4, <1>1, <1>2, <1>3 DEF Inv, Spec - - - - - - - - - - - - - - - - - - (* Side Notes: - - It is annoying that the parser errors don't wrap around lines and I don't seem to be able to sort windows in the toolbox, so I can have them below the obligations... - - - I typed Ctrl-w (emacs-person that I am) and lost the text window somehow... - - - Why do I not get any interesting obligations, when typing C-g C-g in the following state: -++++++++++ -THEOREM Spec => []Safety - -<1> SUFFICES ASSUME Spec - PROVE []Safety -<1>1 []Safety - -<1> QED - BY <1>1, LS4" -+++++++++++ - ?? - - - The fact that the prover sometimes doesn't launch on C-g C-g is very annoying... - - - Highlighting matching parantheses would be helpful... - - - For some reason my touchpad's righ mouse button doesn't open the menu; - given that the key shortcuts are very unstable, it would be good to - be able to get at things from the main menu - - - It would be useful to be able to `print' definitions like Safety -- scolling back and forth in the middle of a long proof takes time... - - - the little `+' and `-' in the sidebar to hide parts of the proof appears and disappears apparently randomly... ? - - - It is not clear to me at all, when I'm allowed to mention somethething in its own proof and when not. - e.g. in step <1>3 - <2>2 I have to put `<2>2' under the `BY' in order for it to go through ... - - - *) - - -============================================================================= - diff --git a/examples_draft/quicksort/Quicksort06.tla b/examples_draft/quicksort/Quicksort06.tla deleted file mode 100755 index 33221b08f..000000000 --- a/examples_draft/quicksort/Quicksort06.tla +++ /dev/null @@ -1,270 +0,0 @@ ------------------------------ MODULE Quicksort06 ----------------------------- -(***************************************************************************) -(* This module specifies a Quicksort algorithm for sorting a sequence A of *) -(* length N of integers. *) -(***************************************************************************) -EXTENDS Integers, TLAPS - -CONSTANT A0, N - -ASSUME ConstantAssump == /\ N \in Nat \ {0} - /\ A0 \in [1..N -> Int] - -IsSorted(B) == \A i, j \in 1..N : (i < j) => (B[i] =< B[j]) - -PermsOf(Arr) == - LET Automorphisms(S) == { f \in [S -> S] : - \A y \in S : \E x \in S : f[x] = y } - f ** g == [x \in DOMAIN g |-> f[g[x]]] - IN { Arr ** f : f \in Automorphisms(DOMAIN Arr) } - -Partitions(B, pivot, lo, hi) == - {C \in PermsOf(B) : - /\ \A i \in 1..(lo-1) \cup (hi+1)..N : C[i] = B[i] - /\ \A i \in lo..pivot, j \in (pivot+1)..hi : C[i] =< C[j] } - -VARIABLES A, U - -TypeOK == /\ A \in [1..N -> Int] - /\ U \in SUBSET ((1..N) \X (1..N)) - -vars == <> - -Init == /\ A = A0 - /\ U = { <<1, N>> } - -Next == /\ U # {} - /\ \E b \in 1..N, t \in 1..N : - /\ <> \in U - /\ IF b # t - THEN \E p \in b..(t-1) : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \cup {<>, <>} - ELSE /\ U' = U \ {<>} - /\ A' = A - -Spec == Init /\ [][Next]_vars /\ WF_vars(Next) ------------------------------------------------------------------------------ -Safety == (U = {}) => (A \in PermsOf(A0)) /\ IsSorted(A) - -Inv_aux == \A i, j \in 1..N : (i < j /\ A[j] < A[i]) - => \E b, t \in 1..N : <> \in U /\ b <= i /\ j <= t - - -Inv == /\ TypeOK - /\ A \in PermsOf(A0) - /\ Inv_aux - - -LEMMA PermsOf_trans == \A a, b, c \in [1..N -> Int] : (c \in PermsOf(b) /\ b \in PermsOf(a)) => c \in PermsOf(a) -<1> ASSUME NEW a\in [1..N -> Int], - NEW b\in [1..N -> Int], - NEW c\in [1..N -> Int], - c \in PermsOf(b), - b \in PermsOf(a) - PROVE c \in PermsOf(a) - BY DEF PermsOf_trans, PermsOf -<1>q QED - BY DEF PermsOf_trans, PermsOf - -LEMMA TRUE BY Isa - -LEMMA PermsOf_refl == \A a \in [1..N -> Int] : a \in PermsOf(a) - BY DEF PermsOf_refl, PermsOf - -THEOREM Spec => []Safety -<1>1 Init => Inv - PROOF - <2>2 SUFFICES (Init => A \in PermsOf(A0)) - /\ (Init => TypeOK) - /\ (Init => Inv_aux) - BY DEF Inv, TypeOK - <2>3 ASSUME Init, - NEW i \in 1.. N, - NEW j \in 1 .. N - PROVE \E b, t \in 1..N: <> \in U /\ b <= i /\ j <= t - - <3>1 <<1,N>> \in U /\ 1 <= i /\ j <= N - BY <2>3, CVC3 DEF Init - <3>q QED - BY <3>1, Z3, ConstantAssump - <2>4 Init => TypeOK - BY Z3, ConstantAssump DEF Init, TypeOK, ConstantAssump - <2>5 Init => A \in PermsOf(A0) - BY PermsOf_refl, Z3, ConstantAssump DEF Init, PermsOf_refl - <2>q QED - BY <2>2, <2>3, <2>4, <2>5 DEF Inv_aux - -<1>2 Inv /\ [Next]_vars => Inv' - <2>1 SUFFICES (Inv /\ [Next]_vars) - => ( TypeOK' - /\ A' \in PermsOf(A0) - /\ Inv_aux' ) - BY DEF Inv - <2>2 ASSUME Inv, [Next]_vars - PROVE TypeOK' /\ A' \in PermsOf(A0) /\ Inv_aux' - <3> USE Inv - <3> USE ConstantAssump - <3>1 CASE UNCHANGED vars - <4>1 TypeOK' - BY <2>2, <3>1 DEF Inv, TypeOK, vars - <4>2 A' \in PermsOf(A0) - BY <2>2, <3>1 DEF Inv, vars - <4>3 Inv_aux' - BY <2>2, <3>1 DEF Inv, Inv_aux, vars - <4>q QED - BY <4>1, <4>2, <4>3, <3>1 - <3>2 CASE Next - <4>1 ASSUME U # {}, - NEW b \in 1..N, - NEW t \in 1..N, - IF b # t - THEN \E p \in b..(t-1) : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \cup {<>, <>} - ELSE /\ U' = U \ {<>} - /\ A' = A - PROVE TypeOK' /\ A' \in PermsOf(A0) /\ Inv_aux' - <5>1 CASE b = t - (* I tried to do the following here, but got an error: - +++++++++++++++ - <6> HAVE A' = A - <6> HAVE U' = U \ {<>} - --------------- -" Error: this HAVE step is applied to the following goal, which is not an implication: - vars' /\ U' \in Partitions(N) /\ Inv' " - - The guide explainst that I can only HAVE things when the current goal is an implication. - Why is the current goal not equal to "TypeOK' /\ A' \in PermsOf(A0) /\ Inv_aux'" though? - - *) - <6>1 A' = A - BY <4>1, <5>1 - <6>2 U' = U \ {<>} - BY <4>1, <5>1 - <6>3 TypeOK' - BY <4>1, <6>1, <6>2 DEF TypeOK, Inv - <6>4 A' \in PermsOf(A0) - BY <6>1, PermsOf_trans DEF PermsOf_trans, ConstantAssump, Inv - <6>5 Inv_aux' - BY DEF Inv_aux, Inv - <6>q QED - BY <6>3, <6>4, <6>5, <5>1 - <5>2 CASE b # t - <6>1 TypeOK' - <6>2 A' \in PermsOf(A0) - <6>3 Inv_aux' - <6>q QED - BY <6>1, <6>2, <6>3, <5>2 - <5>q QED - BY <5>1, <5>2 - <4>q QED - BY <4>1, <3>2, <2>2 DEF Next - <3>q QED - BY <3>1, <3>2, <2>2 DEF Inv - <2>q QED - BY <2>1, <2>2 - - -<1>3 Inv => Safety - <2>1 SUFFICES ASSUME Inv, U = {} - PROVE A \in PermsOf(A0) /\ IsSorted(A) - BY DEF Safety - <2>2 A \in PermsOf(A0) - BY <2>1 DEF Inv - <2>3 ASSUME NEW i \in 1..N, - NEW j \in 1..N, - i < j - PROVE A[i] \leq A [j] - <3>1 ~ (A[j] < A[i]) \/ \E b, t \in N : <> \in U /\ b <= i /\ j <= t - BY <2>1, <2>3 DEF Inv, Inv_aux - <3>2 ~ \E b, t \in N : <> \in U /\ b <= i /\ j <= t - BY <2>1 - <3>q QED BY <3>1, <3>2, <2>3, Z3 DEF Inv, TypeOK - <2>q QED - BY <2>1, <2>2, <2>3 DEF IsSorted -(* -<1>3 Inv => Safety - <2>1 SUFFICES ASSUME Inv, U = {} - PROVE A \in PermsOf(A0) /\ IsSorted(A) - BY DEF Safety - <2>2 ASSUME Inv - PROVE A \in PermsOf(A0) - BY <2>2 DEF Inv - <2>3 ASSUME Inv, - U = {}, - NEW i \in 1..N, - NEW j \in 1..N, - i < j - PROVE A[i] \leq A [j] - <3>1 ~ (A[j] < A[i]) \/ \E b, t \in N : <> \in U /\ b <= i /\ j <= t - BY <2>3 DEF Inv, Inv_aux - <3>2 ~ \E b, t \in N : <> \in U /\ b <= i /\ j <= t - BY <2>3 - <3>3 ~(A[j] < A[i]) => A[i] \leq A[j] - BY Z3 - <3>4 ~(A[j] < A[i]) - BY <3>1, <3>2 - <3>q QED - BY <2>3, <3>4, Z3 DEF Inv, TypeOK - <2>q QED - BY <2>1, <2>2, <2>3 DEF IsSorted -*) -<1>4 QED - BY LS4, <1>1, <1>2, <1>3 DEF Inv, Spec - - - - - - - - - - - - - - - - - - (* Side Notes: - - It is annoying that the parser errors don't wrap around lines and I don't seem to be able to sort windows in the toolbox, so I can have them below the obligations... - - - I typed Ctrl-w (emacs-person that I am) and lost the text window somehow... - - - Why do I not get any interesting obligations, when typing C-g C-g in the following state: -++++++++++ -THEOREM Spec => []Safety - -<1> SUFFICES ASSUME Spec - PROVE []Safety -<1>1 []Safety - -<1> QED - BY <1>1, LS4" -+++++++++++ - ?? - - - The fact that the prover sometimes doesn't launch on C-g C-g is very annoying... - - - Highlighting matching parantheses would be helpful... - - - For some reason my touchpad's righ mouse button doesn't open the menu; - given that the key shortcuts are very unstable, it would be good to - be able to get at things from the main menu - - - It would be useful to be able to `print' definitions like Safety -- scolling back and forth in the middle of a long proof takes time... - - - the little `+' and `-' in the sidebar to hide parts of the proof appears and disappears apparently randomly... ? - - - It is not clear to me at all, when I'm allowed to mention somethething in its own proof and when not. - e.g. in step <1>3 - <2>2 I have to put `<2>2' under the `BY' in order for it to go through ... - - - *) - - -============================================================================= - diff --git a/examples_draft/quicksort/Quicksort07.tla b/examples_draft/quicksort/Quicksort07.tla deleted file mode 100644 index 6b44ecd2f..000000000 --- a/examples_draft/quicksort/Quicksort07.tla +++ /dev/null @@ -1,690 +0,0 @@ ------------------------------ MODULE Quicksort07 ----------------------------- -(***************************************************************************) -(* This module specifies a Quicksort algorithm for sorting a sequence A of *) -(* length N of integers. *) -(***************************************************************************) -EXTENDS Integers, TLAPS, FiniteSetTheorems, Utils, Bags - -CONSTANT A0, N - -ASSUME ConstantAssump == /\ N \in Nat \ {0} - /\ A0 \in [1..N -> Int] - -IsSorted(B) == \A i, j \in 1..N : -(i < j) => (B[i] =< B[j]) - -PermsOf(Arr) == - LET Automorphisms(S) == { f \in [S -> S] : \A y \in S : \E x \in S : f[x] = y } - - f ** g == [x \in DOMAIN g |-> f[g[x]]] - - IN { Arr ** f : f \in Automorphisms(DOMAIN Arr) } - - -Partitions(B, pivot, lo, hi) == -{ C \in [1..N -> Int] : - /\ (\E D \in PermsOf([i \in lo..hi |-> B[i]]) : C = [i \in 1..N |-> IF i \in lo..hi - THEN D[i] - ELSE B[i] ] ) - /\ \A i \in lo..pivot, j \in (pivot+1)..hi : C[i] =< C[j] - } -(* {C \in PermsOf(B) : - /\ \A i \in 1..(lo-1) \cup (hi+1)..N : C[i] = B[i] - /\ \A i \in lo..pivot, j \in (pivot+1)..hi : C[i] =< C[j] } -*) - - -VARIABLES A, U - -TypeOK == /\ A \in [1..N -> Int] - /\ U \in SUBSET ((1..N) \X (1..N)) - -vars == <> - -Init == /\ A = A0 - /\ U = { <<1, N>> } - -Next == /\ U # {} - /\ \E b \in 1..N, t \in 1..N : - /\ <> \in U - /\ IF b # t - THEN \E p \in b..(t-1) : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \cup {<>, <>} - ELSE /\ U' = U \ {<>} - /\ A' = A - -Spec == Init /\ [][Next]_vars /\ WF_vars(Next) ------------------------------------------------------------------------------ - -LEMMA EverythingIsFinite_1N == \A X : IsFiniteSet({X[k] : k \in 1..N}) - <1> SUFFICES ASSUME NEW X - PROVE (*IsFiniteSet({X[i] : i \in 1..N})*) - ExistsSurjection(1..N, {X[k] : k \in 1..N}) - BY ConstantAssump, N \in Nat, FS_NatSurjection - <1> DEFINE Thing == {X[k] : k \in 1..N} - <1> DEFINE W == Restrict(X, 1..N) - - <1>1 W \in Surjection(1..N, Thing) - BY DEF Restrict, Surjection - - - <1>q QED - BY <1>1 DEF ExistsSurjection - -LEMMA EverythingIsFinite == \A X : \A i, j \in 1..N : IsFiniteSet({X[k] : k \in i..j}) - <1> SUFFICES ASSUME NEW X, - NEW i \in 1..N, - NEW j \in 1..N - PROVE IsFiniteSet({X[k] : k \in i..j}) - OBVIOUS - <1> DEFINE S == {X[k] : k \in 1..N} - <1> DEFINE T == {X[k] : k \in i..j} - <1>1 T \in SUBSET S - <2> SUFFICES ASSUME NEW k \in i..j - PROVE k \in 1..N - OBVIOUS - <2>q QED - BY ConstantAssump, SMT - <1>2 IsFiniteSet(S) - BY EverythingIsFinite_1N - <1>q QED - BY <1>1, <1>2, FS_Subset - - - - -Safety == (U = {}) => (A \in PermsOf(A0)) /\ IsSorted(A) - -(* Inv_aux := If there are two positions i,j that point to values which are not sorted, - then they will be sorted (i.e. there is a pair on the stack that has both i and j in range). *) -Inv_aux == \A i, j \in 1..N : (i < j /\ A[j] < A[i]) - => \E b, t \in 1..N : <> \in U /\ b <= i /\ j <= t - - -Inv == /\ TypeOK - /\ A \in PermsOf(A0) - /\ Inv_aux - - - -(* NoOverlap := There is no overlap on the stack ever: *) -NoOverlap == \A a,b \in 1..N : <> \in U => \A i \in a..b : \A c,d \in 1..N : <> \in U \ {<>} => ~ i \in c..d -LEMMA NO == Spec => []NoOverlap -<1>1 Init => NoOverlap - BY DEF Init, NoOverlap - -<1>2 ASSUME NoOverlap, [Next]_vars - PROVE NoOverlap' - <2> NoOverlap - BY <1>2 - <2>1 CASE UNCHANGED vars - BY <2>1 DEF vars, NoOverlap - - <2>2 CASE Next - <3> USE Next - <3>0 PICK b,t \in 1..N : Next!2!(b,t) - BY DEF Next - - - <3>1 ASSUME b # t, - \E p \in b .. t - 1 : - /\ A' \in Partitions(A, p, b, t) - /\ U' = - (U \ {<>}) \union - {<>, <

>} - PROVE NoOverlap' - <4> USE b # t (* why can I do this here, even though <3>1 has a name?? *) - <4> SUFFICES ASSUME NEW a \in (1..N), NEW e \in (1..N), - <> \in U', - NEW i \in (a..e), - NEW c \in (1..N), NEW d \in (1..N), - <> \in U' \ {<>} - PROVE ~ i \in c..d - BY DEF NoOverlap - <4>1 PICK p \in b..t : Next!2!(b,t)!2!2!(p) - BY <3>0, <3>1 DEF Next - <4> U' = (U \ {<>}) \union {<> , <>} - BY <4>1 - <4> <> \in U - BY <3>0 - - <4>2 CASE <> \in U \ {<>} - <5> USE <> \in U \ {<>} - <5>1 \A k, l \in 1 .. N : - <> \in U \ {<>} => \neg i \in k .. l - BY ZenonT(30) DEF NoOverlap (*fragile timeout here... if it doesn't work, try 40 *) - <5>2 CASE <> \in U \ {<>} - BY <5>1, <5>2 - - <5>3 CASE <> = <> \/ <> = <> - <6> USE <5>3 - <6>1 <> \in U \ {<>} - OBVIOUS - <6> ~ i \in b..t - BY DEF NoOverlap - - <6>q QED - OBVIOUS - - <5>q QED - BY <5>2, <5>3 DEF NoOverlap - - <4>3 CASE <> = <> \/ <> = <> - <5> USE <4>3 - - <5>1 CASE <> \in U \ {<>} - <6> USE <5>1 - <6>2 i \in b..t - OBVIOUS - <6>q QED - BY ONLY <> \in U, NoOverlap, <6>2, <5>1, Zenon DEF NoOverlap - - <5>2 CASE <> = <> \/ <> = <> - <6> USE <5>2 - <6>q QED - OBVIOUS - - <5>q QED - BY <5>1, <5>2 - - - - <4>q QED - BY <4>1, <4>2, <4>3 DEF NoOverlap - - - <3>2 ASSUME b = t, - U' = U \ {<>} /\ A' = A - PROVE NoOverlap' - <4> SUFFICES ASSUME NEW a \in (1..N), NEW e \in (1..N), - <> \in U', - NEW i \in (a..e), - NEW c \in (1..N), NEW d \in (1..N), - <> \in U' \ {<>} - PROVE ~ i \in c..d - BY DEF NoOverlap - <4>q QED - BY <3>2 DEF NoOverlap - - - - - <3>q QED - BY <3>1, <3>2, <3>0 DEF Next - - <2>q QED - BY <2>1, <2>2, <1>2 - -<1>q QED - BY LS4, <1>1, <1>2 DEF Spec - - -LEMMA Partitions_PermsOf == \A B, C \in [1..N -> Int] : \A p, l, h \in 1..N : - C \in Partitions(B, p, l, h) => C \in PermsOf(B) - <1> USE ConstantAssump - <1> SUFFICES ASSUME NEW B \in [1..N -> Int], - NEW C \in [1..N -> Int], - NEW p \in 1..N, - NEW l \in 1..N, - NEW h \in 1..N, - C \in Partitions(B, p, l, h) - PROVE \E f \in [1..N -> 1..N] : /\ (\A y \in 1..N : \E x \in 1..N : f[x] = y) - /\ C = [i \in 1..N |-> B[f[i]]] - BY Isa DEF PermsOf - <1>1 PICK D \in PermsOf([i \in l..h |-> B[i]]) : C = [i \in 1..N |-> IF i \in l..h - THEN D[i] - ELSE B[i] ] - BY Isa DEF Partitions - <1>2 \A i \in l..h : C[i] = D[i] - BY <1>1 (* why not??? *) - <1>3 PICK g \in [l..h -> l..h] : (\A y \in l..h : \E x \in l..h : g[x] = y) - /\ D = [x \in l..h |-> B[g[x]]] - BY DEF PermsOf - <1> DEFINE w == [i \in 1..N |-> IF i \in l..h THEN g[i] ELSE i] - <1> w \in [1..N -> 1..N] - OBVIOUS - <1> ASSUME NEW y \in 1..N - PROVE \E x \in 1..N : w[x] = y - - <2> CASE y \in l..h - <3> PICK x \in l..h : g[x] = y - BY <1>3 - <3> x \in Int (* so it actually needed this to get the Witness statement below green... *) - OBVIOUS - <3> WITNESS x \in 1..N - <3>q QED - BY w[x] = g[x] - - <2> CASE ~ y \in l..h - OBVIOUS - <2>q QED - OBVIOUS - - <1> C = [i \in 1..N |-> B[w[i]]] - <2> SUFFICES ASSUME NEW i \in 1..N - PROVE C[i] = B[w[i]] - OBVIOUS - <2> CASE i \in l..h - BY <1>3, <1>2 - <2> CASE ~ i \in l..h - BY w[i] = i DEF Partitions - <2>q QED - OBVIOUS - - - <1> QED - OBVIOUS - - -(* PermsOfSetStable := Permuting does not affect the set of values in an array *) -LEMMA PermsOfSetStable == \A b, t \in 1..N : \A B, C \in [b..t -> Int] : C \in PermsOf(B) => {C[k] : k \in b..t} = {B[k] : k \in b..t} - <1> SUFFICES ASSUME NEW b \in 1..N, - NEW t \in 1..N, - NEW B \in [b..t -> Int], - NEW C \in [b..t -> Int], - C \in PermsOf(B) - PROVE {C[k] : k \in b..t} = {B[k] : k \in b..t} - OBVIOUS - - <1>1 ASSUME NEW x \in {C[k] : k \in b..t} - PROVE x \in {B[k] : k \in b..t} - <2> PICK f \in [b..t -> b..t] : (\A y \in b..t : \E z \in b..t : f[z] = y) - /\ C = [i \in b..t |-> B[f[i]]] - BY Isa DEF PermsOf - <2> PICK i \in b..t : x = C[i] - BY <1>1 - <2> x = B[f[i]] - OBVIOUS - <2>q QED - OBVIOUS - - <1>2 ASSUME NEW x \in {B[k] : k \in b..t} (* surprisingly, here, the actuallly copied and pasted proof from <1>1 works... maybe it's not surprising, but I was surprised...*) - PROVE x \in {C[k] : k \in b..t} - <2> PICK f \in [b..t -> b..t] : (\A y \in b..t : \E z \in b..t : f[z] = y) - /\ C = [i \in b..t |-> B[f[i]]] - BY Isa DEF PermsOf - <2> PICK i \in b..t : x = C[i] - BY <1>1 - <2> x = B[f[i]] - OBVIOUS - <2>q QED - OBVIOUS - - <1> QED - BY <1>1, <1>2 - -(* PartitionsSetStable := Partitions does not affect the set of values between lo and hi - -*) -LEMMA PartitionsSetStable == \A B, C \in [1..N -> Int] : \A b, p, t \in 1..N : - C \in Partitions(B, p, b, t) => {C[k] : k \in b..t} = {B[k] : k \in b..t} - <1> SUFFICES ASSUME NEW B \in [1..N -> Int], - NEW C \in [1..N -> Int], - NEW b \in 1..N, - NEW p \in 1..N, - NEW t \in 1..N, - C \in Partitions(B, p, b, t) - PROVE {C[k] : k \in b..t} = {B[k] : k \in b..t} - OBVIOUS - - <1> USE ConstantAssump - <1> DEFINE Cbt == [i \in b..t |-> C[i]] - <1> DEFINE Bbt == [i \in b..t |-> B[i]] - - <1>4 Cbt \in PermsOf(Bbt) - <2> PICK D \in PermsOf(Bbt) : C = [i \in 1 .. N |-> IF i \in b .. t THEN D[i] ELSE B[i]] - BY DEF Partitions - <2>1 ASSUME NEW i \in b..t - PROVE C[i] = D[i] - OBVIOUS - <2> D \in [b..t -> Int] - BY DEF PermsOf - <2> Cbt = D - BY <2>1 - <2>q QED - OBVIOUS - <1>5 \A X, Y \in [b..t -> Int] : Y \in PermsOf(X) => {Y[k] : k \in b..t} = {X[k] : k \in b..t} (* So Zenon is quite sensitive to the order of quantifiers : switching X and Y around under the \A will break this...*) - BY PermsOfSetStable, Zenon - <1>8 {Cbt[k] : k \in b..t} = {Bbt[k] : k \in b..t} - BY Cbt \in [b..t -> Int], Bbt \in [b..t -> Int], <1>4, <1>5, Zenon - <1>6 {C[k] : k \in b..t} = {Cbt[k] : k \in b..t} - OBVIOUS - <1>7 {B[k] : k \in b..t} = {Bbt[k] : k \in b..t} - OBVIOUS - - <1> QED - BY <1>8, <1>6, <1>7 - - - - -LEMMA PermsOf_trans == \A a, b, c \in [1..N -> Int] : (c \in PermsOf(b) /\ b \in PermsOf(a)) => c \in PermsOf(a) -<1> ASSUME NEW a \in [1..N -> Int], - NEW b \in [1..N -> Int], - NEW c \in [1..N -> Int], - c \in PermsOf(b), - b \in PermsOf(a) - PROVE c \in PermsOf(a) - <2>1 PICK f \in [1..N -> 1..N] : - (\A y \in 1..N : \E x \in 1..N : f[x] = y) - /\ (c = [x \in 1..N |-> b[f[x]]]) - BY Isa DEF PermsOf - <2>2 PICK g \in [1..N -> 1..N] : - (\A y \in 1..N : \E x \in 1..N : g[x] = y) - /\ (b = [x \in 1..N |-> a[g[x]]]) - BY Isa DEF PermsOf - <2> SUFFICES ASSUME TRUE - PROVE \E h \in [1..N -> 1..N] : - (\A y \in 1..N : \E x \in 1..N : h[x] = y) - /\ (c = [x \in 1..N |-> a[h[x]]]) - BY Isa DEF PermsOf - <2> DEFINE h == [k \in 1..N |-> g[f[k]]] - <2>3 WITNESS h \in [1..N -> 1..N] - - <2>4 ASSUME NEW y \in 1..N - PROVE \E x \in 1..N : h[x] = y - <3> PICK i \in 1..N : g[i] = y - BY <2>2 - <3> PICK j \in 1..N : f[j] = i - BY <2>1 - <3>q QED - OBVIOUS - - <2>5 c = [x \in 1..N |-> a[h[x]]] - BY <2>1, <2>2 - - <2>q QED - BY <2>3, <2>4, <2>5 -<1>q QED - OBVIOUS - - -LEMMA PermsOf_refl == \A a \in [1..N -> Int] : a \in PermsOf(a) - BY DEF PermsOf_refl, PermsOf - -THEOREM Spec => []Safety -<1>1 Init => Inv - PROOF - <2>2 SUFFICES (Init => A \in PermsOf(A0)) - /\ (Init => TypeOK) - /\ (Init => Inv_aux) - BY DEF Inv, TypeOK - <2>3 ASSUME Init, - NEW i \in 1.. N, - NEW j \in 1 .. N - PROVE \E b, t \in 1..N: <> \in U /\ b <= i /\ j <= t - - <3>1 <<1,N>> \in U /\ 1 <= i /\ j <= N - BY <2>3, CVC3 DEF Init - <3>q QED - BY <3>1, Z3, ConstantAssump - <2>4 Init => TypeOK - BY Z3, ConstantAssump DEF Init, TypeOK, ConstantAssump - <2>5 Init => A \in PermsOf(A0) - BY PermsOf_refl, Z3, ConstantAssump DEF Init, PermsOf_refl - <2>q QED - BY <2>2, <2>3, <2>4, <2>5 DEF Inv_aux - -<1>2 NoOverlap /\ [Next]_vars /\ Inv => Inv' - <2>1 SUFFICES ( NoOverlap /\ Inv /\ [Next]_vars) - => ( TypeOK' - /\ A' \in PermsOf(A0) - /\ Inv_aux' ) - BY DEF Inv - <2>2 ASSUME Inv, [Next]_vars, NoOverlap - PROVE TypeOK' /\ A' \in PermsOf(A0) /\ Inv_aux' - <3> Inv BY <2>2 - <3> USE ConstantAssump - <3> USE NoOverlap - <3>1 CASE UNCHANGED vars - <4>1 TypeOK' - BY <2>2, <3>1 DEF Inv, TypeOK, vars - <4>2 A' \in PermsOf(A0) - BY <2>2, <3>1 DEF Inv, vars - <4>3 Inv_aux' - BY <2>2, <3>1 DEF Inv, Inv_aux, vars - <4>q QED - BY <4>1, <4>2, <4>3, <3>1 - <3>2 CASE Next - <4> USE Next - <4>1 ASSUME U # {}, - NEW b \in 1..N, - NEW t \in 1..N, - <> \in U, - IF b # t - THEN \E p \in b..(t-1) : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \cup {<>, <>} - ELSE /\ U' = U \ {<>} - /\ A' = A - PROVE TypeOK' /\ A' \in PermsOf(A0) /\ Inv_aux' - <5> USE U # {} - <5> USE <> \in U - <5>1 CASE b = t - <6> USE b = t - <6> A' = A - BY <4>1 - <6> U' = U \ {<>} - BY <4>1 - <6>3 TypeOK' - BY DEF TypeOK, Inv - <6>4 A' \in PermsOf(A0) - BY PermsOf_trans DEF PermsOf_trans, ConstantAssump, Inv - <6>5 Inv_aux' - BY DEF Inv_aux, Inv (* ha, that's very nice, I was expecting this to be work... *) - <6>q QED - BY <6>3, <6>4, <6>5, <5>1 - <5>2 CASE b # t - <6> USE b # t - <6> SUFFICES ASSUME NEW p \in b..(t-1), - A' \in Partitions(A, p, b, t), - U' = (U \ {<>}) \cup {<>, <>} - PROVE TypeOK' /\ A' \in PermsOf(A0) /\ Inv_aux' - BY <4>1 - <6>1 TypeOK' - <7> U' \in SUBSET ( (1..N) \X (1..N) ) - <8> SUFFICES U \ {<>} \in SUBSET ((1..N) \X (1..N)) - /\ {<>, <>} \in SUBSET ((1..N) \X (1..N)) - - OBVIOUS - <8>1 U \ {<>} \in SUBSET ((1..N) \X (1..N)) - BY SMT DEF Inv, TypeOK - <8>2 {<>, <>} \in SUBSET ((1..N) \X (1..N)) - BY SMT - <8>q QED - BY <8>1, <8>2 - <7> A' \in [1..N -> Int] - BY SMT DEF Inv, TypeOK, Partitions, PermsOf - <7>q QED - BY DEF TypeOK - <6>2 A' \in PermsOf(A0) - <7> SUFFICES A' \in PermsOf(A) - BY PermsOf_trans, <6>1 DEF Inv, TypeOK - - <7>q QED - BY <6>1, Partitions_PermsOf DEF TypeOK, Inv - - <6>3 Inv_aux' - <7> p \in 1 .. N - OBVIOUS - - <7> SUFFICES ASSUME NEW i \in (1..N), - NEW j \in (1..N), - (i < j), - A'[j] < A'[i] - PROVE <> \in U' /\ <> \in U' - (* /\ ( (b \leq i /\ j \leq p) \/ (p+1 \leq i /\ j \leq t)) *) - /\ \E b_1, t_1 \in 1..N : <> \in U' /\ b_1 <= i /\ j <= t_1 - BY DEF Inv_aux - <7>1 <> \in U' /\ <> \in U' - OBVIOUS - <7>2 CASE i \in b..t /\ j \in b..t - <8> USE <7>2, b \leq i, j \leq t - <8> HIDE <7>2 (* it seems strange that a USE statement becomes green, but a HIDE statement doesn't...?*) - <8>1 CASE j \leq p - <9> USE j \leq p - <9> b \leq i /\ j \leq p /\ <> \in U' - OBVIOUS - <9>q QED - OBVIOUS - <8>2 CASE p < i - <9> USE p < i - <9> p+1 \leq i /\ j \leq t /\ <> \in U' - BY SMT - <9>q QED - OBVIOUS - - <8>3 CASE i \leq p /\ p < j - <9>1 i \in b .. p - BY <8>3 - <9>2 j \in p+1..t - BY <8>3 - <9>3 A'[i] \leq A'[j] - BY <9>1, <9>2 DEF Partitions - <9>4 CASE A'[i] < A'[j] - BY <9>4 DEF Inv, TypeOK - <9>5 CASE A'[i] = A'[j] - BY <9>5 DEF Inv, TypeOK - <9>q QED - BY <9>3, <9>4, <9>5, SMT DEF Inv, TypeOK - <8>q QED - BY <8>1, <8>2, <8>3 DEF Inv_aux, Inv - - <7>3 CASE ~ i \in b..t /\ ~ j \in b..t - <8> USE <7>3, ~ i \in b..t, ~j \in b..t - <8> HIDE <7>3 - <8> A'[i] = A[i] /\ A'[j] = A[j] - BY DEF Partitions - <8>q QED - BY DEF Inv, Inv_aux - - <7>4 CASE i \in b..t /\ ~ j \in b..t - <8> USE <7>4, i \in b..t, ~j \in b..t - <8> HIDE <7>4 - <8> USE t < j - <8> A'[j] = A[j] - BY DEF Partitions - <8>1 \A x \in {A[k] : k \in b..t} : A[j] >= x - <9> SUFFICES ASSUME NEW x \in b..t - PROVE A[j] >= A[x] - OBVIOUS - <9> USE x < j - <9>0 A[j] < A[x] => (\E m, n \in 1 .. N : <> \in U /\ m \leq x /\ j \leq n) - BY DEF Inv, Inv_aux - <9>3 ~ (\E m, n \in 1 .. N : <> \in U /\ m \leq x /\ j \leq n) - <10> SUFFICES ASSUME NEW m \in 1..N, - NEW n \in 1..N, - <> \in U - PROVE ~ m <= x \/ ~ j <= n - OBVIOUS - <10>1 CASE <> = <> - BY <10>1 - - <10>2 CASE <> # <> - BY <10>2, ~ x \in m..n DEF NoOverlap - - <10>q QED - BY <10>1, <10>2 - <9>4 ~ A[j] < A[x] => A[j] >= A[x] - OBVIOUS - <9>q QED -(* In this situation "BY <9>0, <9>3" doesn't solve the problem, and it took me a whilte to figure out, - that I need to explicitly separate logic from math, by providing <9>4... *) - BY <9>0, <9>3, <9>4 - - <8>2 \A b_1, p_1, t_1 \in 1 .. N : - A' \in Partitions(A, p_1, b_1, t_1) => - {A'[k] : k \in b_1..t_1} = {A[k] : k \in b_1..t_1} - BY ONLY <6>1, A \in [1..N -> Int], p \in 1..N, PartitionsSetStable DEF TypeOK, Inv (* why does this not work?? *) - <8>3 {A'[k] : k \in b..t} = {A[k] : k \in b..t} - BY <8>2, <6>1 DEF TypeOK, Inv - <8>4 A'[i] \in {A[k]: k \in b..t} - BY <8>3 - <8>5 A'[j] >= A'[i] - BY <8>4, <8>1 - <8>q QED - BY <7>1, <8>5, <6>1 DEF TypeOK - <7>5 CASE ~ i \in b..t /\ j \in b..t - <8> USE <7>5, ~ i \in b..t, j \in b..t - <8> HIDE <7>5 - <8> USE i < b - <8> A'[i] = A[i] - BY DEF Partitions - <8>1 \A x \in {A[k] : k \in b..t} : A[i] <= x - <9> SUFFICES ASSUME NEW x \in b..t - PROVE A[i] <= A[x] - OBVIOUS - <9> USE x > i - <9>0 A[i] > A[x] => (\E m, n \in 1 .. N : <> \in U /\ m \leq i /\ x \leq n) - BY DEF Inv, Inv_aux - <9>3 ~ (\E m, n \in 1 .. N : <> \in U /\ m \leq i /\ x \leq n) - <10> SUFFICES ASSUME NEW m \in 1..N, - NEW n \in 1..N, - <> \in U - PROVE ~ m <= i \/ ~ x <= n - OBVIOUS - <10>1 CASE <> = <> - BY <10>1 - - <10>2 CASE <> # <> - BY <10>2, ~ x \in m..n DEF NoOverlap - - <10>q QED - BY <10>1, <10>2 - <9>4 ~ A[i] > A[x] => A[i] <= A[x] - OBVIOUS - <9>q QED -(* In this situation "BY <9>0, <9>3" doesn't solve the problem, and it took me a whilte to figure out, - that I need to explicitly separate logic from math, by providing <9>4... *) - BY <9>0, <9>3, <9>4 - - <8>2 \A b_1, p_1, t_1 \in 1 .. N : - A' \in Partitions(A, p_1, b_1, t_1) => - {A'[k] : k \in b_1..t_1} = {A[k] : k \in b_1..t_1} - BY ONLY <6>1, A \in [1..N -> Int], p \in 1..N, PartitionsSetStable DEF TypeOK, Inv (* why does this not work?? *) - <8>3 {A'[k] : k \in b..t} = {A[k] : k \in b..t} - BY <8>2, <6>1 DEF TypeOK, Inv - <8>4 A'[j] \in {A[k]: k \in b..t} - BY <8>3 - <8>5 A'[j] >= A'[i] - BY <8>4, <8>1 - <8>q QED - BY <7>1, <8>5, <6>1 DEF TypeOK - - <7>q QED - BY <7>2, <7>3, <7>4, <7>5 - <6>q QED - BY <6>1, <6>2, <6>3, <5>2 - <5>q QED - BY <5>1, <5>2 - <4>q QED - BY <4>1, <3>2, <2>2 DEF Next, Inv_aux - <3>q QED - BY <3>1, <3>2, <2>2 DEF Inv - <2>q QED - BY <2>1, <2>2 - -<1>3 Inv => Safety - <2>1 SUFFICES ASSUME Inv, U = {} - PROVE A \in PermsOf(A0) /\ IsSorted(A) - BY DEF Safety - <2>2 A \in PermsOf(A0) - BY <2>1 DEF Inv - <2>3 ASSUME NEW i \in 1..N, - NEW j \in 1..N, - i < j - PROVE A[i] \leq A [j] - <3>1 ~ (A[j] < A[i]) \/ \E b, t \in N : <> \in U /\ b <= i /\ j <= t - BY <2>1, <2>3 DEF Inv, Inv_aux - <3>2 ~ \E b, t \in N : <> \in U /\ b <= i /\ j <= t - BY <2>1 - <3>q QED BY <3>1, <3>2, <2>3, Z3 DEF Inv, TypeOK - <2>q QED - BY <2>1, <2>2, <2>3 DEF IsSorted - -<1>4 QED - BY LS4, <1>1, <1>2, <1>3 , NO DEF Spec - -============================================================================= - diff --git a/examples_draft/quicksort/Quicksort07d.tla b/examples_draft/quicksort/Quicksort07d.tla deleted file mode 100644 index 889e32400..000000000 --- a/examples_draft/quicksort/Quicksort07d.tla +++ /dev/null @@ -1,662 +0,0 @@ ------------------------------ MODULE Quicksort07d ---------------------------- -(***************************************************************************) -(* This module specifies a Quicksort algorithm for sorting a sequence A of *) -(* length N of integers. *) -(***************************************************************************) -EXTENDS Integers, TLAPS, FiniteSetTheorems, FunctionTheorems, Utils - -CONSTANT A0, N - -ASSUME ConstantAssump == /\ N \in Nat \ {0} - /\ A0 \in [1..N -> Int] - -IsSorted(B) == \A i, j \in 1..N : -(i < j) => (B[i] =< B[j]) - -PermsOf(Arr) == - LET Automorphisms(S) == { f \in [S -> S] : \A y \in S : \E x \in S : f[x] = y } - - f ** g == [x \in DOMAIN g |-> f[g[x]]] - - IN { Arr ** f : f \in Automorphisms(DOMAIN Arr) } - -Partitions(B, pivot, lo, hi) == - {C \in PermsOf(B) : - /\ \A i \in 1..(lo-1) \cup (hi+1)..N : C[i] = B[i] - /\ \A i \in lo..pivot, j \in (pivot+1)..hi : C[i] =< C[j] } - -VARIABLES A, U - -TypeOK == /\ A \in [1..N -> Int] - /\ U \in SUBSET ((1..N) \X (1..N)) - -vars == <> - -Init == /\ A = A0 - /\ U = { <<1, N>> } - -Next == /\ U # {} - /\ \E b \in 1..N, t \in 1..N : - /\ <> \in U - /\ IF b # t - THEN \E p \in b..(t-1) : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \cup {<>, <>} - ELSE /\ U' = U \ {<>} - /\ A' = A - -Spec == Init /\ [][Next]_vars /\ WF_vars(Next) ------------------------------------------------------------------------------ - -LEMMA EverythingIsFinite_1N == \A X : IsFiniteSet({X[k] : k \in 1..N}) - <1> SUFFICES ASSUME NEW X - PROVE (*IsFiniteSet({X[i] : i \in 1..N})*) - ExistsSurjection(1..N, {X[k] : k \in 1..N}) - BY ConstantAssump, N \in Nat, FS_NatSurjection - <1> DEFINE Thing == {X[k] : k \in 1..N} - <1> DEFINE W == Restrict(X, 1..N) - - <1>1 W \in Surjection(1..N, Thing) - BY DEF Restrict, Surjection - - - <1>q QED - BY <1>1 DEF ExistsSurjection - -LEMMA EverythingIsFinite == \A X : \A i, j \in 1..N : IsFiniteSet({X[k] : k \in i..j}) - <1> SUFFICES ASSUME NEW X, - NEW i \in 1..N, - NEW j \in 1..N - PROVE IsFiniteSet({X[k] : k \in i..j}) - OBVIOUS - <1> DEFINE S == {X[k] : k \in 1..N} - <1> DEFINE T == {X[k] : k \in i..j} - <1>1 T \in SUBSET S - <2> SUFFICES ASSUME NEW k \in i..j - PROVE k \in 1..N - OBVIOUS - <2>q QED - BY ConstantAssump, SMT - <1>2 IsFiniteSet(S) - BY EverythingIsFinite_1N - <1>q QED - BY <1>1, <1>2, FS_Subset - - - - -Safety == (U = {}) => (A \in PermsOf(A0)) /\ IsSorted(A) - -Inv_aux == \A i, j \in 1..N : (i < j /\ A[j] < A[i]) - => \E b, t \in 1..N : <> \in U /\ b <= i /\ j <= t - - -Inv == /\ TypeOK - /\ A \in PermsOf(A0) - /\ Inv_aux - - - -(* There is no overlap on the stack ever: *) -NoOverlap == \A a,b \in 1..N : <> \in U => \A i \in a..b : \A c,d \in 1..N : <> \in U \ {<>} => ~ i \in c..d -LEMMA NO == Spec => []NoOverlap -<1>1 Init => NoOverlap - BY DEF Init, NoOverlap - -<1>2 ASSUME NoOverlap, [Next]_vars - PROVE NoOverlap' - <2> NoOverlap - BY <1>2 - <2>1 CASE UNCHANGED vars - BY <2>1 DEF vars, NoOverlap - - <2>2 CASE Next - <3> USE Next - <3>0 PICK b,t \in 1..N : Next!2!(b,t) - BY DEF Next - - - <3>1 ASSUME b # t, - \E p \in b .. t - 1 : - /\ A' \in Partitions(A, p, b, t) - /\ U' = - (U \ {<>}) \union - {<>, <

>} - PROVE NoOverlap' - <4> USE b # t (* why can I do this here, even though <3>1 has a name?? *) - <4> SUFFICES ASSUME NEW a \in (1..N), NEW e \in (1..N), - <> \in U', - NEW i \in (a..e), - NEW c \in (1..N), NEW d \in (1..N), - <> \in U' \ {<>} - PROVE ~ i \in c..d - BY DEF NoOverlap - <4>1 PICK p \in b..t : Next!2!(b,t)!2!2!(p) - BY <3>0, <3>1 DEF Next - <4> U' = (U \ {<>}) \union {<> , <>} - BY <4>1 - <4> <> \in U - BY <3>0 - - <4>2 CASE <> \in U \ {<>} - <5> USE <> \in U \ {<>} - <5>1 \A k, l \in 1 .. N : - <> \in U \ {<>} => \neg i \in k .. l - BY ZenonT(30) DEF NoOverlap - <5>2 CASE <> \in U \ {<>} - BY <5>1, <5>2 - - <5>3 CASE <> = <> \/ <> = <> - <6> USE <5>3 - <6>1 <> \in U \ {<>} - OBVIOUS - <6> ~ i \in b..t - BY DEF NoOverlap - - <6>q QED - OBVIOUS - - <5>q QED - BY <5>2, <5>3 DEF NoOverlap - - <4>3 CASE <> = <> \/ <> = <> - <5> USE <4>3 - - <5>1 CASE <> \in U \ {<>} - <6> USE <5>1 - <6>2 i \in b..t - OBVIOUS - <6>q QED - BY ONLY <> \in U, NoOverlap, <6>2, <5>1, Zenon DEF NoOverlap - - <5>2 CASE <> = <> \/ <> = <> - <6> USE <5>2 - <6>q QED - OBVIOUS - - <5>q QED - BY <5>1, <5>2 - - - - <4>q QED - BY <4>1, <4>2, <4>3 DEF NoOverlap - - - <3>2 ASSUME b = t, - U' = U \ {<>} /\ A' = A - PROVE NoOverlap' - <4> SUFFICES ASSUME NEW a \in (1..N), NEW e \in (1..N), - <> \in U', - NEW i \in (a..e), - NEW c \in (1..N), NEW d \in (1..N), - <> \in U' \ {<>} - PROVE ~ i \in c..d - BY DEF NoOverlap - <4>q QED - BY <3>2 DEF NoOverlap - - - - - <3>q QED - BY <3>1, <3>2, <3>0 DEF Next - - <2>q QED - BY <2>1, <2>2, <1>2 - -<1>q QED - BY LS4, <1>1, <1>2 DEF Spec - - - ---------------------------------------------------- -\* Some lemmas about finite sets, cardinality, surjections, bijections -LEMMA FiniteSelfSurjectionIsBijection == - ASSUME NEW S, NEW f, - IsFiniteSet (S), - f \in Surjection (S, S) - PROVE f \in Bijection (S, S) - BY FS_SurjSameCardinalityImpliesInj DEF Bijection - -LEMMA FS_BijSameCardinality == - ASSUME NEW S, NEW T, - IsFiniteSet (S), IsFiniteSet(T), - ExistsBijection(S,T) - PROVE Cardinality(S) = Cardinality(T) - <1>1 PICK f : f \in Bijection(1..Cardinality(S), S) - BY FS_CardinalityType DEF ExistsBijection - <1>2 PICK g : g \in Bijection (S, T) - BY DEF ExistsBijection - <1> DEFINE h == [i \in 1..Cardinality(S) |-> g[f[i]]] - <1>3 h \in Bijection(1..Cardinality(S), T) - BY <1>1, <1>2, Fun_BijTransitive - <1> QED BY <1>3, FS_Bijection DEF ExistsBijection - -LEMMA CardinalitySumDisjoint == - ASSUME NEW S, NEW T, - IsFiniteSet(S), IsFiniteSet(T), - S \cap T = {} - PROVE Cardinality (S \cup T) = Cardinality (S) + Cardinality (T) - <1>1 Cardinality (S \cap T) = 0 BY FS_EmptySet - <1>2 Cardinality (S \cup T) = Cardinality (S) + Cardinality (T) - 0 - BY FS_Union, <1>1 - <1> QED BY <1>2, FS_CardinalityType - ---------------------------------------------------- - - -LEMMA PartitionsSetStable == \A B, C \in [1..N -> Int] : \A b, p, t \in 1..N : - C \in Partitions(B, p, b, t) => {C[k] : k \in b..t} = {B[k] : k \in b..t} - <1> SUFFICES ASSUME NEW B \in [1..N -> Int], - NEW C \in [1..N -> Int], - NEW b \in 1..N, - NEW p \in 1..N, - NEW t \in 1..N, - C \in Partitions(B, p, b, t) - PROVE {C[k] : k \in b..t} = {B[k] : k \in b..t} - OBVIOUS - <1> USE ConstantAssump - - <1> SUFFICES ASSUME NEW x - PROVE x \in {C[i] : i \in b..t} <=> x \in {B[i] : i \in b..t} - OBVIOUS - <1> DEFINE Cx == {i \in 1..N : C[i] = x} - Bx == {i \in 1..N : B[i] = x} - <1> Bx \subseteq 1..N /\ Cx \subseteq 1..N OBVIOUS - <1> IsFiniteSet (Bx) /\ IsFiniteSet (Cx) - BY FS_Interval, IsFiniteSet (1..N), FS_Subset - <1> /\ IsFiniteSet (Bx \ b..t) /\ IsFiniteSet (Bx \cap b..t) - /\ IsFiniteSet (Cx \ b..t) /\ IsFiniteSet (Cx \cap b..t) - BY FS_Difference, FS_Intersection - <1>1 Cardinality (Cx) = Cardinality (Bx) - <2>1 \E f : f \in Bijection(Cx, Bx) - <3>1 PICK f \in Surjection(1..N, 1..N) : C = [i \in 1..N |-> B[f[i]]] - BY DEF Partitions, Surjection, PermsOf - <3>2 f \in Bijection(1..N,1..N) - BY FiniteSelfSurjectionIsBijection, FS_Interval - <3>3 Range (Restrict (f, Cx)) = Bx - <4>1 Cx = {i \in 1..N : B[f[i]] = x} BY <3>1 - <4>2 \A i \in 1..N : f[i] \in 1..N - BY <3>2, Fun_BijectionProperties, f \in [1..N -> 1..N] - <4>3 \A i \in 1..N : i \in Cx <=> f[i] \in Bx - BY <4>1, <4>2 - <4> HIDE DEF Bx, Cx - <4>4 Cx = {i \in 1..N : f[i] \in Bx} BY <4>3 - <4>5 Range(Restrict(f, Cx)) = {f[i] : i \in Cx} - BY DEF Range, Restrict - <4>6 Range(Restrict(f, Cx)) \subseteq Bx - BY <4>4, <4>5 - <4>7 ASSUME NEW k \in Bx - PROVE k \in Range(Restrict(f, Cx)) - <5>1 SUFFICES \E i \in Cx : f[i] = k BY <4>5 - <5>2 B[k] = x BY <4>7 DEF Bx - <5>3 PICK i \in 1..N : f[i] = k BY DEF Surjection - <5>4 C[i] = x BY <3>1, <5>3, <5>2 - <5>5 i \in Cx BY <5>4 DEF Cx - <5> QED BY <5>3, <5>5 - <4> QED BY <4>6, <4>7 - <3>4 Restrict(f, Cx) \in Bijection(Cx, Bx) - BY <3>2, <3>3, Fun_BijRestrict - <3> QED BY <3>4 - <2> QED BY FS_Bijection, <2>1 DEF ExistsBijection - <1>2 Cardinality (Cx \ b..t) = Cardinality (Bx \ b..t) - <2>1 SUFFICES Cx \ b..t = Bx \ b..t OBVIOUS - <2>2 \A i \in Int : i \in 1..N \ b..t <=> i \in 1..(b-1) \cup (t+1)..N - OBVIOUS - <2>3 \A i \in 1..(b-1) \cup (t+1)..N : C[i] = B[i] BY DEF Partitions - <2>4 \A i \in 1..N \ b..t: C[i] = B[i] BY <2>2, <2>3 - <2> QED BY <2>4 - <1>3 Cardinality (Cx \cap b..t) = Cardinality (Bx \cap b..t) - <2>1 Cardinality (Cx) = Cardinality (Cx \ b..t) + Cardinality (Cx \cap b..t) - BY CardinalitySumDisjoint - <2>2 Cardinality (Bx) = Cardinality (Bx \ b..t) + Cardinality (Bx \cap b..t) - BY CardinalitySumDisjoint - <2> HIDE DEF Cx, Bx - <2> QED BY <2>1, <2>2, <1>1, <1>2, FS_CardinalityType - <1>4 x \in {C[i] : i \in b..t} <=> Cardinality (Cx \cap b..t) # 0 - <2>1 x \in {C[i] : i \in b..t} <=> \E i \in b..t : C[i] = x - OBVIOUS - <2>2 Cx \cap b..t = {i \in 1..N \cap b..t : C[i] = x} OBVIOUS - <2>3 1..N \cap b..t = b..t OBVIOUS - <2>4 Cx \cap b..t = {i \in b..t : C[i] = x} BY <2>2, <2>3 - <2> QED BY <2>1, <2>4, FS_EmptySet - <1>5 x \in {B[i] : i \in b..t} <=> Cardinality (Bx \cap b..t) # 0 - <2>1 x \in {B[i] : i \in b..t} <=> \E i \in b..t : B[i] = x - OBVIOUS - <2>2 Bx \cap b..t = {i \in 1..N \cap b..t : B[i] = x} OBVIOUS - <2>3 1..N \cap b..t = b..t OBVIOUS - <2>4 Bx \cap b..t = {i \in b..t : B[i] = x} BY <2>2, <2>3 - <2> QED BY <2>1, <2>4, FS_EmptySet - <1> QED BY <1>3, <1>4, <1>5 - - - -LEMMA PermsOf_trans == \A a, b, c \in [1..N -> Int] : (c \in PermsOf(b) /\ b \in PermsOf(a)) => c \in PermsOf(a) -<1> ASSUME NEW a \in [1..N -> Int], - NEW b \in [1..N -> Int], - NEW c \in [1..N -> Int], - c \in PermsOf(b), - b \in PermsOf(a) - PROVE c \in PermsOf(a) - <2>1 PICK f \in [1..N -> 1..N] : - (\A y \in 1..N : \E x \in 1..N : f[x] = y) - /\ (c = [x \in 1..N |-> b[f[x]]]) - BY Isa DEF PermsOf - <2>2 PICK g \in [1..N -> 1..N] : - (\A y \in 1..N : \E x \in 1..N : g[x] = y) - /\ (b = [x \in 1..N |-> a[g[x]]]) - BY Isa DEF PermsOf - <2> SUFFICES ASSUME TRUE - PROVE \E h \in [1..N -> 1..N] : - (\A y \in 1..N : \E x \in 1..N : h[x] = y) - /\ (c = [x \in 1..N |-> a[h[x]]]) - BY Isa DEF PermsOf - <2> DEFINE h == [k \in 1..N |-> g[f[k]]] - <2>3 WITNESS h \in [1..N -> 1..N] - - <2>4 ASSUME NEW y \in 1..N - PROVE \E x \in 1..N : h[x] = y - <3> PICK i \in 1..N : g[i] = y - BY <2>2 - <3> PICK j \in 1..N : f[j] = i - BY <2>1 - <3>q QED - OBVIOUS - - <2>5 c = [x \in 1..N |-> a[h[x]]] - BY <2>1, <2>2 - - <2>q QED - BY <2>3, <2>4, <2>5 -<1>q QED - OBVIOUS - - -LEMMA PermsOf_refl == \A a \in [1..N -> Int] : a \in PermsOf(a) - BY DEF PermsOf_refl, PermsOf - -THEOREM Spec => []Safety -<1>1 Init => Inv - PROOF - <2>2 SUFFICES (Init => A \in PermsOf(A0)) - /\ (Init => TypeOK) - /\ (Init => Inv_aux) - BY DEF Inv, TypeOK - <2>3 ASSUME Init, - NEW i \in 1.. N, - NEW j \in 1 .. N - PROVE \E b, t \in 1..N: <> \in U /\ b <= i /\ j <= t - - <3>1 <<1,N>> \in U /\ 1 <= i /\ j <= N - BY <2>3, CVC3 DEF Init - <3>q QED - BY <3>1, Z3, ConstantAssump - <2>4 Init => TypeOK - BY Z3, ConstantAssump DEF Init, TypeOK, ConstantAssump - <2>5 Init => A \in PermsOf(A0) - BY PermsOf_refl, Z3, ConstantAssump DEF Init, PermsOf_refl - <2>q QED - BY <2>2, <2>3, <2>4, <2>5 DEF Inv_aux - -<1>2 NoOverlap /\ [Next]_vars /\ Inv => Inv' - <2>1 SUFFICES ( NoOverlap /\ Inv /\ [Next]_vars) - => ( TypeOK' - /\ A' \in PermsOf(A0) - /\ Inv_aux' ) - BY DEF Inv - <2>2 ASSUME Inv, [Next]_vars, NoOverlap - PROVE TypeOK' /\ A' \in PermsOf(A0) /\ Inv_aux' - <3> Inv BY <2>2 - <3> USE ConstantAssump - <3> USE NoOverlap - <3>1 CASE UNCHANGED vars - <4>1 TypeOK' - BY <2>2, <3>1 DEF Inv, TypeOK, vars - <4>2 A' \in PermsOf(A0) - BY <2>2, <3>1 DEF Inv, vars - <4>3 Inv_aux' - BY <2>2, <3>1 DEF Inv, Inv_aux, vars - <4>q QED - BY <4>1, <4>2, <4>3, <3>1 - <3>2 CASE Next - <4> USE Next - <4>1 ASSUME U # {}, - NEW b \in 1..N, - NEW t \in 1..N, - <> \in U, - IF b # t - THEN \E p \in b..(t-1) : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \cup {<>, <>} - ELSE /\ U' = U \ {<>} - /\ A' = A - PROVE TypeOK' /\ A' \in PermsOf(A0) /\ Inv_aux' - <5> USE U # {} - <5> USE <> \in U - <5>1 CASE b = t - <6> USE b = t - <6> A' = A - BY <4>1 - <6> U' = U \ {<>} - BY <4>1 - <6>3 TypeOK' - BY DEF TypeOK, Inv - <6>4 A' \in PermsOf(A0) - BY PermsOf_trans DEF PermsOf_trans, ConstantAssump, Inv - <6>5 Inv_aux' - BY DEF Inv_aux, Inv (* ha, that's very nice, I was expecting this to be work... *) - <6>q QED - BY <6>3, <6>4, <6>5, <5>1 - <5>2 CASE b # t - <6> USE b # t - <6> SUFFICES ASSUME NEW p \in b..(t-1), - A' \in Partitions(A, p, b, t), - U' = (U \ {<>}) \cup {<>, <>} - PROVE TypeOK' /\ A' \in PermsOf(A0) /\ Inv_aux' - BY <4>1 - <6>1 TypeOK' - <7> U' \in SUBSET ( (1..N) \X (1..N) ) - <8> SUFFICES U \ {<>} \in SUBSET ((1..N) \X (1..N)) - /\ {<>, <>} \in SUBSET ((1..N) \X (1..N)) - - OBVIOUS - <8>1 U \ {<>} \in SUBSET ((1..N) \X (1..N)) - BY SMT DEF Inv, TypeOK - <8>2 {<>, <>} \in SUBSET ((1..N) \X (1..N)) - BY SMT - <8>q QED - BY <8>1, <8>2 - <7> A' \in [1..N -> Int] - BY SMT DEF Inv, TypeOK, Partitions, PermsOf - <7>q QED - BY DEF TypeOK - <6>2 A' \in PermsOf(A0) - <7> SUFFICES A' \in PermsOf(A) - BY PermsOf_trans, <6>1 DEF Inv, TypeOK - - <7>q QED - BY DEF Partitions - <6>3 Inv_aux' - <7> p \in 1 .. N - OBVIOUS - - <7> SUFFICES ASSUME NEW i \in (1..N), - NEW j \in (1..N), - (i < j), - A'[j] < A'[i] - PROVE <> \in U' /\ <> \in U' - (* /\ ( (b \leq i /\ j \leq p) \/ (p+1 \leq i /\ j \leq t)) *) - /\ \E b_1, t_1 \in 1..N : <> \in U' /\ b_1 <= i /\ j <= t_1 - BY DEF Inv_aux - <7>1 <> \in U' /\ <> \in U' - OBVIOUS - <7>2 CASE i \in b..t /\ j \in b..t - <8> USE <7>2, b \leq i, j \leq t - <8> HIDE <7>2 (* it seems strange that a USE statement becomes green, but a HIDE statement doesn't...?*) - <8>1 CASE j \leq p - <9> USE j \leq p - <9> b \leq i /\ j \leq p /\ <> \in U' - OBVIOUS - <9>q QED - OBVIOUS - <8>2 CASE p < i - <9> USE p < i - <9> p+1 \leq i /\ j \leq t /\ <> \in U' - BY SMT - <9>q QED - OBVIOUS - - <8>3 CASE i \leq p /\ p < j - <9>1 i \in b .. p - BY <8>3 - <9>2 j \in p+1..t - BY <8>3 - <9>3 A'[i] \leq A'[j] - BY <9>1, <9>2 DEF Partitions - <9>4 CASE A'[i] < A'[j] - BY <9>4 DEF Inv, TypeOK - <9>5 CASE A'[i] = A'[j] - BY <9>5 DEF Inv, TypeOK - <9>q QED - BY <9>3, <9>4, <9>5, SMT DEF Inv, TypeOK - <8>q QED - BY <8>1, <8>2, <8>3 DEF Inv_aux, Inv - - <7>3 CASE ~ i \in b..t /\ ~ j \in b..t - <8> USE <7>3, ~ i \in b..t, ~j \in b..t - <8> HIDE <7>3 - <8> A'[i] = A[i] /\ A'[j] = A[j] - BY DEF Partitions - <8>q QED - BY DEF Inv, Inv_aux - - <7>4 CASE i \in b..t /\ ~ j \in b..t - <8> USE <7>4, i \in b..t, ~j \in b..t - <8> HIDE <7>4 - <8> USE t < j - <8> A'[j] = A[j] - BY DEF Partitions - <8>1 \A x \in {A[k] : k \in b..t} : A[j] >= x - <9> SUFFICES ASSUME NEW x \in b..t - PROVE A[j] >= A[x] - OBVIOUS - <9> USE x < j - <9>0 A[j] < A[x] => (\E m, n \in 1 .. N : <> \in U /\ m \leq x /\ j \leq n) - BY DEF Inv, Inv_aux - <9>3 ~ (\E m, n \in 1 .. N : <> \in U /\ m \leq x /\ j \leq n) - <10> SUFFICES ASSUME NEW m \in 1..N, - NEW n \in 1..N, - <> \in U - PROVE ~ m <= x \/ ~ j <= n - OBVIOUS - <10>1 CASE <> = <> - BY <10>1 - - <10>2 CASE <> # <> - BY <10>2, ~ x \in m..n DEF NoOverlap - - <10>q QED - BY <10>1, <10>2 - <9>4 ~ A[j] < A[x] => A[j] >= A[x] - OBVIOUS - <9>q QED -(* In this situation "BY <9>0, <9>3" doesn't solve the problem, and it took me a whilte to figure out, - that I need to explicitly separate logic from math, by providing <9>4... *) - BY <9>0, <9>3, <9>4 - - <8>2 \A b_1, p_1, t_1 \in 1 .. N : - A' \in Partitions(A, p_1, b_1, t_1) => - {A'[k] : k \in b_1..t_1} = {A[k] : k \in b_1..t_1} - BY ONLY <6>1, A \in [1..N -> Int], p \in 1..N, PartitionsSetStable DEF TypeOK, Inv (* why does this not work?? *) - <8>3 {A'[k] : k \in b..t} = {A[k] : k \in b..t} - BY <8>2, <6>1 DEF TypeOK, Inv - <8>4 A'[i] \in {A[k]: k \in b..t} - BY <8>3 - <8>5 A'[j] >= A'[i] - BY <8>4, <8>1 - <8>q QED - BY <7>1, <8>5, <6>1 DEF TypeOK - <7>5 CASE ~ i \in b..t /\ j \in b..t - <8> USE <7>5, ~ i \in b..t, j \in b..t - <8> HIDE <7>5 - <8> USE i < b - <8> A'[i] = A[i] - BY DEF Partitions - <8>1 \A x \in {A[k] : k \in b..t} : A[i] <= x - <9> SUFFICES ASSUME NEW x \in b..t - PROVE A[i] <= A[x] - OBVIOUS - <9> USE x > i - <9>0 A[i] > A[x] => (\E m, n \in 1 .. N : <> \in U /\ m \leq i /\ x \leq n) - BY DEF Inv, Inv_aux - <9>3 ~ (\E m, n \in 1 .. N : <> \in U /\ m \leq i /\ x \leq n) - <10> SUFFICES ASSUME NEW m \in 1..N, - NEW n \in 1..N, - <> \in U - PROVE ~ m <= i \/ ~ x <= n - OBVIOUS - <10>1 CASE <> = <> - BY <10>1 - - <10>2 CASE <> # <> - BY <10>2, ~ x \in m..n DEF NoOverlap - - <10>q QED - BY <10>1, <10>2 - <9>4 ~ A[i] > A[x] => A[i] <= A[x] - OBVIOUS - <9>q QED -(* In this situation "BY <9>0, <9>3" doesn't solve the problem, and it took me a whilte to figure out, - that I need to explicitly separate logic from math, by providing <9>4... *) - BY <9>0, <9>3, <9>4 - - <8>2 \A b_1, p_1, t_1 \in 1 .. N : - A' \in Partitions(A, p_1, b_1, t_1) => - {A'[k] : k \in b_1..t_1} = {A[k] : k \in b_1..t_1} - BY ONLY <6>1, A \in [1..N -> Int], p \in 1..N, PartitionsSetStable DEF TypeOK, Inv (* why does this not work?? *) - <8>3 {A'[k] : k \in b..t} = {A[k] : k \in b..t} - BY <8>2, <6>1 DEF TypeOK, Inv - <8>4 A'[j] \in {A[k]: k \in b..t} - BY <8>3 - <8>5 A'[j] >= A'[i] - BY <8>4, <8>1 - <8>q QED - BY <7>1, <8>5, <6>1 DEF TypeOK - - <7>q QED - BY <7>2, <7>3, <7>4, <7>5 - <6>q QED - BY <6>1, <6>2, <6>3, <5>2 - <5>q QED - BY <5>1, <5>2 - <4>q QED - BY <4>1, <3>2, <2>2 DEF Next, Inv_aux - <3>q QED - BY <3>1, <3>2, <2>2 DEF Inv - <2>q QED - BY <2>1, <2>2 - -<1>3 Inv => Safety - <2>1 SUFFICES ASSUME Inv, U = {} - PROVE A \in PermsOf(A0) /\ IsSorted(A) - BY DEF Safety - <2>2 A \in PermsOf(A0) - BY <2>1 DEF Inv - <2>3 ASSUME NEW i \in 1..N, - NEW j \in 1..N, - i < j - PROVE A[i] \leq A [j] - <3>1 ~ (A[j] < A[i]) \/ \E b, t \in N : <> \in U /\ b <= i /\ j <= t - BY <2>1, <2>3 DEF Inv, Inv_aux - <3>2 ~ \E b, t \in N : <> \in U /\ b <= i /\ j <= t - BY <2>1 - <3>q QED BY <3>1, <3>2, <2>3, Z3 DEF Inv, TypeOK - <2>q QED - BY <2>1, <2>2, <2>3 DEF IsSorted - -<1>4 QED - BY LS4, <1>1, <1>2, <1>3 , NO DEF Spec - -============================================================================= - diff --git a/examples_draft/quicksort/Quicksort21.tla b/examples_draft/quicksort/Quicksort21.tla deleted file mode 100644 index 71ff8b8d2..000000000 --- a/examples_draft/quicksort/Quicksort21.tla +++ /dev/null @@ -1,380 +0,0 @@ ------------------------------ MODULE Quicksort21 ---------------------------- -(***************************************************************************) -(* This module specifies a Quicksort algorithm for sorting a sequence A of *) -(* length N of integers. *) -(* Derived by Stephan from Jael's Quicksort07. *) -(***************************************************************************) -EXTENDS Integers, TLAPS, FiniteSetTheorems, Utils, Bags - -CONSTANT A0, N - -ASSUME ConstantAssump == /\ N \in Nat \ {0} - /\ A0 \in [1..N -> Int] - -IsSorted(B) == \A i, j \in 1..N : -(i < j) => (B[i] =< B[j]) - -(* Modification: made Automorphisms and ** top-level operators because we want - to reason about them. -PermsOf(Arr) == - LET Automorphisms(S) == { f \in [S -> S] : \A y \in S : \E x \in S : f[x] = y } - - f ** g == [x \in DOMAIN g |-> f[g[x]]] - - IN { Arr ** f : f \in Automorphisms(DOMAIN Arr) } -*) - -(* The set of automorphisms of a finite set S. *) -Automorphisms(S) == { f \in [S -> S] : \A y \in S : \E x \in S : f[x] = y } - -(* Function composition. *) -f ** g == [x \in DOMAIN g |-> f[g[x]]] - -(* Set of permutations of array Arr (with finite domain). *) -PermsOf(Arr) == { Arr ** f : f \in Automorphisms(DOMAIN Arr) } - -(* Leslie's original definition: the problem is that the automorphism that generates - C from B is not restricted to the interval lo .. hi, so it might exchange some - elements within this interval with elements outside (as long as the exchanged - elements have the same values). This not only drastically complicates the proofs - but also obviously does not correspond to any sensible implementation. One could - even argue that it complicates parallelization of Quicksort, since it is not - obvious from the specification that partitioning two non-overlapping intervals in - the worklist does not interfere. -Partitions(B, pivot, lo, hi) == - {C \in PermsOf(B) : - /\ \A i \in 1..(lo-1) \cup (hi+1)..N : C[i] = B[i] - /\ \A i \in lo..pivot, j \in (pivot+1)..hi : C[i] =< C[j] } -*) - -(* Jael's definition. I'm following the same idea but introduce a bit more structure. -Partitions(B, pivot, lo, hi) == -{ C \in [1..N -> Int] : - /\ (\E D \in PermsOf([i \in lo..hi |-> B[i]]) : C = [i \in 1..N |-> IF i \in lo..hi - THEN D[i] - ELSE B[i] ] ) - /\ \A i \in lo..pivot, j \in (pivot+1)..hi : C[i] =< C[j] - } -*) - -(* Set of permutations such that all elements below pivot are smaller than all - elements above it. *) -OrderingPerms(Arr, pivot) == - { B \in PermsOf(Arr) : \A i,j \in DOMAIN Arr : i <= pivot /\ pivot < j => B[i] <= B[j] } - -(* Copy of array Arr with elements between lo and hi overridden with values from B. *) -Override(Arr, lo, hi, B) == - [x \in DOMAIN Arr |-> IF x \in lo .. hi THEN B[x] ELSE Arr[x]] - -Partitions(B, pivot, lo, hi) == - { Override(B, lo, hi, C) : C \in OrderingPerms(Restrict(B, lo .. hi), pivot) } - -VARIABLES A, U - -(* Type correctness predicate strengthened w.r.t. Jael's version *) -TypeOK == /\ A \in [1..N -> Int] - /\ A \in PermsOf(A0) - /\ U \in SUBSET { u \in (1..N) \X (1..N) : u[1] <= u[2] } - -vars == <> - -Init == /\ A = A0 - /\ U = { <<1, N>> } - -Next == /\ U # {} \* NB: This conjunct is implied by the following one - /\ \E b \in 1..N, t \in 1..N : - /\ <> \in U - /\ IF b # t - THEN \E p \in b..(t-1) : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \cup {<>, <>} - ELSE /\ U' = U \ {<>} - /\ A' = A - -Spec == Init /\ [][Next]_vars /\ WF_vars(Next) - ------------------------------------------------------------------------------ - -(* The main correctness (safety) property: - whenever U becomes empty, A contains a sorted permutation of A0 *) -Safety == (U = {}) => (A \in PermsOf(A0)) /\ IsSorted(A) - - -(* UnsortedIsCovered : if there are two positions i,j that point to values which are not sorted, - then the work list U contains a pair <> that covers both i and j. *) -UnsortedIsCovered == \A i, j \in 1..N : i < j /\ A[j] < A[i] - => \E u \in U : {i,j} \subseteq u[1] .. u[2] - -(* NoOverlap : no two pairs contained in the work list U overlap in range *) -NoOverlap == \A u,v \in U : (u[1] .. u[2]) \cap (v[1] .. v[2]) # {} => u = v -(* NoOverlap == \A a,b \in 1..N : <> \in U => \A i \in a..b : \A c,d \in 1..N : <> \in U \ {<>} => ~ i \in c..d *) - - -Inv == - /\ UnsortedIsCovered - /\ NoOverlap - ------------------------------------------------------------------------------ - -(***************************************************************************) -(* Lemmas about constant operators. *) -(***************************************************************************) - -LEMMA ImageOfIntervalIsFinite == - ASSUME NEW X, NEW a \in Int, NEW b \in Int - PROVE IsFiniteSet({X[k] : k \in a..b}) -<1>1. Restrict(X, a..b) \in Surjection(a..b, {X[k] : k \in a..b}) - BY DEF Restrict, Surjection -<1>. QED - BY <1>1, FS_Surjection, FS_Interval - -(* A permutation of an array is an array of the same type. *) -LEMMA PermsOf_type == - ASSUME NEW S, NEW T, NEW X \in [S -> T], NEW Y \in PermsOf(X) - PROVE Y \in [S -> T] -BY DEF PermsOf, Automorphisms, ** - -(* Any array is a permutation of itself. *) -LEMMA PermsOf_refl == - ASSUME NEW S, NEW T, NEW X \in [S -> T] - PROVE X \in PermsOf(X) -BY Isa DEF PermsOf, Automorphisms, ** - -(* The composition of two automorphisms is an automorphism. *) -LEMMA Automorphisms_trans == - ASSUME NEW S, NEW f \in Automorphisms(S), NEW g \in Automorphisms(S) - PROVE f ** g \in Automorphisms(S) -BY DEF Automorphisms, ** - -(* A permutation of a permutation of X is a permutation of X. *) -LEMMA PermsOf_trans == - ASSUME NEW S, NEW T, NEW X \in [S -> T], NEW Y \in PermsOf(X), NEW Z \in PermsOf(Y) - PROVE Z \in PermsOf(X) -<1>1. Y \in [S -> T] - BY PermsOf_type -<1>2. PICK f \in Automorphisms(S) : Y = X ** f - BY DEF PermsOf -<1>3. PICK g \in Automorphisms(S) : Z = Y ** g - BY <1>1 DEF PermsOf -<1>4. Z = X ** (f ** g) - BY <1>2, <1>3 DEF Automorphisms, ** -<1>. QED - BY Automorphisms_trans, <1>4 DEF PermsOf - -(* The set of values contained in a permutation is the set of the original array. *) -LEMMA PermsOf_range == - ASSUME NEW X, NEW Y \in PermsOf(X) - PROVE Range(Y) = Range(X) -BY DEF PermsOf, Automorphisms, **, Range - -(* A partition is a permutation. *) -LEMMA PartitionPermsOf == - ASSUME NEW S, NEW T, NEW B \in [S -> T], - NEW lo \in Int, NEW hi \in Int, NEW pivot \in Int, lo .. hi \subseteq S, - NEW C \in Partitions(B, pivot, lo, hi) - PROVE C \in PermsOf(B) -<1>1. PICK CC \in OrderingPerms(Restrict(B, lo .. hi), pivot) : - C = Override(B, lo, hi, CC) - BY DEF Partitions -<1>2. CC \in PermsOf(Restrict(B, lo .. hi)) - BY DEF OrderingPerms -<1>3. PICK g \in Automorphisms(lo .. hi) : CC = Restrict(B, lo..hi) ** g - BY <1>2 DEF PermsOf, Restrict -<1>. DEFINE h == [x \in S |-> IF x \in lo .. hi THEN g[x] ELSE x] -<1>4. h \in Automorphisms(S) - BY DEF Automorphisms -<1>5. C = B ** h - BY <1>1, <1>3 DEF Automorphisms, **, Override, Restrict -<1>. QED - BY <1>4, <1>5 DEF PermsOf - -(* For any partition, the set of values between lo and hi is the set of the - original values contained in the array within that interval. -*) -LEMMA PartitionsSetStable == - ASSUME NEW B, NEW pivot, NEW lo, NEW hi, lo .. hi \subseteq DOMAIN B, - NEW C \in Partitions(B, pivot, lo, hi) - PROVE Range(Restrict(C, lo .. hi)) = Range(Restrict(B, lo .. hi)) -<1>1. PICK CC \in OrderingPerms(Restrict(B, lo .. hi), pivot) : - C = Override(B, lo, hi, CC) - BY DEF Partitions -<1>2. DOMAIN CC = lo .. hi - BY DEF OrderingPerms, PermsOf, Automorphisms, **, Restrict -<1>3. Range(CC) = Range(Restrict(B, lo .. hi)) - BY PermsOf_range DEF OrderingPerms -<1>4. Range(Restrict(C, lo .. hi)) = Range(CC) - BY <1>1, <1>2 DEF Override, Range, Restrict -<1>. QED - BY <1>3, <1>4 - - ------------------------------------------------------------------------------ - -(***************************************************************************) -(* Proof of the invariant. *) -(***************************************************************************) - -USE ConstantAssump - -(***************************************************************************) -(* We first prove type correctness, although there is no logical reason *) -(* to prove it separately from the main invariant. *) -(***************************************************************************) - -LEMMA Typing == Spec => []TypeOK -<1>1. ASSUME Init - PROVE TypeOK - <2>1. A \in [1..N -> Int] BY <1>1 DEF Init - <2>2. A \in PermsOf(A0) BY <1>1, PermsOf_refl DEF Init - <2>3. U \in SUBSET {u \in (1 .. N) \X (1 .. N) : u[1] =< u[2]} - BY <1>1 DEF Init - <2>. QED BY <2>1, <2>2, <2>3 DEF TypeOK - -<1>2. ASSUME TypeOK, [Next]_vars - PROVE TypeOK' - <2>1. CASE Next - <3>1. PICK b \in 1..N, t \in 1..N : - /\ <> \in U - /\ IF b # t - THEN \E p \in b..(t-1) : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \cup {<>, <>} - ELSE /\ U' = U \ {<>} - /\ A' = A - BY <2>1 DEF Next - <3>2. CASE b # t - <4>1. PICK p \in b .. (t-1) : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \cup {<>, <>} - BY <3>1, <3>2 - <4>1a. /\ b \in Int - /\ t \in Int - /\ p \in Int - /\ b .. t \subseteq 1 .. N - OBVIOUS - <4>2. A' \in PermsOf(A) - BY PartitionPermsOf, TypeOK, <4>1, <4>1a, Zenon DEF TypeOK \* not proved by SMT - <4>3. A' \in [1..N -> Int] - BY <4>2, TypeOK, PermsOf_type, Zenon DEF TypeOK - <4>4. A' \in PermsOf(A0) - BY <4>2, TypeOK, PermsOf_trans, Zenon DEF TypeOK - <4>4a. /\ b <= p - /\ p+1 <= t - /\ p \in 1 .. N - /\ p+1 \in 1 .. N - OBVIOUS - <4>5. U' \in SUBSET {u \in (1 .. N) \X (1 .. N) : u[1] =< u[2]} - BY <4>1, <4>4a, TypeOK, Isa DEF TypeOK - <4>. QED BY <4>3, <4>4, <4>5 DEF TypeOK - <3>3. CASE b = t - BY <3>1, <3>3, TypeOK DEF TypeOK - <3>. QED BY <3>2, <3>3 - <2>2. CASE UNCHANGED vars BY <1>2, <2>2 DEF vars, TypeOK - <2>. QED BY <1>2, <2>1, <2>2 -<1>. QED BY <1>1, <1>2, PTL DEF Spec - -(***************************************************************************) -(* Now we prove the main invariant. *) -(***************************************************************************) -LEMMA Invariance == Spec => []Inv -<1>1. ASSUME Init - PROVE Inv - BY <1>1 DEF Init, Inv, UnsortedIsCovered, NoOverlap -<1>2. ASSUME Inv, TypeOK, TypeOK', [Next]_vars - PROVE Inv' - <2>. CASE Next - <3>1. PICK b \in 1..N, t \in 1..N : - /\ <> \in U - /\ IF b # t - THEN \E p \in b..(t-1) : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \cup {<>, <>} - ELSE /\ U' = U \ {<>} - /\ A' = A - BY DEF Next - <3>. CASE b # t - <4>. PICK p \in b..(t-1) : - /\ A' \in Partitions(A, p, b, t) - /\ U' = (U \ {<>}) \cup {<>, <>} - BY <3>1 - <4>2. UnsortedIsCovered' - <5>. SUFFICES ASSUME NEW i \in 1 .. N, NEW j \in 1 .. N, - i < j, A'[j] < A'[i] - PROVE \E u \in U' : {i,j} \subseteq u[1] .. u[2] - BY DEF UnsortedIsCovered - <5>1. b .. t \subseteq DOMAIN A - BY TypeOK DEF TypeOK - <5>2. Range(Restrict(A', b..t)) = Range(Restrict(A, b..t)) - BY <5>1, PartitionsSetStable - <5>. CASE i \notin b .. t - (* In this case j cannot be within the interval b..t either because - this would imply the existence of two overlapping intervals in U. - But then A'[i] = A[i] and A'[j] = A[j], and there exists some - entry in the worklist that covers them and that stays in the worklist. *) - <6>1. A'[i] = A[i] - BY TypeOK DEF TypeOK, Partitions, Override - <6>2. ASSUME j \in b .. t PROVE FALSE - <7>1. PICK jj \in b..t : A[jj] = A'[j] - BY ONLY <6>2, <5>2, Zenon DEF Range, Restrict - \* Zenon may timeout on slow machines without ONLY - <7>2. /\ jj \in 1..N - /\ i < jj - /\ A[jj] < A[i] - BY <6>1, <6>2, <7>1, TypeOK, TypeOK' DEF TypeOK - <7>3. PICK u \in U : {i,jj} \subseteq u[1] .. u[2] - BY <7>2, Inv DEF Inv, UnsortedIsCovered - <7>4. u = <> - BY <3>1, <7>3, Inv DEF Inv, NoOverlap - <7>. QED BY <7>3, <7>4 - <6>3. A'[j] = A[j] - BY TypeOK, <6>2 DEF TypeOK, Partitions, Override - <6>. QED BY <6>1, <6>3, Inv DEF Inv, UnsortedIsCovered - <5>. CASE j \notin b .. t - (* This case is symmetric to the preceding one. *) - <6>1. A'[j] = A[j] - BY TypeOK DEF TypeOK, Partitions, Override - <6>2. ASSUME i \in b .. t PROVE FALSE - <7>1. PICK ii \in b..t : A[ii] = A'[i] - BY ONLY <6>2, <5>2, Zenon DEF Range, Restrict - \* Zenon may timeout on slow machines without ONLY - <7>2. /\ ii \in 1..N - /\ ii < j - /\ A[j] < A[ii] - BY <6>1, <6>2, <7>1, TypeOK, TypeOK' DEF TypeOK - <7>3. PICK u \in U : {ii,j} \subseteq u[1] .. u[2] - BY <7>2, Inv DEF Inv, UnsortedIsCovered - <7>4. u = <> - BY <3>1, <7>3, Inv DEF Inv, NoOverlap - <7>. QED BY <7>3, <7>4 - <6>3. A'[i] = A[i] - BY TypeOK, <6>2 DEF TypeOK, Partitions, Override - <6>. QED BY <6>1, <6>3, Inv DEF Inv, UnsortedIsCovered - <5>. CASE i \in b .. t /\ j \in b .. t - (* In this case A'[i] and A'[j] have to be covered by one of the - two new entries of the worklist because A' is a partition. *) - <6>1. /\ A' \in [1..N -> Int] - /\ \A k,l \in b..t : k <= p /\ p < l => A'[k] <= A'[l] - BY TypeOK, TypeOK', Z3 DEF TypeOK, Partitions, Override, OrderingPerms, Restrict - <6>. QED BY <6>1, Z3 - <5>. QED OBVIOUS - <4>3. NoOverlap' - BY <3>1, Inv DEF Inv, NoOverlap - <4>. QED BY <4>2, <4>3 DEF Inv - <3>. CASE b = t - BY Inv, <3>1 DEF Inv, UnsortedIsCovered, NoOverlap - <3>. QED OBVIOUS - <2>. CASE UNCHANGED vars BY Inv DEF Inv, UnsortedIsCovered, NoOverlap, vars - <2>. QED BY <1>2 -<1>. QED BY <1>1, <1>2, Typing, PTL DEF Spec - -(***************************************************************************) -(* Finally, we prove the correctness (safety) property. *) -(***************************************************************************) -THEOREM Spec => []Safety -<1>1. ASSUME TypeOK, Inv PROVE Safety - BY <1>1, Z3 DEF TypeOK, Inv, UnsortedIsCovered, Safety, IsSorted -<1>. QED BY <1>1, Typing, Invariance, PTL - - -============================================================================= - diff --git a/examples_draft/quicksort/Utils.tla b/examples_draft/quicksort/Utils.tla deleted file mode 100644 index 6f293c58a..000000000 --- a/examples_draft/quicksort/Utils.tla +++ /dev/null @@ -1,237 +0,0 @@ ----------------------- MODULE Utils ------------------------------- -EXTENDS Integers, TLAPS, FiniteSetTheorems - -(*************************************************************************) -(* Auxiliary Definitions and Lemmas for Quicksort proofs *) -(*************************************************************************) - - -(*************************************************************************) -(* Max Definition and Lemmata *) - - -(* Max stolen from "Implementing and Combining Specifications" *) -Max(S) == CHOOSE n \in S : \A m \in S : m =< n - - -(* for any non-empty finite set of Ints, S, - Max(S) is in S, - and Max(S) is greater-equal than all elements of S *) -LEMMA finite_Max == - ASSUME NEW S \in SUBSET Int, S # {}, IsFiniteSet(S) - PROVE /\ Max(S) \in S - /\ \A m \in S : m <= Max(S) -<1>. DEFINE P(T) == T \in SUBSET Int /\ T # {} => Max(T) \in T /\ \A m \in T : m <= Max(T) -<1>1. P({}) OBVIOUS -<1>2. ASSUME NEW T, NEW x, IsFiniteSet(T), P(T), x \notin T - PROVE P(T \cup {x}) - <2>. SUFFICES ASSUME T \in SUBSET Int, x \in Int - PROVE /\ Max(T \cup {x}) \in T \cup {x} - /\ \A m \in T \cup {x} : m <= Max(T \cup {x}) - OBVIOUS - <2>1. CASE T = {} - <3>1. Max(T \cup {x}) = x BY <2>1 DEF Max - <3>. QED BY <2>1, <3>1 - <2>2. T # {} => x <= Max(T) \/ x > Max(T) - <3>1. T # {} => Max(T) \in Int BY <1>2 - <3>. QED BY <3>1 - <2>3. CASE T # {} /\ x <= Max(T) - <3>. DEFINE MT == Max(T) - <3>2. /\ MT \in T \cup {x} - /\ \A m \in T \cup {x} : m <= MT - BY <1>2, <2>3 - <3>. HIDE DEF MT - <3>3. Max(T \cup {x}) = MT - BY <3>2 DEF Max - <3>. QED BY <3>2, <3>3 - <2>4. CASE T # {} /\ x > Max(T) - <3>. DEFINE MT == Max(T) - <3>1. /\ MT \in Int - /\ \A m \in T : m <= MT - BY <1>2, <2>4 - <3>2. \A m \in T \cup {x} : m <= x - BY <3>1, <2>4 - <3>3. Max(T \cup {x}) = x - BY <3>2 DEF Max - <3>. QED BY <3>2, <3>3 - <2>. QED BY <2>1, <2>2, <2>3, <2>4 -<1>. HIDE DEF P -<1>3. P(S) BY <1>1, <1>2, FS_Induction, IsaM("blast") -<1>. QED BY <1>3 DEF P - -LEMMA leq_Max == - ASSUME NEW m \in Int, NEW S \in SUBSET Int, IsFiniteSet(S), - NEW x \in S, m <= x - PROVE m <= Max(S) -<1>1. /\ Max(S) \in Int - /\ x <= Max(S) - BY finite_Max -<1>. QED BY <1>1 - - -(* for any finite subset of Ints, S, Max(S) is an Int *) -LEMMA MaxTypeOK == \A S : S \in SUBSET Int /\ IsFiniteSet(S) => Max(S) \in Int - <1> SUFFICES ASSUME NEW S, - S \in SUBSET Int, - IsFiniteSet(S) - PROVE (* Max(S) \in Int *) - \A n \in S : n \in Int - BY DEF Max - <1>1 ASSUME NEW n \in S - PROVE n \in Int - OBVIOUS - <1> QED - BY <1>1 - -(* For any finite subset of Ints, S, and any non-empty subset of S, T, Max(T) is less-than-or-equal Max(S) *) -LEMMA subset_Max == \A S : S \in SUBSET Int /\ IsFiniteSet(S) => \A T : T \in SUBSET S /\ T # {} => Max(T) <= Max(S) - <1> SUFFICES ASSUME NEW S, - S \in SUBSET Int, - IsFiniteSet(S), - NEW T, - T \in SUBSET S, - T # {} - PROVE Max(T) <= Max(S) - OBVIOUS - - <1>1 Max(T) \in T - BY T \in SUBSET Int, FS_Subset, IsFiniteSet(T), finite_Max - - <1>2 \A x \in T : \E y \in S : x <= y - <2> SUFFICES ASSUME NEW x \in T - PROVE \E y \in S : x <= y - OBVIOUS - <2>1 Max(S) \in S - BY finite_Max - <2>2 x \in S - OBVIOUS - <2> QED - BY <2>1, <2>2 - - <1>3 \A x \in S : x <= Max(S) - BY finite_Max - - <1> QED - BY <1>1, <1>2, <1>3 - - - - - -(*************************************************************************) -(* Min Definition and Lemmata *) - -Min(S) == CHOOSE n \in S : \A m \in S : n =< m - -LEMMA finite_Min == - ASSUME NEW S \in SUBSET Int, S # {}, IsFiniteSet(S) - PROVE /\ Min(S) \in S - /\ \A m \in S : m >= Min(S) -<1>. DEFINE P(T) == T \in SUBSET Int /\ T # {} => Min(T) \in T /\ \A m \in T : m >= Min(T) -<1>1. P({}) OBVIOUS -<1>2. ASSUME NEW T, NEW x, IsFiniteSet(T), P(T), x \notin T - PROVE P(T \cup {x}) - <2>. SUFFICES ASSUME T \in SUBSET Int, x \in Int - PROVE /\ Min(T \cup {x}) \in T \cup {x} - /\ \A m \in T \cup {x} : m >= Min(T \cup {x}) - OBVIOUS - <2>1. CASE T = {} - <3>1. Min(T \cup {x}) = x - BY <2>1 DEF Min - <3>. QED - BY <2>1, <3>1 - <2>2. T # {} => x >= Min(T) \/ x < Min(T) - <3>1. T # {} => Min(T) \in Int BY <1>2 - <3>. QED BY <3>1 - <2>3. CASE T # {} /\ x >= Min(T) - <3>. DEFINE MT == Min(T) - <3>2. /\ MT \in T \cup {x} - /\ \A m \in T \cup {x} : m >= MT - BY <1>2, <2>3 - <3>. HIDE DEF MT - <3>3. Min(T \cup {x}) = MT - BY <3>2 DEF Min - <3>. QED - BY <3>2, <3>3 - <2>4. CASE T # {} /\ x < Min(T) - <3>. DEFINE MT == Min(T) - <3>1. /\ MT \in Int - /\ \A m \in T : m >= MT - BY <1>2, <2>4 - <3>2. \A m \in T \cup {x} : m >= x - BY <3>1, <2>4 - <3>3. Min(T \cup {x}) = x - BY <3>2 DEF Min - <3>. QED BY <3>2, <3>3 - <2>. QED BY <2>1, <2>2, <2>3, <2>4 -<1>. HIDE DEF P -<1>3. P(S) BY <1>1, <1>2, FS_Induction, IsaM("blast") -<1>. QED BY <1>3 DEF P - -LEMMA leq_Min == - ASSUME NEW m \in Int, - NEW S \in SUBSET Int, - IsFiniteSet(S), - NEW x \in S, - m >= x - PROVE m >= Min(S) - <1>1 /\ Min(S) \in Int - /\ x >= Min(S) - BY finite_Min -<1>. QED BY <1>1 - - - -LEMMA MinTypeOK == \A S : S \in SUBSET Int /\ IsFiniteSet(S) => Min(S) \in Int - <1> SUFFICES ASSUME NEW S, - S \in SUBSET Int, - IsFiniteSet(S) - PROVE (* Min(S) \in Int *) - \A n \in S : n \in Int - BY DEF Min - <1>1 ASSUME NEW n \in S - PROVE n \in Int - OBVIOUS - <1> QED - BY <1>1 - - -LEMMA subset_Min == \A S : S \in SUBSET Int /\ IsFiniteSet(S) => \A T : T \in SUBSET S /\ T # {} => Min(S) <= Min(T) - <1> SUFFICES ASSUME NEW S, - S \in SUBSET Int, - IsFiniteSet(S), - NEW T, - T \in SUBSET S, - T # {} - PROVE Min(S) <= Min(T) - OBVIOUS - - <1>1 Min(T) \in T - BY T \in SUBSET Int, FS_Subset, IsFiniteSet(T), finite_Min - - <1>2 \A x \in T : \E y \in S : x >= y - <2> SUFFICES ASSUME NEW x \in T - PROVE \E y \in S : x >= y - OBVIOUS - <2>1 Min(S) \in S - BY finite_Min - <2>2 x \in S - OBVIOUS - <2> QED - BY <2>1, <2>2 - - <1>3 \A x \in S : x >= Min(S) - BY finite_Min - - <1> QED - BY <1>1, <1>2, <1>3 - - - - - -============================================================================= -\* Modification History -\* Last modified Wed Jan 22 11:15:57 CET 2014 by jael -\* Created Wed Jan 22 09:08:48 CET 2014 by jael - diff --git a/library/FiniteSetTheorems.tla b/library/FiniteSetTheorems.tla index 28988d1d0..a0ae7fce2 100644 --- a/library/FiniteSetTheorems.tla +++ b/library/FiniteSetTheorems.tla @@ -224,7 +224,7 @@ THEOREM FS_BoundedSetOfNaturals == THEOREM FS_Induction == ASSUME NEW S, IsFiniteSet(S), NEW P(_), P({}), - ASSUME NEW T, NEW x, IsFiniteSet(T), P(T), x \notin T + ASSUME NEW T \in SUBSET S, IsFiniteSet(T), P(T), NEW x \in S \ T PROVE P(T \cup {x}) PROVE P(S) diff --git a/library/FiniteSetTheorems_proofs.tla b/library/FiniteSetTheorems_proofs.tla index feb60d545..a62b0946e 100644 --- a/library/FiniteSetTheorems_proofs.tla +++ b/library/FiniteSetTheorems_proofs.tla @@ -387,7 +387,7 @@ THEOREM FS_Singleton == <2>1. /\ IsFiniteSet({} \cup {x}) /\ Cardinality({} \cup {x}) = 0 + 1 BY FS_EmptySet, FS_AddElement, Zenon - <2>. QED BY <2>1, Isa + <2>. QED BY <2>1, {x} = {} \cup {x} <1>2. ASSUME NEW S, IsFiniteSet(S), Cardinality(S) = 1 PROVE \E x : S = {x} BY <1>2, FS_CardinalityType, Fun_NatBijSingleton, Zenon @@ -568,22 +568,22 @@ THEOREM FS_BoundedSetOfNaturals == THEOREM FS_Induction == ASSUME NEW S, IsFiniteSet(S), NEW P(_), P({}), - ASSUME NEW T, NEW x, IsFiniteSet(T), P(T), x \notin T + ASSUME NEW T \in SUBSET S, IsFiniteSet(T), P(T), NEW x \in S \ T PROVE P(T \cup {x}) PROVE P(S) -<1>. DEFINE Q(n) == \A T : IsFiniteSet(T) /\ Cardinality(T) = n => P(T) +<1>. DEFINE Q(n) == \A T \in SUBSET S : Cardinality(T) = n => P(T) <1>1. SUFFICES \A n \in Nat : Q(n) BY FS_CardinalityType -<1>2. Q(0) BY FS_EmptySet, Zenon +<1>2. Q(0) BY FS_EmptySet, FS_Subset <1>3. ASSUME NEW n \in Nat, Q(n), - NEW T, IsFiniteSet(T), Cardinality(T) = n+1 + NEW T \in SUBSET S, Cardinality(T) = n+1 PROVE P(T) - <2>1. PICK x \in T : TRUE BY <1>3, FS_EmptySet - <2>2. /\ IsFiniteSet(T \ {x}) + <2>1. PICK x \in T : TRUE BY <1>3, FS_EmptySet, FS_Subset + <2>2. /\ T \ {x} \in SUBSET S + /\ IsFiniteSet(T \ {x}) /\ Cardinality(T \ {x}) = n - BY <1>3, FS_RemoveElement, Isa + BY <1>3, FS_RemoveElement, FS_Subset <2>3. P(T \ {x}) BY <2>2, Q(n) - <2>4. P((T \ {x}) \cup {x}) BY <2>2, <2>3, Zenon - <2>. QED BY <2>4, Zenon + <2>. QED BY <2>2, <2>3, Zenon <1>4. QED BY <1>2, <1>3, NatInduction, Isa @@ -674,7 +674,7 @@ THEOREM FS_Union == /\ Cardinality(S \cup A) = Cardinality(S) + Cardinality(A) - Cardinality(S \cap A) <1>1. P({}) BY FS_EmptySet, FS_CardinalityType -<1>2. ASSUME NEW A, NEW x, IsFiniteSet(A), P(A), x \notin A +<1>2. ASSUME NEW A \in SUBSET T, IsFiniteSet(A), P(A), NEW x \in T \ A PROVE P(A \cup {x}) <2>1. IsFiniteSet(S \cup (A \cup {x})) BY P(A), FS_AddElement, Isa <2>. /\ IsFiniteSet(S \cup A) @@ -796,7 +796,7 @@ THEOREM FS_UNION == <1>. DEFINE P(U) == (\A T \in U : IsFiniteSet(T)) => IsFiniteSet(UNION U) <1>1. P({}) BY FS_EmptySet, Zenon -<1>2. ASSUME NEW U, NEW x, P(U), x \notin U +<1>2. ASSUME NEW U \in SUBSET S, P(U), NEW x \in S \ U PROVE P(U \cup {x}) BY <1>2, FS_Union, Isa <1>. HIDE DEF P @@ -828,31 +828,31 @@ THEOREM FS_Product == /\ Cardinality(S) \in Nat BY FS_EmptySet, FS_CardinalityType, Zenon <2>. QED BY <2>1 -<1>2. ASSUME NEW A, NEW x, IsFiniteSet(A), P(A), x \notin A +<1>2. ASSUME NEW A \in SUBSET T, IsFiniteSet(A), P(A), NEW x \in T \ A PROVE P(A \cup {x}) <2>. /\ Cardinality(A) \in Nat /\ Cardinality(S) \in Nat - BY <1>2, FS_CardinalityType + BY <1>2, FS_CardinalityType, FS_Subset <2>. DEFINE SX == { <> : s \in S } <2>1. /\ IsFiniteSet(A \cup {x}) /\ Cardinality(A \cup {x}) = Cardinality(A) + 1 BY <1>2, FS_AddElement, Zenon <2>2. S \X (A \cup {x}) = (S \X A) \cup SX - BY <1>2, Isa + BY <1>2 <2>3. ExistsBijection(S, SX) <3>. DEFINE f == [s \in S |-> <>] <3>. f \in Bijection(S, SX) - BY Zenon DEF Bijection, Injection, IsInjective, Surjection + BY DEF Bijection, Injection, IsInjective, Surjection <3>. QED BY DEF ExistsBijection <2>4. /\ IsFiniteSet(SX) /\ Cardinality(SX) = Cardinality(S) BY <2>3, FS_Bijection <2>5. /\ IsFiniteSet(S \X (A \cup {x})) - /\ Cardinality(S \X (A \cup {x})) = + /\ Cardinality(S \X (A \cup {x})) = Cardinality(S \X A) + Cardinality(SX) - Cardinality((S \X A) \cap SX) - BY <2>2, <2>4, P(A), FS_Union, Isa + BY <2>2, <2>4, P(A), FS_Union <2>6. (S \X A) \cap SX = {} BY <1>2 - <2>7. Cardinality((S \X A) \cap SX) = 0 BY <2>6, FS_EmptySet, Zenon + <2>7. Cardinality((S \X A) \cap SX) = 0 BY <2>6, FS_EmptySet <2>. QED BY <2>1, <2>5, <2>4, <2>7, P(A) <1>. HIDE DEF P <1>. P(T) BY <1>1, <1>2, FS_Induction, IsaM("blast") @@ -860,7 +860,6 @@ THEOREM FS_Product == - (***************************************************************************) (* `. .' *) (* *) @@ -880,7 +879,7 @@ THEOREM FS_SUBSET == /\ Cardinality({{}}) = 1 BY FS_Singleton, Zenon <2>. QED BY FS_EmptySet, TwoExpLemma, Zenon -<1>2. ASSUME NEW A, NEW x, IsFiniteSet(A), x \notin A, P(A) +<1>2. ASSUME NEW A \in SUBSET S, IsFiniteSet(A), P(A), NEW x \in S \ A PROVE P(A \cup {x}) <2>. DEFINE Ax == {B \cup {x} : B \in SUBSET A} <2>1. Cardinality(A \cup {x}) = Cardinality(A) + 1 BY <1>2, FS_AddElement, Zenon @@ -906,9 +905,9 @@ THEOREM FS_SUBSET == <2>6. /\ IsFiniteSet(SUBSET (A \cup {x})) /\ Cardinality(SUBSET (A \cup {x})) = Cardinality(SUBSET A) + Cardinality(Ax) - Cardinality((SUBSET A) \cap Ax) - BY <2>3, <2>5, P(A), FS_Union, Isa + BY <2>3, <2>5, P(A), FS_Union <2>7. (SUBSET A) \cap Ax = {} BY <1>2 - <2>8. Cardinality((SUBSET A) \cap Ax) = 0 BY <2>7, FS_EmptySet, Zenon + <2>8. Cardinality((SUBSET A) \cap Ax) = 0 BY <2>7, FS_EmptySet <2>. QED BY <2>2, <2>5, <2>6, <2>8, P(A), FS_CardinalityType <1>. HIDE DEF P <1>. P(S) BY <1>1, <1>2, FS_Induction, IsaM("blast") @@ -916,9 +915,4 @@ THEOREM FS_SUBSET == ============================================================================= -\* Modification History -\* Last modified Fri Jun 13 19:01:57 CEST 2025 by merz -\* Last modified Thu Jul 04 15:15:07 CEST 2013 by bhargav -\* Last modified Tue Jun 04 11:44:51 CEST 2013 by bhargav -\* Last modified Fri May 03 12:02:51 PDT 2013 by tomr \* Created Fri Oct 05 15:04:18 PDT 2012 by tomr