Contracts may be quite complex, as complex as code in fact, so it is not surprising that they contain errors sometimes. GNATprove can help by pinpointing suspicious constructs that, although legal, do not make much sense. These constructs are likely to be caused by mistakes made by the programmer when writing the contract.

For example, consider the following procedure postcondition that contains a typo:

Did you spot the typo? GNATprove did and it signals it with a warning:

Indeed, the first occurrence of X in the postcondition of Bad_Max should really be Z, the output parameter of the procedure. As a result of this typo, the postcondition is now only referring input values, which is definitely not expected in a postcondition! At least one output value should be mentioned, hence the warning.

Let's consider a variant of Bad_Max in which a parameter is updated with the maximum value of its parameters:

There is again a typo in this contract: the uses of X and Y should be reversed. GNATprove detects that, although it is legal, applying attribute Old to get the input value of Y does not make sense as Y is not modified in the procedure:

The most typical error though is when writing the contract of a function returning a boolean value. It is very easy to write the wrong contract:

Here, the postcondition of Bad_Is_Increasing is expressing what we'd like the result to be: True when X is less than Y, False otherwise. But this is not what the postcondition above expresses. Instead, it states that when Bad_Is_Increasing returns, X should always be less than Y! GNATprove detects that problems and signals it with two warnings:

The correct postcondition for Bad_Is_Increasing is indeed:

Now, it is common in postconditions to compare the input value and the output value of a parameter, something that is facilitated for composite objects (arrays and records) by the use of the attribute Update.

One common mistake when using attribute Update in that context is the following:

Did you spot the mistake? GNATprove did and it signals it with a warning:

The issue here is that we mean to compare the output value of S with its updated input value, which is expressed with S'Old'Update. S'Update means instead the updated output value of S, so in effect the above postcondition compares the output value of S with an updated version of itself, which is unlikely to be true, hence the warning.

The correct postcondition for Bad_Capitalize is:

Other common mistakes involve the use of quantifiers. The existential quantifier (for some) expresses that a property holds for a value in a given range. The universal quantifier (for all) expresses that a property holds for all values in a given range. The example below shows common mistakes involving these quantified expressions. Procedure Bad_Find_Next should take as input a string S and an index I in S such that the character in S at index I can also be found at a greater index in S. The procedure should find this index and return it in output parameter J.

Found the problems? GNATprove did and it signals them with warnings. For the existential quantification in the precondition, it issues:

Indeed, we want to express here that there is an index K greater than I such that S(K) is the same as S(I). The form (for some X => (if P then Q)) is a common mistake made in such a case to express that property. This form of expression is rarely relevant, because it will be true in almost all cases, as soon as there is a value of K here that is less than or equal to I, because that invalidates the test in the if-expression, which results in the whole if-expression being true (remember that (if P then Q) is the same as (if P then Q else True)).

The warnings suggest possible correct ways to express our properties. Here, the correct way is (for some K in S'Range => K > I and then S(K) = S(I))

For the universal quantification in the postcondition, GNATprove issues the warning:

Indeed, K is not mentioned at all in the expression S(J) /= S(I)! This cannot be intentional. The correct postcondition here is (for all K in I+1 .. J-1 => S(K) /= S(I));

I mentioned GNATprove above because I assumed a workflow where a user develops contracts on her code without necessarily compiling, but the GNAT compiler also issues all these warnings by default. They can be disabled with the compilation switch -gnatw.T, as documented in the GNAT User's Guide.

We'll keep enhancing GNAT and GNATprove with other useful warnings for helping developers with contract based programming, so let us know about your other needs in that area.