From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=0.2 required=5.0 tests=BAYES_00,INVALID_MSGID,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: fac41,2c6139ce13be9980
X-Google-Attributes: gidfac41,public
X-Google-Thread: 103376,3d3f20d31be1c33a
X-Google-Attributes: gid103376,public
From: nospam@thanks.com.au (Don Harrison)
Subject: Re: Precondition Checking For Ada 0X (Was: Separation of IF and Imp:
 process issue?)
Date: 1997/09/16
Message-ID: <EGLBMK.A5I@syd.csa.com.au>#1/1
X-Deja-AN: 272910327
Sender: news@syd.csa.com.au
References: <mheaney-ya023680001009971956580001@news.ni.net>
Reply-To: nospam@thanks.com.au
X-Nntp-Posting-Host: dev50
Organization: CSC Australia, Sydney
Newsgroups: comp.lang.ada,comp.lang.eiffel
Date: 1997-09-16T00:00:00+00:00
List-Id: <comp.lang.ada>


Matt Heaney suggested a way of adding assertions to Ada. Part of the example..
 
:procedure Pop
:  (Stack : in out Root_Stack)
:precondition
:   Not_Empty: not Empty (Stack);
:end Pop;

[..]

:You get the idea.  The subprogram precondition is a list of boolean
:expressions that are functions of one or more of the subprogram arguments. 
:The precondition (and postcondition too - I didn't show that) is part of
:the signiture of the subprogram.

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


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

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.

2) OTOH, if you allow invariants to use only operations declared in the spec, 
   they are visible in public child packages but can't include operations from 
   the body - not as general as Eiffel invariants.

This seems to reveal a weakness of separate interface and implementation 
which doesn't arise in Eiffel's embedded model.

Assuming 2) was adopted, you could have (assuming Matt's declarations):

  private
    type Root_Stack is abstract tagged record
      ...
    invariant
      Full (Current) implies not Empty (Current);
      Empty (Current) implies not Full (Current);
    end record;
  end Pkg; 

(Current = Self = This - take your pick).

Sorry to have to point this out, but "Full" and "Empty" would have to be 
pre-declared - more redundancy. :(


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


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