Every prime (piece of logic) is accompanied by a description of
what it does using intended function notation. Typically the
intended function accompanies the source code as a comment, and
is placed inside
[ square brackets
]. This description is essential to all steps of the method,
and completely describes the interface to that prime.
Formally, an intended function describes a piece of code as a set of simultaneous changes to the state of one or more state items. State items include:
The values of variables.
Attributes of an object, such as the text color of a button on a graphical user interface.
Files: not just their contents, but the current position if open, the states of buffers, and every other stateful aspect of file handling.
External devices and entities such as display screens, servers, TCP/IP sockets, freight trains, medical radiation machines, and so forth.
We break our discussion of intended function construction into three parts.
Section 5.1, “Simple intended functions”: When the prime always does the same thing.
Section 5.3, “Compound intended functions”: When the prime may do different things in different cases.
By simple intended function we mean a set of state changes that are made in every case. If the prime does different things in different cases, see Section 5.3, “Compound intended functions”.
Here is a small example showing an intended function for
two lines of code. The intended function lives in a
comment preceding the code, and is placed in
[ square brackets
distinguish it from other kinds of comments.
# [ x, y := 0, y+1 ] x = 0 y += 1
This form of the intended function follows Dr. Stavely's book. On the
left of the “
:=” symbol is a
list of state items whose state will be changed by the
code. On the right is a list of the new values for each
state item, in the same order.
It is critical to write your intended function so that
conceptually all state changes happen in
parallel. This is especially important when one
of the state items on the left side of the “
:=” also appears on the right side.
If a state item that appears on the left side of a
:=” also appears on the right
side of the same intended function, its value in expressions
on right-hand sides always refers to
its old value, before the execution of that block.
Consider the simple task of exchanging the values of two
. In Python,
this statement works just fine:
x, y = y, x
However, let's assume for the moment that the person who had to write the code came from a C background and assumes you need a temporary variable to exchange two values. Here is a first attempt at the intended function and code.
# [ x, y := y, x ] temp = x x = y y = temp
So when you read the intended function above, the two
assignments happen conceptually in parallel, so we could read
it as “
gets the old value of
gets the old value of
However, the above example violates one of the cardinal Cleanroom rules:
The intended function must match the code.
Here is the corrected intended function and code:
# [ x, y, temp := y, x, x ] temp = x x = y y = temp
The code affects three state
items, not two: after execution, the value of
temp is the old value of
Unless you add the line “
del temp”, that value stays around, and it must be
accounted for during verification.
Life is relatively simple when we're just dealing with the values of variables. The fun begins when we consider input and output, error recovery, and the other baggage of living in a world where the user may be clueless or downright evil.
Let's consider the classic hello-world program. Here is a complete script:
#!/usr/bin/env python # [ sys.stdout := sys.stdout + (a cheery greeting) ] print "Welcome to the Batley Townswomen's Guild!"
Although we haven't explicitly imported
sys here, the destination for the
the notation is clear to anyone who knows Python. The
+” operator here means
string concatenation. We might read the intended
function as: “Whatever was in standard output
before, it's still there, but our cheery greeting has
been added to the end of it.”
Here's an example of an input operation.
# [ inFile, rest := inFile advanced to end of file, # all remaining data from inFile ] rest = inFile.read()
There's a lot more to programming that simple, single operators. When your author was learning this method, he tried to express everything in an algebraic way, but this can made the code harder to read when the application is not primarily an algebra problem.
Writing intended functions is a writing task more than it is a programming task, and your descriptions of the new value of a state item are prose, not code. Here are some examples of intended functions that are quite clear as English.
shoppingList := a set of the unique ingredients from all the recipes in recipeTable horse_list := horse_list with new_horse added scrollBar := scrollBar positioned one page further down but no further than the bottom of the page runButton := runButton grayed out and unresponsive to the mouse locomotive := locomotive with emergency braking applied
You may find that the larger pieces of your design are easier to describe in English, and that the intended functions look more like math as you get closer to the smaller pieces of your design, but this is only a generalization. Use any combination of mathematical notation and English that you think best expresses what the program does. This ability improves with practice, especially when you practice peer verification: in that situation what counts is clarity, clarity that is perceived by the people who didn't write the code.
As with any kind of writing, if you find yourself stuck for a good way to phrase things, try explaining its purpose out loud, to a friend, or to a broom if no one is around. Then write down what you said. It may not be perfect, but it gives you something to work with. The author has found that this method tends to damp down his tendency toward overblown rhetoric (somewhat, at least).
The author deviates from Stavely's intended function notation in a few unimportant ways.
The above intended function could be written in a way
that mimics Python's “augmented
assignment” convention. The formulation below
is the same as the one above, and can be read the
same way: “Whatever was in
sys.stdout there before, it's still there,
but now it has our cheery greeting tacked on.”
# [ sys.stdout +:= (a cheery greeting) ]
Often when an intended function names several state
items, the author will break up intended function
into multiple lines, each one with a “
:=” separating the state item from
its new value. It is important to remember that all
the state changes happen conceptually in parallel,
and the order of these lines does not matter.
For example, in this intended function:
# [ year, month, day, fracDay := year part of date, # month part of date, day part of date, fractional day # from date as a float ]
you have to look carefully to see which state item goes with which new state. The author would break this up so the associations are clear:
# [ year := year part of date # month := month part of date # day := day part of date # fracDay := fractional day from date as a float ]
Still, during verification, all of the changes displayed on multiple lines are considered to happen simultaneously. The order in which you happen to arrange multiple state changes in one simple intended function is not and cannot be important.
Programs do a number of things that do not really fit the model of a state item being changed: they terminate; they raise exceptions; functions return values or just return. For the handling of these cases, see Section 5.5, “Special forms for intended functions”.
All the intended functions above are what we call simple intended functions: the code always makes the same set of state changes. Before we talk about compound intended functions, for code that may do different things in different cases, first read Section 5.2, “Preconditions: The other side of the contract”.