Next / Previous / Shipman's Home Sweet Homepage / Site map

Cleanroom intended functions: Simple I/Fs

A simple intended function may consist of one or more lines of the form

    state-item  :=  expression
This means that during the execution of the function, the given expression is computed and assigned to the state-item.

A state-item may be:

Important: All the lines of an intended function are assumed to execute in parallel, that is, you may not make any assumption about which order they are executed in.

As a consequence of this rule, if a state-item appears in one of the expressions in an I/F, we always assume that we are talking about the state of that item on entry to the function.

Consider this I/F and accompanying code:

    # [ (i, j)  :=  (i+1, i+1) ]
    i  =  i + 1
    j  =  i
This I/F matches its code, because after its execution, j will contain the original value of i, plus one.

I also use the common C and Python convention that an operator can appear to the left of the ":=" to mean modification in place. For example,

    <stdout>  +:=  "Arr.\n"
is shorthand for
    <stdout>  :=  <stdout> + "Arr.\n"

Additional, more specialized I/F lines are discussed in the next topics, Cleanroom intended functions: Prose I/Fs and Cleanroom intended functions: Special I/Fs.

Next: Cleanroom intended functions: Prose I/Fs
See also: Writing Cleanroom intended functions
Site map
John W. Shipman,
Last updated: 2002/09/28 01:30:39