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

[nospam@thanks.com.au (Don Harrison)]

Matt Heaney wrote:

: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."

I mean having to duplicate the information in the operation declaration and 
its body just as you have to do for its signature.

: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.

Same here.

: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 would say you *do* need to if you have to duplicate the signature (as you do).

:>: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;

Okay, so you mean visibility to the attributes of the type.

Yes, it's true that access to just the attributes of a type is sufficient 
to declare an invariant. However, more flexible is the ability to also use
functions which encapsulate an aspect of that state. Such functions are 
generally declared in the same modules that directly *update* an object of 
that type. In Ada, that means, potentially, a collection of modules, 
specifically:

1) For tagged private types, the body or a child package body.
2) Additionally, for tagged (non-private) type, any client package body!

Hence, there is no single module responsible for updating the object. Further, 
there is no single module that has access both to the attributes of an object 
*plus* all the functions used to describe its state. Consequently, it's 
impossible to add an invariant mechanism to Ada which allows you to describe 
the state of an object using all the resources you may want to use. 

This problem doesn't arise in Eiffel because there is only one such module - 
the class that defines the type - which can update the object directly and 
hence contains the functions which describe its state. So, an Eiffel class 
invariant can include everything you may want to use.

:>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.

I agree you could restrict invariants to use only *attributes* of a type
but this denies you the choice of also using abstraction to describe state,
so forcing you to duplicate code.


: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:

[Matt's example]

: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.

Yes, it's true they aren't necessary, though they are *helpful*. For example, 
if the condition defined by your invariant was useful elsewhere, you could
encapsulate it in a function and reuse it:

  function Internally_Consistent (Queue: Unbounded_Queue) return Boolean is
  begin
    ...     -- return a boolean reflecting Matt's invariant
  end;

  ...

  type Unbounded_Queue is
     tagged record
     ...
  invariant
    Internally_Consistent (Current);
  end record;

Somewhere:

  if Internally_Consistent (Q) then ..


:>postcondition
:>   Shorter: Length (Sequence) < Length (Sequence'Old)
:>end;
:
:I like this idea.

Thanks.


:>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? 

Grrrr! Now you know how I feel about the unneccessary editing inflicted on me
by maintaining redundant code in Ada! :)
 

:Thank you!

No problem! :)


Don.
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
Don Harrison          donh at syd.csa.com.au
                      ^^^^^^^^^^^^^^^^^^^^^^
Hopefully, this is an improvement and foils some spammers.