1 PDD
2 Computing the
Max
2.2 The Algorithm 3. Errors 4. More Complete Testing 4.1 Functions Project Prev: Session 2 Next: Session 4 Contents 
1 Property Driven DevelopmentWe will now consider a very simple algorithm, one that actually computes something: the maximum of a tuple of numbers. You may have heard about Property Driven Development (PDD). Programmers typically start with a general idea of what a program should do and work out the details as they write the code. The idea of PDD is that you should decide precisely what a program should do before writing the code that describes how the program does it. The what are the properties the program's output should satisfy. PDD helps avoid this mistake: After writing a large part of the program, the programmer realizes her code doesn't handle some special case or satisfy some subtle property that it should. She must then either throw away a lot of what she has done, or else correct the problem with ad hoc patches that produce an ugly, hard to maintain program. PDD also aids in writing tests, because the properties that the program's output should satisfy are precisely what need to be tested. I have been told that at Microsoft, the strongest advocates of writing those properties are the groups that test software. PlusCal is well suited to PDD because we can check directly if the algorithm satisfies its required properties. After writing the properties, there is no need to write (nontrivial) code to test that the algorithm satisfies them.
2 Computing the Max of a Tuple2.1 Pre/PostconditionsWe'll see how PDD works with an algorithm to compute the maximum of a tuple of numbers. Let's assume that the tuple is the value of a variableinp and that its maximum is to be put in the
variable max . The property to be satisfied is that,
when the program terminates, max equals the maximum of
all the values of inp[n] for all n in the
index set 1..Len(inp) . This means that
max must satisfy two conditions:
(\E n \in 1..Len(inp) : max = inp[n]) Why parentheses are needed. /\ (\A n \in 1..Len(inp) : max >= inp[n])We can get TLC to check that this condition holds by putting it in an assert statement that is executed just before the
algorithm terminates. This kind of property is called a
postcondition of the algorithm.
Very often, we don't expect an algorithm to work for all conceivable inputs. It needs to meet its goal only for inputs satisfying some condition. To simplify our algorithm's task, let's suppose that we care only about input tuples whose values are greater than some number—say the number 99999. This assumption is expressed as: \A n \in 1..Len(inp) : inp[n] > 9999This kind of assumption is called a precondition of the algorithm. It will go in an assert statement at the
beginning of the algorithm, so TLC will stop the execution and report
an error if we try running the algorithm on input it's not designed to
handle.
2.2 The Algorithm
Open the specification EXTENDS Integers, Sequences, TLCThis statement imports definitions from three standard TLA+ modules into the current module. The modules and what they define are:
Nothing can come before an
Next comes a comment containing
algorithm
The computation is done in the obvious way, examining the tuple
elements while (test) { body }evaluates the expression test and, if it equals
TRUE , executes the code body and then
executes the while statement again. If
test equals FALSE , then execution of the
while statement terminates and control passes to the next
statement. Thus, if test is initially false, then
body is not executed at all. In our algorithm, the
body of the while increments i by 1, so it
is executed with i equal to 1, 2, and 3, since
Len(inp) equals 3 (the number of elements in the tuple
inp ).
The if (test) { if_body } else { else_body }where the part beginning with else can be omitted. If
the expression test is true, then the code
if_body is executed. If test is false and
the else part is present, then the code
else_body is executed. The curly braces { }
around if_body can be eliminated if that code consists of
a single statement, and similarly for the braces around
else_body . However, those braces make the code easier to
read and I recommend always using them.
The complete algorithm is: algorithm TupleMax { variables inp = <<1, 3, 2>>, max = 99999, i = 1 ; { assert \A n \in 1..Len(inp) : inp[n] > 99999 ; while (i =< Len(inp)) { if (inp[i] > max) { max := inp[i] } ; i := i + 1 } ; assert (\E n \in 1..Len(inp) : max = inp[n]) /\ (\A n \in 1..Len(inp) : max >= inp[n]) } }Run the translator, then create a new model and run TLC on it. TLC should report no error. Let's test it on another tuple by changing the initial value of inp . If you're an
experienced programmer and write a piece of code that takes an array
as input, and that code seems to be working, you know that you should
probably test it on an array of length 0—one with no
elements. So, set the initial value of inp to
<< >> , translate, and run TLC. This raises an error
window that looks something like the following. (The line and
column numbers may not be quite the same as in the error window you
get.)
Clicking on line 14, column 6
takes you to the beginning of the
The error message makes it pretty clear that the error was an
We have discovered that the code does not satisfy its
postcondition for the input
The simplest fix is to decide that the code doesn't have to handle
that case. We just add to the precondition the conjunct
The alternative is to change the code and/or the postcondition.
Since we are already assuming that the elements of the tuple are
greater than 99999, we can change the postcondition to require
It's more elegant to have the postcondition stated as an
IF inp = << >> THEN max = 99999 ELSE (\E n \in 1..Len(inp) : max = inp[n]) /\ (\A n \in 1..Len(inp) : max >= inp[n])Don't confuse this IF expression with the if
statement. The if statement describes something the
algorithm is to do. The IF expression is an expression
that describes a value—in this case a Boolean value, but it
could be any kind of value. Only the test, in this case
inp = << >> , has to be a Boolean value. Note that there
is no delimiter to end the ELSE expression. If an
IF expression occurs in the middle of a formula, you may
have to enclose it in parentheses to prevent what follows it from
becoming part of the ELSE clause.
Replace the if statement you added to test the
postcondition with an assert of this formula, and have
TLC check it.
The algorithm still contains some particular tuple used for testing
as the initial value of 2.3 Declaring a Constant
The use of the arbitrary number 99999 in the algorithm is ugly.
And if the algorithm were not so trivial, it might not be clear that
any sufficiently small number could be used instead. It's better
to replace 99999 by an unspecified integer. Let's call it
CONSTANT minValueThis declares minValue to be an unspecified constant.
We don't want it to be completely unspecified; we want to say that
it's an integer.
Recall that the set of all integers is written
Int , so we assert the assumption that minValue
is an integer by adding this statement after the CONSTANT
declaration.
ASSUME minValue \in IntTLC checks ASSUME statements.
Modify the algorithm by substituting
TLC can't check an algorithm containing a constant just knowing
that it's an integer. For it to check the algorithm, we have
to tell it what value to use for
That new window provides the three options shown to the left.
The Ordinary assignment option lets you enter any constant
value you want for 3 Errors We make lots of little errors when writing an algorithm, so let's
take a closer look at TLC's error reports. Just so we'll be
working with exactly the same specification, open a new specification
with module
Now introduce an error by changing
This time, examine the error trace section of the window, which should
look like the one shown here on the left. The trace describes
the execution of the algorithm as a sequence of 4 steps, where a step
goes from one of the 5 states to the next. A state is an
assignment of values to variables. (Values that have changed
since the previous state are highlighted in pink.) In addition
to the three variables declared by the
The first step (from state number 1 to state number 2) represents the
execution of the
TLA+ describes an execution of an algorithm as a sequence of
steps. How an execution is split into steps doesn't matter for
the uniprocess algorithms we are now considering. For
efficiency, the translator by default splits them into the smallest
number of steps it can. What constitutes a step is a vital part
of the description of a multiprocess algorithm. You'll see later
how steps are specified. For now, the error trace and the
locations reported in the error message should let you figure out what
caused an error. The error raised by the 4 More Complete Testing
This version of algorithm
The obvious approach is to test it on randomly chosen, realistic
inputs. These would be large tuples—especially if we
expect the algorithm to be used with inputs that are tuples having
millions of elements. Some testing of large inputs might be
necessary to ensure that the algorithm is efficient enough.
However, that's not a good way to look for inputs that satisfy the
precondition and violate the postcondition. To see why, consider
this error one might make in the algorithm: writing
Instead of testing the algorithm with randomly chosen 1000tuples, it
would be better to test it with all possible 3tuples. We can't
do that because there are an infinite number of integers, so there are
an infinite number of 3tuples of integers. However, we can
effectively test it for all 3tuples by testing it on all 3tuples
with elements in a set of three different integers. This is
because the behavior of the algorithm depends only on whether an
element of the tuple is greater than, less than, or equal to other
elements, not on the actual values of the elements. For example,
algorithm 4.1 Functions and Sets of Functions
As you've seen, a 3tuple is an array with index set
The set of all functions having domain
\A i \in D : f[i] \in SThus, [1..3 > S] is the set of all 3tuples with
elements in S . For testing TupleMax , we take
S to be a set of three integers. We could let S
equal 1..3 . However, letting the values in
S not be in 1..3 makes it easier to
understand an error trace because we can see if a number is an element
of the tuple or of its domain. So, let's test the set
[1..3 > 3..1] of 3tuples.
4.2 Initial Value SetsWith PlusCal, we don't test an algorithm by giving it multiple inputs; we write an algorithm that allows multiple behaviors, each corresponding to a different input. Here, we don't write an algorithm that allowsinp
to have a single initial value and then change that value.
Instead, we write an algorithm that allows the initial value
of inp to be any element of a set of values.
TLC will check executions starting with all possible initial values.
If we want our algorithm to allow the initial value
of
inp \in [1..3 > 3..1] We want to test the algorithm for additional tuples as
well. We could initialize
However, TLC would then not be able to check the algorithm because
it would allow infinitely many initial states. It's possible to tell TLC
to check it on only a finite subset of them, but doing that is a little
complicated. An easier approach is to define a constant that
is assumed to be a set of tuples of integers and allow the initial value
of
We can add another
CONSTANT minValue, TuplesInstead of adding a separate ASSUME statement to say that
Tuples is a set of tuples of integers, we can add it to the
existing assumption as:
ASSUME (minValue \in Int) /\ (Tuples \subseteq Seq(Int))Then change the declaration of inp to
inp \in Tuples .
We can now replace the precondition of the algorithm by an assumption about
ASSUME (minValue \in Int) /\ (\A t \in Tuples : \A i \in 1..Len(t) : t[i] > minValue) /\ (Tuples \subseteq Seq(Int))TLA+ has a convention that most mathematicians hate and most engineers love: We can write this formula, which is a conjunction of three formulas, as a bulleted list of those three formulas with /\ as the bullets:
ASSUME /\ (minValue \in Int) /\ (\A t \in Tuples : \A i \in 1..Len(t) : t[i] > minValue) /\ (Tuples \subseteq Seq(Int))The /\ bullets should be
perfectly
aligned. The reason this is a great notation is that such a list
is parsed as if there were parentheses around each of the items. We
therefore don't need the explicit parentheses and can write this
statement as:
ASSUME /\ minValue \in Int /\ \A t \in Tuples : \A i \in 1..Len(t) : t[i] > minValue /\ Tuples \subseteq Seq(Int)We can also eliminate the parentheses in the assertion of the postcondition by writing it as:
assert IF inp = << >> THEN max = minValue ELSE /\ \E n \in 1..Len(inp) : max = inp[n] /\ \A n \in 1..Len(inp) : max >= inp[n]This convention for writing conjunctions as bulleted lists is also used to write a disjunction as a list of formulas bulleted with \/ . It is especially useful for a list of
disjunctions inside a list of conjunctions, or viceversa.
Now let's test algorithm
[{1} > {1}] \cup [1..2 > 2..1] \cup [1..3 > 3..1]Run the model; it should find no error. Everything seems fine, except we haven't checked it on the empty tuple. Edit the value the model assigns to Tuples by
doubleclicking on its entry on the Model Overview subtab, and
add the empty tuple to that set. (You do this by taking the
union of the current value with the set containing only the empty
tuple.)
Puzzle How many different ways can you write
the set containing only the
Answer
The obvious way is \A i \in {} : f[i] \in Sis true for any set S because any formula
\A i \in {} : ...
is true. In particular, we can write it as
[{} > {}] .
Since 1..0 and 0..1 equal the empty
set {} , we can also write it
[1..0 > 0..1]
so it looks just like the other sets of tuples we will use.
Run TLC on the model again to make sure the algorithm still works
for the empty tuple. You can also change the
Project
You will write two algorithms by yourself.
Put each one in a new specification, which you create the same way you opened
a specification in
Section 2.1 of Session 1,
except by browsing to any folder you want and entering a nonexisting
file name (with no extension) as the name of the specification.
For each algorithm, use our modified version of algorithm
^ , where
m ^ n equals m^{n} , defined only
if n is nonnegative. Write an algorithm to
compute m ^ n by multiplying m by itself
n times.
You can use ^ in an
assert statement to check the correctness of your
algorithm. Try to test it on maximal pairs of sets of values for
m and n that TLC can handle—pairs
such that TLC will fail if one additional number is added to either
set. For example, 8..1 \cup 1..8 and 0..10 is
one such pair on my computer.
Part 2.
The algorithm in Part 1 uses about
\A m, n \in Int : (n > 0) => /\ m = n * (m \div n) + (m % n) /\ (0 =< m % n) /\ (m % n < n)
Hint:
back to top
