Prev:  Session 9

Next:  Session 10

Contents

Intermezzo 1   Sequences

Leslie Lamport

It's time to pause the study of algorithms and learn some more about finite sequences, also known as tuples.  After numbers and sets, I think they are the most commonly used data type in PlusCal specifications.  Except when discussing behaviors, which are sequences of states that can be infinite, I use the term sequence to mean a finite sequence—unless I precede it by infinite.

You've already learned that Len(seq) is the length of a sequence seq, and that Seq(S) is the set of all sequences whose elements are all in S.  You also know that a sequence seq is a function with domain 1..Len(seq), so it equals

[i \in 1..Len(seq) |-> seq[i]]
Here are some other operators on sequences:
Head(seq) is the first element of a non-empty sequence seq.  For example, Head(<<"a", "c", "b">>) equals "a".
Tail
Tail(seq) is the sequence obtained by removing the first element from the non-empty sequence seq.  For example, Tail(<<"a", "c", "b">>) equals <<"c", "b">>.
Append
Append(seq,e) is the sequence obtained by appending the value e as the new last element of the sequence seq. For example, Append(<<1, 2>>, 42) equals <<1, 2, 42>>.
\o   (concatenation, pretty-printed   )
seq1 \o seq2 is the sequence obtained by concatinating the sequences seq1 and seq2 in the obvious way.  For example, seq \o <<e>> equals Append(seq,e) for any sequence seq and value e
SubSeq
SubSeq(seq, m, n) for a sequence seq and integers m and n is the subsequence of seq containing the elements seq[i] for i in m..n.  It is defined iff m..n \subseteq 1..Len(seq) is true.  For example, SubSeq(<<"a", "b", "c", "d">>, 3, 4) equals <<"c", "d">>.
There is also an operator SelectSeq for describing the subsequence of a sequence containing only the elements satisfying some criterion.  You can learn about it in Section 18.1 of Specifying Systems

Observe that <<Head(seq)>> \o Tail(seq) equals seq for any non-empty sequence seq.  Both Head(seq) and Tail(seq) are undefined if seq equals << >>.  Of course, Head(seq) is just a long way of writing seq.  However, it's often better to write Head(seq) because many computer engineers are familiar with the operators Head and Tail, while few are used to seq[i] being the ith element of sequence seq.

Exercise   Define the operator RemoveElt such that RemoveElt(n, seq) is the sequence obtained by removing the nth element from the sequence seq, for n in 1..Len(seq) Show the answer.

Answer   RemoveElt(n, seq) should be a sequence of length Len(seq) - 1, so your answer should have the form:

RemoveElt(n, seq) == [i \in 1..(Len(seq)-1) |-> expr]
for some expression expr.  You should be able to find the correct expression by trial and error, using TLC to check your answer.  But a better exercise is to think carefully about what the answer should be so you get it right on the first try.

Puzzle   Find a set S for which Seq(S) is a finite set.  Show the answer.

Answer   The set Seq({}) contains the single element << >>.

Puzzle   The original version of the Sequences module defined:

Tail(seq)  ==  [i \in 1..(Len(seq)-1) |-> seq[i+1]]
what's wrong with that definition?  Show the answer.

Answer   It incorrectly defines Tail(<< >>) to equal << >>.  One way to correct the error is:

Tail(seq)  ==  IF seq /= << >> THEN [i \in 1..(Len(seq)-1) |-> seq[i+1]]
ELSE some undefined expression
What undefined expression would you use?

Additional operators on sequences and operators on other data structures can be found in the Community Modules repository of the TLA+ GitHub Site.