1 PDD

2 Computing the Max

2.1 Pre/Postconditions


2.2 The Algorithm


2.3 Declaring a Constant


3. Errors

4. More Complete Testing

4.1 Functions


4.2 Initial Value Sets


Project

Prev:  Session 2

Next:  Session 4

Contents
 ↑

top

 ↑

top

 ↑

top

 ↑

top

 ↑

top

 ↑

top

 ↑

top

 ↑

top

 ↑

top

 ↑

top

 ↑

top

 ↑

top

 ↑

top

 ↑

top

 ↑

top

 ↑

top

 ↑

top

Session 3   A Simple Algorithm

Leslie Lamport

Last modified on 6 December 2021


1  Property Driven Development

We 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 (non-trivial) code to test that the algorithm satisfies them.

2  Computing the Max of a Tuple

2.1  Pre/Postconditions

We'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 variable inp 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:
  • max must equal some inp[n]
  • max must be greater than or equal to all inp[n]
These two conditions can be written mathematically as this single formula.

      (\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] > -9999 
This 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 Session3.  This time, let's look at the module's first statement:

EXTENDS Integers, Sequences, TLC

This statement imports definitions from three standard TLA+ modules into the current module.  The modules and what they define are:

Integers  Defines standard operators of arithmetic like + and =<, the integer interval operator .., and the sets Nat and Int.

Sequences  Defines operators on tuples (finite sequences) including Len.

TLC  Defines operators used in the TLA+ translation of some PlusCal statements, including print.

Nothing can come before an EXTENDS statement in the body of the module except comments.

Next comes a comment containing algorithm TupleMax.  The algorithm's variables statement declares the input and output variables inp and max and a variable i also used in the code.  The initial value of inp is an arbitrary tuple used to test the code.  We'll see later how to do more thorough testing.  Following the variables statement is an assert statement that checks the precondition.

The computation is done in the obvious way, examining the tuple elements inp[1], inp[2], etc. in order and keeping max equal to the largest value it has found.  If you're acquainted with popular programming languages, it will probably look familiar.  The standard way to write a loop in PlusCal is with a while statement.  The statement

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 statement has the general form

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 assert statement in the code.  At the bottom of the message in the error window is a list of positions in the algorithm's TLA+ translation.  The last one is usually the most relevant one.  Clicking on it takes you to the part of the TLA+ translation whose execution caused the error.  But you don't want to look at the translation now.  You can go to the part of the PlusCal code that produced that part of the translation by pressing the F10 key.  You can go directly from the error window to the PlusCal code by control-clicking (holding down the control key when you click) on that line in the error message. 

The error message makes it pretty clear that the error was an assert statement whose expression was false.  It's not always so easy to figure out what caused the error TLC is reporting.  Going to the PlusCal code that was being evaluated when the error occurred can be a big help.

We have discovered that the code does not satisfy its postcondition for the input inp equal to << >> that satisfies the precondition.  So, we have to change the precondition to disallow that input, fix the code, or change the postcondition.  Which we do depends on what the code will be used for.  Since this is a toy example, it's not going to be used for anything.  So let's look at the possibilities and pick the one that's the most fun.

The simplest fix is to decide that the code doesn't have to handle that case.  We just add to the precondition the conjunct inp /= << >> or the conjunct Len(inp) > 0.  But that's no fun; it's too easy.

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 max to get the value -99999 if inp equals << >>.  We don't even have to change the code; that's what it already does.  We just have to modify the postcondition.  This can be done by replacing the assert statement that asserts the postcondition with an if statement (with an else clause) containing two assert statements.  One clause, executed when inp equals << >>, asserts max = -99999.  The other clause contains the current assert statement.  Do that now and have TLC check that it works—both for inp equal to << >> and equal to a couple of other tuples.  (Don't forget to save the file and run the translator each time before running TLC.)

It's more elegant to have the postcondition stated as an assert of a single formula. That formula can be written as

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 inp.  We'll fix that below.

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 minValue.  Put the following statement in the Session3 module, after the EXTENDS statement and before the comment containing the algorithm.

CONSTANT minValue
This 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 Int
TLC checks ASSUME statements. 

Modify the algorithm by substituting minValue for each of the three instances of -99999.  Save the module and run the translator.  Now let's check it.  Click on your model's tab.  It will probably open to the Model Checking Results sub-tab.  Whichever sub-tab it's on, there will be a link at the top saying 1 error detected.  Clicking on that link takes you to the Model Overview sub-tab.  Hovering the mouse over either of the two icons reveals the problem to be that you have to provide a value for the constant minValue

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 minValue. We do this in the section of the sub-tab shown to the right.  Click on the Edit button, which raises a menu in which you can specify the value of minValue

That new window provides the three options shown to the left.  The Ordinary assignment option lets you enter any constant value you want for minValue in the window.  Let's set it to -99999.  Enter that value and click Finish (or type Control-Enter) to close the window.  Run TLC and check that you haven't introduced any error when making the changes.

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 Session3a.  It contains a version of algorithm TupleMax that should be the same as the modified version of TupleMax now in your module Session3, except with the original initial value <<1,3,2>> for inp.  The specification should already contain the translation and a model named Model_1.  Open that model and run it to make sure everything is OK.

Now introduce an error by changing max >= inp[n] in the assert statement to max > inp[n].  Run the translator and run TLC on the model.  TLC should raise an error window reporting that the assertion is violated.

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 variables statement, there is a variable pc introduced by the TLA+ translation; you can ignore it for now.

The first step (from state number 1 to state number 2) represents the execution of the assert statement.  The second step represents a complete execution of one iteration of the while loop: evaluation of the test i =< Len(inp), execution of the if statement, and execution of the assignment to i.

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 assert statement occurred when TLC was computing the state after the last one in the trace.  In this case, the last state in the trace was the one in which TLC was about to evaluate the while test with i = 4, and TLC executed the assert statement that raised the error while it was computing the next state.  TLC produces no error trace for an error that occurs when it is computing the initial values of the variables.

4  More Complete Testing

This version of algorithm TupleMax still contains an arbitrary initial value for inp. We could declare a new constant that we could use for that initial value.  We would test different inputs by changing the value assigned to the constant by the TLC model.  This algorithm is so simple that not much testing is required to convince ourselves that it's correct, so that's a reasonable approach.  But let's pretend that the algorithm is performing some difficult computation on tuples and we want to be sure it has no subtle error.  How would we test it?

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 =< in the while statement's test.  This causes an error only if the maximum element is the last one in the tuple.  We're much more likely to catch that error with a randomly chosen 3-tuple than with a randomly chosen 1000-tuple.

Instead of testing the algorithm with randomly chosen 1000-tuples, it would be better to test it with all possible 3-tuples.  We can't do that because there are an infinite number of integers, so there are an infinite number of 3-tuples of integers.  However, we can effectively test it for all 3-tuples by testing it on all 3-tuples 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 TupleMax behaves the same with the inputs <<2, 8, 2>> and <<-7, 0, -7>> because both tuples have their first and third elements equal to each other and less than their second element.  Any error that occurs with a 3-tuple input will be found by choosing an arbitrary set of three integers and testing the algorithm on all 3-tuples whose elements belong to that set.  We'll now see how to write such a set of 3-tuples and get a PlusCal algorithm to use it.

4.1  Functions and Sets of Functions

As you've seen, a 3-tuple is an array with index set 1..3.  Mathematicians call an array a function, and they call its index set its domain.  I will use the mathematicians' terms because I want you to learn to think about algorithms mathematically.  (This will also let you think of arrays as only having elements numbered from 0, if you want to.)  But remember that TLA+ writes the value of the function f applied to the element e in its domain as f[e], not as f(e) the way mathematicians do.

The set of all functions having domain D and having values in a set S is written in TLA+ as [D -> S].  In other words, [D -> S] is the set of all functions f with domain D for which this is true:

\A i \in D : f[i] \in S
Thus, [1..3 -> S] is the set of all 3-tuples 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 3-tuples.

4.2  Initial Value Sets

With 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 allows inp 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 to be any 3-tuple with elements in -3..-1, we just change the declaration of inp in the variables statement to:

inp \in [1..3 -> -3..-1]

We want to test the algorithm for additional tuples as well.  We could initialize inp to the set of all tuples we want to test it on.  However, if this were an algorithm that we wanted to show to other people, we would want to describe the set of all allowed initial values of inp.  Since the initial value of inp can be any tuple of integers, the variables declaration should allow inp to be any element in the set of all such tuples.  The set of all tuples with elements in a set S is written in TLA+ as Seq(S) (Why Seq?)  So, we should write int \in Seq(Int) in the variables declaration. 

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 inp to be any element of that set.  We can then tell TLC to substitute for that constant the set of initial values of inp for which we want to test the algorithm.  Let's call that constant Tuples

We can add another CONSTANT declaration for Tuples to the module, but I usually prefer to declare all constants at once.  So, change the existing declaration to:

CONSTANT minValue, Tuples
Instead 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 minValue. Instead of asserting that all the elements of inp are greater than minValue, we can require that all the elements of all the tuples in Tuples are greater than minValue.  We can do this by adding a condition to the ASSUME statement as follows:

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 vice-versa.

Now let's test algorithm TupleMax on lots of tuples.  Save the file, run the translator, and open the model.  You will see that there is now an error in the model because the constant Tuples has not been assigned a value.  Go to the Model Overview sub-tab and double-click on Tuples in the What is the model section.  Copy and paste the following set of tuples as the value:

 [{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 double-clicking on its entry on the Model Overview sub-tab, 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
0-tuple << >> Show the answer.

Answer   The obvious way is {<< >>}.  It can also be written [{} -> S] for any set S, since the domain (index set) of the 0-tuple contains no elements, so it is the empty set; and

\A i \in {} : f[i] \in S
is 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 while test to i < Len(inp) and check that TLC finds the error.

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 non-existing file name (with no extension) as the name of the specification.  For each algorithm, use our modified version of algorithm TupleMax from module Session3a as a template, copying its EXTENDS statement.  Do not try to open a model for a specification until you have written and successfully translated its algorithm.

Part 1.  TLA+ has the exponentiation operator ^, where m ^ n equals mn, defined only if n is non-negative.  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 n multiplications to compute m ^ n.  Write an algorithm that uses only about log2n multiplications.  You will need to use these two TLA+ operators:

Integer Division  \div  (pretty-printed ÷)
m \div n is the largest integer less than or equal to m / n.  For example, 5 \div 2 equals 2 and (-5) \div 2 equals -3.  (But -5 \div 2 equals -(5 \div 2), which equals -2.)
Modulo  %
m % n is the non-negative remainder when the integer m is divided by the positive integer n.  For example, 5 % 2 and -5 % 2 both equal 1.  Thus, m % n equals 0 iff m is a multiple of n.
The precise definitions of these two operators make this formula true:

 \A m, n \in Int :
    (n > 0) => /\ m  =  n * (m \div n)  +  (m % n)
               /\ (0  =< m % n)  /\  (m % n < n)

Hint:   m ^ 13 = (m ^ 8) * (m ^ 4) * (m ^ 1)