SPARK 2014 Rationale: Specification Functions

by Yannick Moy – Jul 15, 2013

Specifying a program's behavior is seldom expressible in a satisfiable way without the capability of abstraction provided by function calls. Consider a Reset procedure which sets a valid initial state for a variable X of type T. Rather than stating in the postcondition the individual constraints satisfied by every component of X, it is much better to abstract these details away under calls to functions Is_Valid and Is_Initial:

procedure Reset (X : in out T) with
    Post => Is_Valid (X) and then Is_Initial (X);

If Reset is part of the public API of private type T, this is the only way to define a contract for Reset, as the details of implementation of T are not visible.

The specification functions like Is_Valid and Is_Initial that are called in contracts and other annotations (assertions, loop invariants, etc.) must obey specific constraints:

They must not perform side-effects, like writing to a global variable, which could change the behavior of the program depending on whether annotations are executed or not.
They must always terminate, so that the contract in which they appear can be logically interpreted.

Both come easily when specifications are not executable, like in SPARK 2005 or the ACSL specification language for C: a logic function cannot have side-effects, and it is defined to always compute a result.

This is not so easy when specifications are executable, and specification functions are the same functions as the ones called in code. For example, the programming language Eiffel recommends that functions used in annotations are free from side-effects, but does not provide means to enforce it. The specification language JML for Java goes further by requiring that specification functions are declared pure, which indicates that they are free from side-effects and they terminate. So Is_Valid could be declared in JML as follows:

/*@ pure @*/ boolean isValid(T x);

JML tools check that a pure method only calls other pure methods, which guarantees that a pure method does not have side-effects, but termination is not checked. In other words, a non-terminating implementation of isValid could invalidate all proof results:

/*@ pure @*/ boolean isValid(T x) {
     return not isValid(x);  /* does not terminate */
  }

The Spec# specification language for C# has borrowed from JML the notion of purity for the absence of side-effects, that can be both declared by the programmer or inferred by the Spec# verifier:

[pure] public bool IsValid(T x) {
     return not IsValid(x);  // does not terminate
  }

Spec# does not consider termination at all though, so the same non-terminating implementation of IsValid as above could invalidate all proof results.

So how does SPARK 2014 compares to all that? For one thing, all functions in SPARK 2014 are free from side-effects, like in previous versions of SPARK. It is as simple as that. If you want a subprogram that modifies a parameter or a global variable, you should define it as a procedure instead of a function:

procedure Is_Valid_Log_Result (X : T; Result : out Boolean);

A procedure cannot be called in an expression in Ada, hence cannot appear in an annotation. But Ada allows functions that have side-effects, so the formal verification tool GNATprove checks specifically that SPARK 2014 functions cannot have side-effects. Take for example the following implementation of Is_Valid:

function Is_Valid (X : T) return Boolean is
     Result : Boolean;
  begin
     ...             --  compute result here
     Log := Result;  --  store result in global variable
     return Result;
  end Is_Valid;

GNATprove issues the following error on this code:

p.ads:5:13: function with side-effects is not in SPARK

GNATprove does not attempt to prove termination. So, like in Eiffel, JML and Spec#, a non-terminating implementation of Is_Valid could theoretically invalidate all proof results:

function Is_Valid (X : T) return Boolean is (not Is_Valid (X));

In practice, GNATprove uses two mechanisms to limit the extent to which an incorrect specification function invalidates proof results:

Non-termination caused by other reasons than recursion (for example, a loop that does not terminate, or raising an exception) do not invalidate proof results. This is obtained by only generating axioms in the proof system for expression functions (like Is_Valid above) whose definition is given by a single expression, not for other more complex functions.
Only results for subprograms that use directly or indirectly the incorrect specification function can be invalidated. This is obtained by restricting visibility in the proof system to axioms of entities used directly or indirectly in the component being proved.

To completely avoid issues with incorrect specification functions, users can either check manually that specification functions are not recursive, or adopt a general coding standard that forbids recursion completely (like the Recursive_Subprogram rule checked automatically by the coding standard tool GNATcheck).

What we have achieved with these two mechanisms is that GNATprove does not generate global incorrect axioms in the proof system for subtly wrong specification functions. Take for example the following function that returns a number between 0 and its parameter Max:

function Pseudo_Random_Value (G : Generator; Max : Natural) return Natural with
    Post => Pseudo_Random_Value'Result >= 0 and then Pseudo_Random_Value'Result < Max;

If we generated an axiom for such a function, it would be something like (in the syntax of the Why intermediate language)

function pseudo_random_value (g:generator, max:natural): natural

  axiom pseudo_random_value_def:
    forall g:generator. forall max:natural.
      pseudo_random_generator g max >= 0 /\ pseudo_random_generator g max < max

Can you spot the problem? If not, take the value 0 for max, and you get

pseudo_random_generator g 0 >= 0 /\ pseudo_random_generator g 0 < 0

so the value pseudo_random_generator g 0 is both non-negative and negative, which is a contradiction. If an automatic prover manages to discover such a contradiction, it can then prove anything, even on code that does not use Pseudo_Random_Value. The problem in the original contract for Pseudo_Random_Generator is that it cannot always return a value between 0 (included) and Max (excluded) if Max is of type Natural. So either Max should be of type Positive, or the postcondition should allow returning a value between 0 included and Max included.

GNATprove avoids these problems by not generating such wrong axioms. Instead, callers of the function Pseudo_Random_Generator will get access in their context to the postcondition of the function.

Posted in #Formal Verification #SPARK

About 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 blog.adacore.com). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.