An example of a specification is:




must both be true. Informally, a Coin doesn't get you more or less than 1 games and the GAMES machine cannot be better than that 1 coin ahead. (In some sense, we have ;SPM_quot;contracted;SPM_quot; in the s/w engineering sense, not to rip off the customer or the games manufacturer).