Skip to content

Instantly share code, notes, and snippets.

@JeremyLWright
Created February 19, 2022 20:44
Show Gist options
  • Save JeremyLWright/8dcbb7a6953e9b82175b74297562333f to your computer and use it in GitHub Desktop.
Save JeremyLWright/8dcbb7a6953e9b82175b74297562333f to your computer and use it in GitHub Desktop.
Part of the 4-part video series on Refinement & Abstraction in TLA+
---------------------------- MODULE bubble_sort ----------------------------
EXTENDS SequencesExt, Sequences, Integers, TLC, Naturals
CONSTANTS N
ASSUME NonEmptyArray == N \in Nat /\ N > 1
(*--fair algorithm BubbleSort {
variables A \in [1..N -> Nat], A0 = A, i = 1, j = 1, totalSteps = 1;
{ while(i < N)
{
j := i + 1;
while(j > 1 /\ A[j - 1] > A[j])
{
A[j - 1] := A[j] || A[j] := A[j - 1];
j := j - 1;
totalSteps := totalSteps + 1;
};
i := i + 1;
totalSteps := totalSteps + 1;
};
}
}
*)
\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "898549ba")
VARIABLES A, A0, i, j, totalSteps, pc
vars == << A, A0, i, j, totalSteps, pc >>
Init == (* Global variables *)
/\ A \in [1..N -> Nat]
/\ A0 = A
/\ i = 1
/\ j = 1
/\ totalSteps = 1
/\ pc = "Lbl_1"
Lbl_1 == /\ pc = "Lbl_1"
/\ IF i < N
THEN /\ j' = i + 1
/\ pc' = "Lbl_2"
ELSE /\ pc' = "Done"
/\ j' = j
/\ UNCHANGED << A, A0, i, totalSteps >>
Lbl_2 == /\ pc = "Lbl_2"
/\ IF j > 1 /\ A[j - 1] > A[j]
THEN /\ A' = [A EXCEPT ![j - 1] = A[j],
![j] = A[j - 1]]
/\ j' = j - 1
/\ totalSteps' = totalSteps + 1
/\ pc' = "Lbl_2"
/\ i' = i
ELSE /\ i' = i + 1
/\ totalSteps' = totalSteps + 1
/\ pc' = "Lbl_1"
/\ UNCHANGED << A, j >>
/\ A0' = A0
(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == pc = "Done" /\ UNCHANGED vars
Next == Lbl_1 \/ Lbl_2
\/ Terminating
Spec == /\ Init /\ [][Next]_vars
/\ WF_vars(Next)
Termination == <>(pc = "Done")
\* END TRANSLATION
TypeOK == /\ i \in 1..N
/\ j \in 1..N
/\ A \in [1..N -> Nat]
/\ A0 \in [1..N -> Nat]
/\ pc \in {"Lbl_1", "Lbl_2", "Done"}
IsCompletelySorted == \A a, b \in 1..N: a < b => A[a] <= A[b]
ComputationalComplexity == totalSteps <= N * N
SortedWhenDone == pc = "Done" => IsCompletelySorted
Mapping ==
INSTANCE sort WITH
\* magic sort side <- bubble sort side
A <- IF pc = "Done" THEN A ELSE A0
Refinement == Mapping!Spec
=============================================================================
\* Modification History
\* Last modified Sat Feb 19 12:57:14 MST 2022 by jeremy
\* Created Wed Feb 02 09:44:00 MST 2022 by jeremy
-------------------------------- MODULE sort --------------------------------
EXTENDS TLC, Integers, Folds, Sequences, SequencesExt, FiniteSetsExt
CONSTANT N
ASSUME N > 1
VARIABLES A
vars == <<A>>
IsSortedAsc(seq) == \A a,b \in 1..N: a < b => seq[a] <= seq[b]
IsSortedDec(seq) == \A a,b \in 1..N: a < b => seq[a] >= seq[b]
ApplyIndicies(seq, indices) == [ i \in 1..Len(seq) |-> seq[indices[i]]]
PermutationsSeq(seq) == {ApplyIndicies(seq, p) : p \in Permutations(1..Len(seq))}
SortByMagic(seq) == CHOOSE p \in PermutationsSeq(seq) : IsSortedAsc(p)
Init == A = <<2,3,4,5,1>>
Init2 == A \in [1..N -> Nat]
Next == A' = SortByMagic(A)
Spec == Init2 /\ [][Next]_vars /\ WF_vars(Next)
EventuallySortedAsc == <>[]IsSortedAsc(A)
EventuallySortedDec == <>[]IsSortedDec(A)
TypeOK == Len(A) = N
=============================================================================
\* Modification History
\* Last modified Fri Feb 11 13:21:02 MST 2022 by jeremy
\* Created Wed Feb 02 09:18:21 MST 2022 by jeremy
@JeremyLWright
Copy link
Author

JeremyLWright commented Feb 19, 2022

Watch the Video Series on Refinement and Abstraction https://youtube.com/playlist?list=PLacslU3Fwm5sJx5fTcYgOt1oOj0JMKKc5

Untitled Diagram-Page-5

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment