Gem #149 : Asserting the truth, but (possibly) not the whole truth
by Yannick Moy —AdaCore
Let's get started...
In the beginning was created Ada. It did not have any assertions. Then came GNAT, which introduced pragma Assert. The ARG saw that it was good, and adopted it in Ada 2005. Then came GNAT again, which introduced pragma Precondition and pragma Postcondition. The ARG saw that they were good too, and adopted them as aspects in Ada 2012. The ARG even tried to beat GNAT at this game, and introduced at the same time aspects for type predicates (see Gems #146 and #147) and type invariants (see Gem #148), which are other forms of assertions. Then came GNAT again, introducing pragmas Assume, Assert_And_Cut, and Loop_Invariant, and aspect Contract_Cases, yet other forms of assertions.
So now the Ada programmer has a rich set of assertions to state control-relevant properties (Assert, Pre, Post, Loop_Invariant, Assume, Assert_And_Cut) and data-relevant properties (Static_Predicate, Dynamic_Predicate, Type_Invariant).
How does one state which assertions get executed? And how does one differentiate between different executables, say, between one created for debugging/testing, and one created for production?
GNAT provides a switch -gnata that enables all assertions: pragma Assert of course, but also all the newer forms of assertions presented above. So each unit can be independently compiled with or without assertions. But that's not always adequate.
Let's take the example of writing a library. We want to use preconditions to prevent the library from being called in an invalid context (defensive programming), and postconditions plus type predicates to help with debugging and maintenance of the library (assertion-based verification). Here is the code:
package Library is type Status is (None, Acquired, Released); type Resource is record Id : Integer; Stat : Status; end record with Dynamic_Predicate => (if Resource.Id = 0 then Resource.Stat = None else Resource.Stat /= None); No_Resource : constant Resource := Resource'(0, None); procedure Get (R : in out Resource; Id : Integer) with Pre => R.Stat = None, Post => R.Stat = Acquired; procedure Free (R : in out Resource) with Post => (if R.Stat'Old = Acquired then R.Stat = Released); end Library;
package body Library is procedure Get (R : in out Resource; Id : Integer) is begin R.Stat := Acquired; R.Id := Id; end Get; procedure Free (R : in out Resource) is begin if R.Stat /= Acquired then return; end if; R.Stat := Released; end Free; end Library;
When this code is compiled with the switch -gnata, each call to Get incurs four run-time assertions (and calls to Free have three):
- a precondition check on subprogram entry
- a postcondition check on subprogram exit
- a predicate check for parameter R on subprogram entry
- a predicate check for parameter R on subprogram exit
That's fine during testing and debugging (when we use -gnata), but we'd like the production code to only contain run-time assertions for the preconditions, to catch misuse of the library in the actual product, while avoiding the overhead of the other checks.
Ada 2012 provides pragma Assertion_Policy for that purpose. This pragma can take the name of an assertion aspect/pragma as first argument, and the desired policy for that aspect as second argument. To enforce checking of preconditions even when -gnata is not used, one only has to include the following line at the start of library.ads:
pragma Assertion_Policy (Pre => Check);
Now, any misuse of the library by client code will be detected, no matter how the library is compiled. Take for example a program that fails to release the resource between two calls to Get:
with Library; use Library; procedure Client is R : Resource := No_Resource; begin Get (R, 1); Get (R, 2); -- incorrect end Client;
This code (and the library code) can now be compiled without -gnata:
$ gnatmake client.adb gcc -c client.adb gcc -c library.adb gnatbind -x client.ali gnatlink client.ali
And it still raises an error at run time:
$ ./client raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from library.ads:16
For more information on pragma Assertion_Policy, or the new assertion pragmas/aspects supported by GNAT, see the GNAT Pro Reference Manual.
And as Tony Hoare puts it: "Assert early and assert often!"
About the AuthorYannick Moy’s work focuses on software source code analysis, mostly to detect bugs or verify safety/security properties. Yannick previously worked for PolySpace (now The MathWorks) where he started the project C++ Verifier. He then joined INRIA Research Labs/Orange Labs in France to carry out a PhD on automatic modular static safety checking for C programs. Yannick joined AdaCore in 2009, after a short internship at Microsoft Research.
Yannick holds an engineering degree from the Ecole Polytechnique, an MSc from Stanford University and a PhD from Université Paris-Sud. He is a Siebel Scholar.