Next / Previous / Contents / Shipman's homepage

5.3. Compound intended functions

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.

Formally:

simple intended function

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.

compound intended function

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:

  1. The conditions are examined to see which simple intended function applies in this case.

  2. The state changes for the selected simple intended function occur simultaneously.

Here is the general form as it might appear in the code:

    # [ if C0 ->
    #     S0
    #   else if C1 ->
    #     S1
    #   else if ...
    #     ...
    #   else ->
    #     Sn ]

Each Ci is a description of some condition, and each Si is a simple intended function.

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.

C0C1Case
TTS0
TFS0
FTS1
FFS2

Note that two lines of the above truth table have the same simple intended function. Using the convention from digital logic that “X” means “don't care”, the above truth table can be reduced to three rows:

C0C1Case
TXS0
FTS1
FFS2

Here is a concrete example: an intended function for a call to Python's str.isdigit() method.

    # [ 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.