Part of the 4-part video series on Refinement & Abstraction in TLA+

bubble_sort.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

sort.tla

-------------------------------- 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

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