Re: Precondition Checking For Ada 0X (Was: Separation of IF and Imp: process issue?)

[mheaney@ni.net (Matthew Heaney)]

In article <EGLBMK.A5I@syd.csa.com.au>, nospam@thanks.com.au wrote:


>One issue to consider is whether to include preconditions and postconditions
>in separate operation declarations - doing so would only worsen the 
>redundancy problem but not doing so creates an inconsistency similar to Pascal
>"forward" declarations. :(
>
Yes, I would include preconditions and postconditions in separate operation
declarations.  But I'm not sure what you mean by a "redundancy problem."

o If you mean the overloaded subprograms each have to list potentially
identical pre and post-conditions, then I don't have any problem with that.

o If you mean list pre and postconditions again in the package body, I
would say you don't need to bother (but there may be issues about that that
I haven't considered).

>:I still have to think about how to state a representation invariant.  Its
>:specification would somehow have to be attached to the full view of the
>:type, and would be evaluated at exit from a subprogram.
>
>What is meant by "the full view of the type"? Do you mean including the 
>operations in the package body? - this would be close to the Eiffel concept.

The full view of a type is the type declaration that appears after the word
"private" in the spec, ie:

generic
   type Stack_Item;
   Max_Depth : Positive;
package Stacks_G is

   -- This is the "partial" view:
   type Bounded_Stack is tagged private;
...
private

   type Stack_Item_Array is 
      array (Positive range 1 .. Max_Depth) of Stack_Item;

   -- This is the "full" view:
   type Bounded_Stack is 
      tagged record
          Items : Stack_Item_Array;
          Depth : Natural := 0;
       end record;

end;

>Unless I'm mistaken, you're faced with a dilemma in trying to implement
>invariants:
>
>1) On the one hand, you want to allow invariants to include all of the 
>   type's operations declared in a package - exported and hidden, primitive 
>   and class-wide - it implies declaring them in the package body somehow. 
>   While such invariants could use the "full" view of the type, they 
>   wouldn't be visible to public child packages. This would make it 
>   impossible to extend an invariant in a descendant type in a public child.

Actually, I hadn't considered using operations in the invariant.  What I
had in mind is a relationship among the variables that are the
representation of an object.  As these variables are part of the
implementation, my thinking was that no public operations would apply.

For example, I have a queue implemented as a linked list, with a pointer to
the front of the list, and a pointer to the back.  I would like to state as
a representation invariant that the previous pointer of the front node is
null, and the next pointer of the back node is also null:

generic
   type Queue_Item is private;
package Queues_G is

   type Unbounded_Queue is tagged private;
...
private

   package Queue_Item_Lists is 
      new Lists_G (Queue_Item);
    use Queue_Item_Lists;

   type Unbounded_Queue is
      tagged record
         Front, Back : Unbounded_List;
         Length : Natural := 0;
      invariant
         Front_OK : Length /= 0 implies Front.Previous = null;
         Back_OK : Length /= 0 implies Back.Next = null;
         Length = 0 implies Front = null and Back = null;
         Length = 1 implies Front = Back;
         Length > 1 implies Front /= Back;
      end record;

        
So I'm not clear that operations are even needed to implement an invariant,
if one accepts the model that invariants are simply boolean expressions
comprising only record components.


>:I also haven't thought of a convenient way to state a postcondition in
>:terms of a change in a value (ie the length before the call versus the
>:length after the call).
>
>Do you mean like the following?..
>
>procedure Remove_Item
>  (Sequence : in out Root_Sequence; 
>   Index    : in     Positive)
>precondition
>   Is_Present: Index <= Length (Sequence);
>postcondition
>   Shorter: Length (Sequence) < Length (Sequence'Old)
>end;

I like this idea.


>Don.                     (Reverse to reply)
>=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
>Don Harrison             au.com.csa.syd@donh

Can you fix this so I don't have to do some much damn editing reply to you? 
How about

   donh*syd.csa.com.au
   syd.csa.com.au@donh

Thank you!

--------------------------------------------------------------------
Matthew Heaney
Software Development Consultant
<mailto:matthew_heaney@acm.org>
(818) 985-1271