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
       Put_Line (Sqrt (9)'Img);
       Put_Line (Sqrt (10)'Img);
       Put_Line (Sqrt (-3)'Img);

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:


       Precondition failed at

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

      postcondition failed at

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

Dr. Robert Dewar is co-founder, President and CEO of AdaCore and Emeritus Professor of Computer Science at New York University. With a focus on programming language design and implementation, Dr. Dewar has been a major contributor to Ada throughout its evolution and is a principal architect of AdaCore’s GNAT Ada technology. He has co-authored compilers for SPITBOL (SNOBOL), Realia COBOL for the PC (now marketed by Computer Associates), and Alsys Ada, and has also written several real-time operating systems, for Honeywell Inc. Dr. Dewar has delivered papers and presentations on programming language issues and safety certification and, as an expert on computers and the law, he is frequently invited to conferences to speak on Open Source software, licensing issues, and related topics.