Gem #31: Preconditions/postconditions

by Robert Dewar —AdaCore

Let's get started…

The notion of preconditions and postconditions is an old one. A precondition is a condition that must be true before a section of code is executed, and a postcondition is a condition that must be true after the section of code is executed.

In the context we are talking about here, the section of code will always be a subprogram. Preconditions are conditions that must be guaranteed by the caller before the call, and postconditions are results guaranteed by the subprogram code itself.

It is possible, using pragma Assert (as defined in Ada 2005, and as implemented in all versions of GNAT), to approximate run-time checks corresponding to preconditions and postconditions by placing assertion pragmas in the body of the subprogram, but there are several problems with that approach:

1. The assertions are not visible in the spec, and preconditions and postconditions are logically a part of (in fact, an important part of) the spec.

2. Postconditions have to be repeated at every exit point.

3. Postconditions often refer to the original value of a parameter on entry or the result of a function, and there is no easy way to do that in an assertion.

The latest versions of GNAT implement two pragmas, Precondition and Postcondition, that deal with all three problems in a convenient way. The easiest way to describe these is to use an example:

    package Arith is
       function Sqrt (Arg : Integer) return Integer;
       pragma Precondition (Arg >= 0);
       pragma Postcondition
        (Sqrt'Result >= 0
           and then
        (Sqrt'Result ** 2) <= Arg
           and then
        (Sqrt'Result + 1) ** 2 > Arg);
    end Arith;

    with Arith; use Arith;
    with Text_IO; use Text_IO;
    procedure Main is
    begin
       Put_Line (Sqrt (9)'Img);
       Put_Line (Sqrt (10)'Img);
       Put_Line (Sqrt (-3)'Img);
    end;

Now if we compile with -gnata (which enables preconditions and postconditions), and we have a correct body for Sqrt, then when we run Main we will get:

     3
     3

    raised SYSTEM.ASSERTIONS.ASSERT_FAILURE :
       Precondition failed at arith.ads:3

Now if there was something wrong with the body of Sqrt that gave the wrong answer, we might get:

    raised SYSTEM.ASSERTIONS.ASSERT_FAILURE :
      postcondition failed at arith.ads:4

Indicating that we have a bug in the body of Sqrt that we must investigate.

There is one more thing to mention, which is the promised ability to refer to the old value of parameters. A new attribute 'Old allows this as shown in this example:

    procedure Write_Data (Total_Writes : in out Natural);
    --  Write out the data incrementing Total_Writes to
    --  show number of write operations performed.
    pragma Postcondition (Total_Writes > Total_Writes'Old);

The introduction of preconditions and postconditions into GNAT provides a powerful tool for design and documentation (Eiffel has referred to this approach as "design by contract").

The preconditions and postconditions serve three functions
1. They provide valuable formal documentation in the spec
2. They provide input to proof tools
3. They help find bugs in the course of normal debugging as shown by the example above.

Support for preconditions and postconditions will be available in GNAT Pro 6.2.1 and forthcoming versions of GNAT GPL. If you are a GNAT Pro user and you want to try this feature out today, request a wavefront by using GNAT Tracker.

About the Author