Next / Previous / Contents / Shipman's homepage

5. Intended function notation

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:

We break our discussion of intended function construction into three parts.

5.1. Simple intended functions

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 ] to 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.

Important

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 items x and y. 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 “x gets the old value of y, and y gets the old value of x.”

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 x. 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 print statement is the same as sys.stdout, so 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.

  1. 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) ]
    
  2. 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.

  3. 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”.