---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/BinarySearch.tla
---
----------------------------- MODULE BinarySearch ------------------------------
(***************************************************************************)
(* This module defines a binary search algorithm for finding an item in a *)
(* sorted sequence, and contains a TLAPS-checked proof of its safety *)
(* property. We assume a sorted sequence seq with elements in some set *)
(* Values of integers and a number val in Values, it sets the value *)
(* `result' to either a number i with seq[i] = val, or to 0 if there is no *)
(* such i. *)
(* *)
(* It is surprisingly difficult to get such a binary search algorithm *)
(* correct without making errors that have to be caught by debugging. I *)
(* suggest trying to write a correct PlusCal binary search algorithm *)
(* yourself before looking at this one. *)
(* *)
(* This algorithm is one of the examples in Section 7.3 of "Proving Safety *)
(* Properties", which is at *)
(* *)
(* http://lamport.azurewebsites.net/tla/proving-safety.pdf *)
(***************************************************************************)
EXTENDS Integers, Sequences, TLAPS
CONSTANT Values
ASSUME ValAssump == Values \subseteq Int
SortedSeqs == {ss \in Seq(Values):
\A i, j \in 1..Len(ss): (i < j) => (ss[i] <= ss[j])}
LEMMA SortedLess ==
ASSUME NEW s \in SortedSeqs, NEW i \in 1 .. Len(s), NEW j \in 1 .. Len(s),
s[i] < s[j]
PROVE i < j
<1>. SUFFICES ASSUME j <= i PROVE FALSE
OBVIOUS
<1>. QED BY ValAssump DEF SortedSeqs
(***************************************************************************
--fair algorithm BinarySearch {
variables seq \in SortedSeqs, val \in Values,
low = 1, high = Len(seq), result = 0 ;
{ a: while (low =< high /\ result = 0) {
with (mid = (low + high) \div 2, mval = seq[mid]) {
if (mval = val) { result := mid}
else if (val < mval) { high := mid - 1}
else {low := mid + 1} } } } }
***************************************************************************)
\* BEGIN TRANSLATION
VARIABLES seq, val, low, high, result, pc
vars == << seq, val, low, high, result, pc >>
Init == (* Global variables *)
/\ seq \in SortedSeqs
/\ val \in Values
/\ low = 1
/\ high = Len(seq)
/\ result = 0
/\ pc = "a"
a ==
/\ pc = "a"
/\ IF low <= high /\ result = 0
THEN
/\ LET mid == (low + high) \div 2 IN
LET mval == seq[mid] IN
IF mval = val
THEN
/\ result' = mid
/\ UNCHANGED << low, high >>
ELSE
/\ IF val < mval
THEN
/\ high' = mid - 1
/\ low' = low
ELSE
/\ low' = mid + 1
/\ high' = high
/\ UNCHANGED result
/\ pc' = "a"
ELSE
/\ pc' = "Done"
/\ UNCHANGED << low, high, result >>
/\ UNCHANGED << seq, val >>
(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == pc = "Done" /\ UNCHANGED vars
Next == a
\/ Terminating
Spec ==
/\ Init /\ [][Next]_vars
/\ WF_vars(Next)
Termination == <>(pc = "Done")
\* END TRANSLATION
--------------------------------------------------------------------------------
(***************************************************************************)
(* Partial correctness of the algorithm is expressed by invariance of *)
(* formula resultCorrect. To get TLC to check this property, we use a *)
(* model that overrides the definition of Seq so Seq(S) is the set of *)
(* sequences of elements of S having at most some small length. For *)
(* example, *)
(* *)
(* Seq(S) == UNION {[1..i -> S] : i \in 0..3} *)
(* *)
(* is the set of such sequences with length at most 3. *)
(***************************************************************************)
resultCorrect ==
(pc = "Done") => IF \E i \in 1..Len(seq): seq[i] = val
THEN seq[result] = val
ELSE result = 0
(***************************************************************************)
(* Proving the invariance of resultCorrect requires finding an inductive *)
(* invariant that implies it. A suitable inductive invariant Inv is *)
(* defined here. You can use TLC to check that Inv is an inductive *)
(* invariant. *)
(***************************************************************************)
TypeOK ==
/\ seq \in SortedSeqs
/\ val \in Values
/\ low \in 1..(Len(seq) + 1)
/\ high \in 0..Len(seq)
/\ result \in 0..Len(seq)
/\ pc \in {"a", "Done"}
Inv ==
/\ TypeOK
/\ (result /= 0) => (Len(seq) > 0) /\ (seq[result] = val)
/\ (pc = "a") =>
IF \E i \in 1..Len(seq): seq[i] = val
THEN \E i \in low..high: seq[i] = val
ELSE result = 0
/\ (pc = "Done") => (result /= 0) \/ (\A i \in 1..Len(seq): seq[i] /= val)
(***************************************************************************)
(* Here is the invariance proof. *)
(***************************************************************************)
THEOREM Spec => []resultCorrect
<1>1. Init => Inv
BY DEF Init, Inv, TypeOK, SortedSeqs
<1>2. Inv /\ [Next]_vars => Inv'
<2> SUFFICES ASSUME Inv,
[Next]_vars
PROVE Inv'
OBVIOUS
<2>1. CASE a
<3>. UNCHANGED <<seq, val>>
BY <2>1 DEF a
<3>1. CASE low =< high /\ result = 0
<4> DEFINE mid == (low + high) \div 2
mval == seq[mid]
<4> (low =< mid) /\ (mid =< high) /\ (mid \in 1..Len(seq))
BY <3>1, Z3 DEF Inv, TypeOK, SortedSeqs
<4>1. TypeOK'
<5>1. seq' \in SortedSeqs
BY <2>1 DEF a, Inv, TypeOK
<5>2. val' \in Values
BY <2>1 DEF a, Inv, TypeOK
<5>3. (low \in 1..(Len(seq)+1))'
<6>1. CASE seq[mid] = val
BY <6>1, <2>1, <3>1, Z3 DEF Inv, TypeOK, a
<6>2. CASE seq[mid] /= val
BY <6>2, <2>1, <3>1, Z3 DEF Inv, TypeOK, a, SortedSeqs
<6>3. QED
BY <6>1, <6>2
<5>4. (high \in 0..Len(seq))'
<6>1. CASE seq[mid] = val
BY <6>1, <2>1, <3>1, Z3 DEF Inv, TypeOK, a
<6>2. CASE seq[mid] /= val
BY <6>2, <2>1, <3>1, Z3 DEF Inv, TypeOK, a, SortedSeqs
<6>3. QED
BY <6>1, <6>2
<5>5. (result \in 0..Len(seq))'
<6>1. CASE seq[mid] = val
BY <6>1, <2>1, <3>1, Z3 DEF Inv, TypeOK, a
<6>2. CASE seq[mid] /= val
BY <6>2, <2>1, <3>1, Z3 DEF Inv, TypeOK, a
<6>3. QED
BY <6>1, <6>2
<5>6. (pc \in {"a", "Done"})'
BY <2>1, <3>1 DEF Inv, TypeOK, a
<5>7. QED
BY <5>1, <5>2, <5>3, <5>4, <5>5, <5>6 DEF TypeOK
<4>2. ((result /= 0) => (Len(seq) > 0) /\ (seq[result] = val))'
<5>1. CASE seq[mid] = val
BY <5>1, <2>1, <3>1 DEF Inv, TypeOK, a
<5>2. CASE seq[mid] /= val
BY <5>2, <2>1, <3>1 DEF Inv, TypeOK, a
<5>3. QED
BY <5>1, <5>2
<4>3. ((pc = "a") =>
IF \E i \in 1..Len(seq) : seq[i] = val
THEN \E i \in low..high : seq[i] = val
ELSE result = 0)'
<5>1. CASE seq[mid] = val
BY <5>1, <2>1, <3>1 DEF Inv, TypeOK, a
<5>2. CASE seq[mid] /= val
<6>1. /\ Len(seq) > 0 \* /\ Len(seq) \in Nat
/\ low \in 1..Len(seq)
/\ high \in 1..Len(seq)
BY ValAssump DEF Inv, TypeOK, SortedSeqs
<6>2. CASE \E i \in 1..Len(seq) : seq[i] = val
<7>1. PICK i \in low..high : seq[i] = val
BY <6>2, <2>1 DEF a, Inv
<7>2. /\ Len(seq) > 0 /\ Len(seq) \in Nat
/\ low \in 1..Len(seq)
/\ high \in 1..Len(seq)
/\ seq[i] = val
BY ValAssump, <6>2, <7>1 DEF Inv, TypeOK, SortedSeqs
<7>3. \A j \in 1..Len(seq) : seq[j] \in Int
BY ValAssump DEF Inv, TypeOK, SortedSeqs
<7>4. CASE val < seq[mid]
<8>1. seq[i] < seq[mid]
BY <7>2, <7>4
<8>2. i < mid
BY <7>2, <8>1, SortedLess DEF Inv, TypeOK
<8>3. i \in low .. mid-1
BY ONLY <7>2, <8>1, <8>2, Z3
<8>4. /\ (pc' = "a") /\ (low' = low) /\ (high' = mid-1)
/\ \E j \in 1..Len(seq) : seq[j] = val
BY <2>1, <3>1, <5>2, <6>2, <7>4 DEF a, mid
<8>. QED
BY <7>2, <8>4, <8>3
<7>5. CASE ~(val < seq[mid])
<8> HIDE DEF mid
<8>1. seq[mid] < seq[i]
BY ValAssump, <7>2, <7>5, <5>2, <7>3, Z3
<8>2. mid < i
BY <7>2, <8>1, SortedLess DEF Inv, TypeOK
<8>3. i \in mid+1 .. high
BY <7>2, <8>1, <8>2, Z3
<8>4. /\ (pc' = "a") /\ (low' = mid+1) /\ (high' = high)
/\ \E j \in 1..Len(seq) : seq[j] = val
BY <2>1, <3>1, <5>2, <6>2, <7>5 DEF a, mid
<8>5. QED
BY <7>2, <8>4, <8>3 \* , <8>5
<7>7. QED
BY <7>4, <7>5
<6>3. CASE ~ \E i \in 1..Len(seq) : seq[i] = val
BY <6>3, <5>2, <2>1, <3>1 DEF Inv, TypeOK, a
<6>4. QED
BY <6>2, <6>3
<5>3. QED
BY <5>1, <5>2
<4>4. ((pc = "Done") => (result /= 0) \/ (\A i \in 1..Len(seq) : seq[i] /= val))'
BY <3>1, <2>1 DEF Inv, TypeOK, a
<4>5. QED
BY <4>1, <4>2, <4>3, <4>4 DEF Inv
<3>2. CASE ~(low =< high /\ result = 0)
BY <3>2, <2>1 DEF Inv, TypeOK, a
<3>3. QED
BY <3>1, <3>2
<2>2. CASE UNCHANGED vars
BY <2>2 DEF Inv, TypeOK, vars
<2>3. QED
BY <2>1, <2>2 DEF Next, Terminating
<1>3. Inv => resultCorrect
BY DEF resultCorrect, Inv, TypeOK
<1>4. QED
BY <1>1, <1>2, <1>3, PTL DEF Spec
================================================================================
\* Modification History
\* Last modified Fri Feb 17 16:12:03 CET 2023 by merz
\* Last modified Tue Aug 27 12:59:52 PDT 2019 by loki
\* Last modified Fri May 03 16:28:58 PDT 2019 by lamport
\* Created Wed Apr 17 15:15:12 PDT 2019 by lamport