Preconditions and postconditions define a very strong mechanism for specifying invariant properties over the program's control. What about similar properties for the program's data? It turns out Ada 2012 defined such a construct, type predicates, which was not supported in SPARK until now. And now it is.

With type predicates, one can express all the invariant properties of data that could not be expressed with type ranges, non-nullness constraints, discriminants, etc. For example, are you doing cryptography and you want to define a type for prime numbers? You can with type predicates:

The predicate above reads: "for all values of divisor between 2 and half the value of a prime number, the divisor does not divide the prime number". Which is indeed a possible definition of prime numbers.

Closer to a problem reported recently by a customer, are you building control software for a chip that does not support subnormal floating-point numbers, and you want to define a type for normal floating-point numbers only? You can with type predicates:

Whether you're doing cryptography or control software, in both cases you'll get an error at run time if you try to assign a value that does not respect the predicate into a variable of that type. With GNATprove, you can additionally prove that such run-time errors can never occur in your programs, hence that the predicates are always respected by the data.

Interestingly, predicate checks are the first kind of run-time checks for which SPARK rules mandate more verifications than the Ada rules. Indeed, Ada rules are on purpose not bulletproof. It would be hard in Ada, because any Boolean expression is allowed as predicate, so we can write:

But then, if I assign value 0 in Global_Var somewhere in the code, I'm suddenly violating the predicates of all values of type My_Type. I could even hide the predicate behind function calls to further complicate the matter. Hence, when they created predicates in Ada, the ARG committee chose to request that only some run-time checks are performed to verify that predicates are respected, without trying to detect all possible violations.

In SPARK, we took the opposite path, restricting expressions that can be used as predicates so that we can perform bulletproof formal verification that no violation can occur. In the SPARK Reference Manual, the restriction is expressed quite succinctly: "A Dynamic_Predicate expression shall not have a variable input." In particular, this means that the predicate of My_Type above is not allowed in SPARK.

Even with this restriction, the Ada rules are not sufficient to make sure a predicate is never violated. In particular, Ada does not require that the predicate is checked after assignment to a record component. For example, assume you have a type for pairs of distinct integer values:

Ada rules do not disallow the following code (although it violates the spirit of using type predicates) which temporarily violates the predicate above:

In SPARK, we have defined a verification rule that forces the predicate to hold when assigning to component Val2 above. Thus, GNATprove detects the possible violation in this code. Note that this is only a verification rule, which does not change how GNAT compiles this code.

For simplicity, I used the GNAT-specific aspect Predicate in the examples above. In fact, Ada defines two different aspects Static_Predicate and Dynamic_Predicate. See the references below for an explanation of their differences.

To know more about predicates in Ada, see the Ada Reference Manual and John Barnes's excellent rationale on the subject (section 5 on Subtype predicates).

To know more about predicates in SPARK, see the SPARK User's Guide.