When the semantics of a block of code are different depending on runtime conditions, we use a compound intended function. This is basically an if-then-else structure on top of a set of simple intended functions.
A list of state changes that happen simultaneously. Each state change is an ordered pair (vi, ei) where vi is some state item that changes in the prime, and ei is a description of the new value.
A compound intended function is a set of simple intended functions S0, S1, …, and a set of one or more conditions C0, C1, … that select one of the intended functions.
Conceptually, the execution of a prime with a compound intended function proceeds in two steps:
The conditions are examined to see which simple intended function applies in this case.
The state changes for the selected simple intended function occur simultaneously.
Here is the general form as it might appear in the code:
# [ if
S0# else if
S1# else if ... # ... # else -> #
is a description of some
condition, and each
is a simple
The relationship between the conditions and the simple intended functions can be expressed as a truth table. Here is an abstract example:
# [ if C0 -> # S0 # else if C1 -> # S1 # else -> # S2 ]
Here is a presentation of that case structure as a truth table.
Note that two lines of the above truth table have the
same simple intended function. Using the convention from
digital logic that “
“don't care”, the above truth table can be
reduced to three rows:
Here is a concrete example: an intended function for a call to
# [ if (s has at least one character) and # (all of s's characters are digits) -> # digitCheck := True # else -> # digitCheck := False ] digitCheck = s.isdigit()
In more complex cases, if you prefer, you may nest
if” and “
else” clauses. However, be sure that you
have covered all possible cases. Any case that is not
covered is undefined, but this is not good practice;
better practice is to use preconditions to insure that
all cases are covered. A truth table is a good way to be
sure you have considered all the edge cases.