AdaCore Blog

GNATprove Tips and Tricks: Catching Mistakes in Contracts

by Yannick Moy

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:

procedure Bad_Max (X, Y : in Integer; Z : out Integer) with
     Post => X = Integer'Max (X, Y);

Did you spot the typo? GNATprove did and it signals it with a warning: warning: postcondition does not check the outcome of calling "Bad_Max"

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:

procedure Bad_Max (X : in out Integer; Y : in Integer) with
     Post => Y = Integer'Max (X, Y'Old);

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: warning: attribute "Old" applied to constant has no effect

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:

function Bad_Is_Increasing (X, Y : in Integer) return Boolean with
     Post => X < Y;

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: warning: postcondition does not check the outcome of calling "Bad_Is_Increasing" warning: postcondition does not mention function result

The correct postcondition for Bad_Is_Increasing is indeed:

function Bad_Is_Increasing (X, Y : in Integer) return Boolean with
     Post => Bad_Is_Increasing'Result = (X < Y);

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:

procedure Bad_Capitalize (S : in out String) with
     Post => S = S'Update (1 => Ada.Characters.Handling.To_Upper (S(1)));

Did you spot the mistake? GNATprove did and it signals it with a warning: warning: suspicious equality test with modified version of same object

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:

procedure Bad_Capitalize (S : in out String) with
     Post => S = S'Old'Update (1 => Ada.Characters.Handling.To_Upper (S'Old(1)));

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.

procedure Bad_Find_Next (S : String; I : Positive; J : out Positive) with
     Pre  => I in S'Range and then
             (for some K in S'Range => (if K > I then S(K) = S(I))),
     Post => (for all K in I+1 .. J-1 => S(J) /= S(I));

Found the problems? GNATprove did and it signals them with warnings. For the existential quantification in the precondition, it issues: warning: suspicious expression warning: did you mean (for all X => (if P then Q)) warning: or (for some X => P and then Q) instead?

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: warning: unused variable "K"

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.

Posted in #Formal Verification    #Compilation    #SPARK   

About Yannick Moy

Yannick Moy

Yannick Moy is Head of the Static Analysis Unit at AdaCore. Yannick contributes to the development of SPARK, a software source code analyzer aiming at verifying safety/security properties of programs. He frequently talks about SPARK in articles, conferences, classes and blogs (in particular Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.