Preconditions

Before a client calls any function of Fsm(3C++), it is the client's responsibility to see to it that the preconditions for that function (if any) are satisfied. The preconditions for each function are specified in the Fsm(3C++) manual page.

Failure to satisfy a precondition leads to undefined behavior. A core dump or an infinite loop might result; even worse, a problem might not turn up until much later in a way that would be difficult to trace.

An example of a function with a precondition is fire(). For the vending machine in the section, ``A Simple Vending Machine'', suppose a bad value of i is returned by the hardware:

       the hardware returns 1000 as the value of i
       v.fire(i);

Since the (one and only) precondition of fire() requires that the value of the argument must lie in the range [0,255]), and since 1000 fails to satisfy this precondition, the behavior of fire() is completely undefined for this call. For example, the vending machine could empty the contents of its cashbox through the coin return.

If the hardware is known to be faulty, then code should be added to to the client to enforce the precondition:

       get the next value of i from the hardware
       if(i>255){
           Turn on the MACHINE TEMPORARILY OUT OF ORDER sign.
           Permanently activate the coin release.
           Place a call to the service beeper number.
       while(1){ }
       }
       v.fire(i);

If, on the other hand, the hardware is robust and never returns a bad value, then the check is unnecessary. The important point is that programs that are known to be correct, either by virtue of correctness arguments (like the one about the robust hardware) or by advance checking of preconditions, should run as quickly as possible.