Next / Previous / Contents / Shipman's homepage

2.3. Application example

Let's turn now to an example of a prime and analyze the routes through it. Here is an intended function:

    [ if a is zero ->
        x  :=  0
      else if b is positive ->
        x  :=  y + 1
      else ->
        x  :=  y - 1 ]

The possible paths through this prime are governed by two conditions, which we will call C1 and C2.

There are three paths through the code, because if C1 is true, we don't care whether C2 is true or not. So our truth table has three cases.

C1C2Case
TXC1
FFC1′ ∧ C2′
FTC1′ ∧ C2