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 Author