Besides the usual expression of a subprogram contract as a pair of a precondition and a postcondition, SPARK 2014 provides a way to express such a contract by cases. For example, one might specify by cases the work plan of a 15th century castle guard opening the gate to visitors

The cases can be read as follows:

• if the visitor is a beggar, then no gate should be opened
• if the visitor is a serf, then the side gate should be opened
• if the visitor is a merchant, then the small gate should be opened
• if the visitor is high-ranking, then the big gate should be opened

At first sight, it could seem that the above contract can also be expressed as a regular postcondition with an if-expression:

But there is a bit more than that, which makes contract cases more than syntactic sugar for a an if-expression, and a little history might help to understand it.

Previous versions of SPARK only had preconditions and postconditions. This was carried to Ada 2012. But SPARK 2014 also draws its inspiration from other specification languages, such as JML and ACSL, which define the notion of subprogram behavior.

JML is the main specification language for Java. In JML, the specification of a subprogram is either lightweight (made up of a precondition and postcondition), or heavyweight (made up of several behaviors). Each behavior corresponds to a separate contract for the method, with its own precondition (introduced by requires) and postcondition (introduced by ensures). For example, the contract given for Open_Gate would be written as follows in JML:

Each of the behaviors given above is independent from the others, as shown by the desugaring process that transforms this contract into the equivalent:

Note that the precondition is not directly visible on the original contract, as it is the disjunction of all requires clauses of all behaviors.

Note also that the precondition allows calling openGate to a lord coming to ask for money, which would fit both the descriptions of the beggar and the high-ranking visitor, leaving the poor guard worry that he may be blamed for both leaving the gates closed on a high-ranking visitor, or letting in a beggar.

Both issues have been solved in ACSL, a specification language for C that builds on the lessons from JML. In ACSL, the specification of a function can contain both a plain precondition/postcondition pair, and a set of behaviors. For example, the contract given for Open_Gate would be written as follows in ACSL:

The precondition is now in one place, and the case of a begging high-ranking visitor is ruled out by the annotation "disjoint behaviors", which requires that only one behavior applies at any time. The other annotation "complete behaviors" requires that at least one behavior applies at any time.

For SPARK 2014, we started with a design very close to the one of ACSL, with individual contract cases matching the behaviors of ACSL. So initially, the contract of Open_Gate was written:

Our discussions on the (now closed) public mailing list of project Hi-Lite revealed that:

1. the above notation is less readable than the equivalent if-expression
2. the property that each execution matches a unique contract case should be the default

The final synthetic syntax was proposed by Tucker Taft, and we added the rule that contract cases in SPARK 2014 are always disjoint and complete. Et voilà!

Since then, I have found it extremely valuable that contract cases are disjoint and complete, both during proof and testing (yes, these properties are checked at run time when compiling with switch -gnata in GNAT). The concise syntax and the additional expressive power make it indeed valuable to use contract cases in many cases!