|
Intermezzo 1 Sequences
Leslie Lamport
Last modified on 1 December 2021
|
|
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-
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[1]. 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.
|