Can you cheat contracts / asserts in SPARK?

Question

Suppose I have a subprogram written using the SPARK Ada subset with postconditions verifying some property - for example, that the returned array is sorted, whose body just calls out to a function external to SPARK - for example, a C/C++ function that sorts arrays. Is there any way to force SPARK to assume, after this call, that the array will be sorted?

Answer 1

In short, GNATprove takes a divide-and-conquer approach when analyzing code. The following explanation is incomplete and in practice things are slightly more complicated, but for the sake of understanding, it gives a useful perspective on how things work.

For each assertion, loop invariant and pre-/post-condition GNATprove creates verification conditions (VCs) that must be proven. Verification conditions are to be proven by assumptions and the semantics of the code.

1. When a code section is being analyzed, and this code section starts just after a call to a subprogram, then any post-condition of that subprogram is assumed to hold.

2. If that particular subprogram is implemented in SPARK, then GNATprove will try to proof that the post-conditions indeed hold by analyzing the subprogram. However, if the particular subprogram is not in SPARK (e.g., the subprogram is imported), then the post-conditions will remain assumptions and it is left to the developer to prove them by other means.

A nice example that illustrates the first point can be found in sections 1 and 2 of the recently published article The Work of Proof in SPARK (available here). Note in particular how a repeated call to the Increment function is being analyzed by GNATprove.

So, if you want SPARK to assume particular post-conditions to hold for a subprogram that is not in SPARK (an imported function, for example), just provide the post-conditions.