|
Gem #31: preconditions/postconditions
Author: Robert Dewar, AdaCore
Abstract: Ada Gem #31 — 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.
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.
 682b |
Posted
in Development Log, Ada / Ada 2005, Devt log - Gem of the Week
Have your own idea for a Gem?
If you have an idea for a Gem you would like to contribute please feel free to contact us at: gems@adacore.com
Jeff Creem said:
Nice and interesting timing. I was just re-reading some of the old AIs in this area and thinking that I wish this had been implemented in Ada 2005.
One concern that had been expressed with the AIs was that in Ada we typically want static compile time checking and this only was seen as a dynamic check but hopefully tools like Polyspace and other static tools can begin to use this information. Even short of that, I like the idea of being able to use this to help document expectations.
Cyrille Comar said:
Thanks for your nice comment Jeff. The issue of static vs dynamic pre/post conditions is indeed very interesting. Static analysis tools exploiting the information provided by the dynamic versions are already on their way… More on this later ;-)
The static versions have been provided by tools such as Spark from Praxis for a while already.
Finding a way to marry the static & the dynamic versions is an interesting challenge that we are considering seriously!