A simple intended function may consist of one or more lines of the form
state-item := expressionThis means that during the execution of the function, the given expression is computed and assigned to the state-item.
A state-item may be:
a := b + c - 1
quitButton := quitButton with its text changed to red
# [ <stdout> := <stdout> + "Arrr." + newline ] sys.stdout.write ( "Arrr.\n" );In this example, <stdout> is a notational shorthand for the process's standard output stream.
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 = iThis 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.