Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

On 22.06.12 09:23, Dmitry A. Kazakov wrote:
> Neither #1 nor #2 is defendable.

Maybe dynamic checking is not defendable when the attack is
based on some biased, and, frankly, narrow set of assumptions.
Which is probably OK in some narrow field.

But from a workshop point of view, I'd throw in that
Pre/Post gives us vastly better error messages, as follows.

A clause of the contract, involving exceptions, looks
like this:

If you, client, do not obey the constract *Pre*, then I,
supplier, may fail to produce in accord with the contract
*Post*. I will throw something at you.

Exceptions will happen in any case. The Pre/Post aspects
show that this is the case.

However, exceptions will point to somewhere *inside* the
supplier's package if Pre/Post checking is off, or Pre = True.
Whereas, if Pre/Post checking is on as intended, exceptions
can pinpoint a *contract* violation by the client.

This behavior requires that pre/post conditions are properly
reflected in the supplier's implementation.

(I have indicated alternative possibilities (just on Pop),
as the specific contract of this example is probably one
among a number of choices. For the sake of simplicity, this
is a single stack package; the contractual behavior shouldn't
change much with a stack type declared instead.)

Compare

raised SYSTEM.ASSERTIONS.ASSERT_FAILURE :
  failed precondition from stk.ada:20 instantiated at stk.ada:79

vs

raised CONSTRAINT_ERROR :
  stk.ada:60 range check failed


Note that the first message mentions a specific precondition
from the spec.  The second message points to the body. This
body may not be available for inspection! That is, if you want
to spend time finding your own error by understanding
the supplier's implementation first!


generic package Stk is

   pragma Elaborate_Body (Stk);

   Capacity : constant := 10;   -- or use a constrained subtype

   type T is interface;
   type Stackable is access constant T'Class;


   function Length return Natural;
   --  Number of items currently on the stack.

   procedure Push (Item : Stackable)
     with   Pre  => Length < Capacity,
            Post => Top = Item and Length = Length'Old + 1;
   -- Item becomes topmost if there is room

   procedure Pop
     with  Pre  => Length > 0,
           Post => Length = Length'Old - 1;
   -- Drops the topmost item, if any.
   -- [ALTERNATIVELY,
   --     Pre => True,
   --    Post => Length = Natural'Max (0, Length'Old - 1)]

   function Top return Stackable
     with   Pre => Length > 0;
   --  A copy of the topmost item.
   -- [ALTERNATIVELY ...]

end Stk;



package body Stk is

   Ptr : Natural range 0 .. Capacity;
   Data : array (Natural range 1 .. Capacity) of Stackable;

   --
   -- Strategy: there is a 1:1 correspondence between
   -- Ptr being in range and the pre/post conditions
   --

   function Length return Natural is
   begin
      return Ptr;
   end Length;

   procedure Push (Item : Stackable) is
   begin
      -- cannot produce Post if the stack is full, may raise C_E
      Data (Ptr + 1) := Item;
      -- Ptr not increased in case of failure
      Ptr := Ptr + 1;
   end Push;

   procedure Pop is
   begin
      Ptr := Ptr - 1;  -- if Ptr = 0, then C_E
   end Pop;

   function Top return Stackable is
   begin
      -- if Ptr not in 1 .. Capacity, then C_E
      return Data (Ptr);
   end Top;

begin
   Ptr := 0;
end Stk;