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=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,43216c2d2bcda533,start
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!news2.google.com!npeer02.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!nntp.club.cc.cmu.edu!feeder.erje.net!feeder.news-service.com!npeer.de.kpn-eurorings.net!npeer-ng0.de.kpn-eurorings.net!newsfeed.arcor.de!newsspool2.arcor-online.net!news.arcor.de.POSTED!not-for-mail
Date: Thu, 04 Feb 2010 12:26:11 +0100
From: Georg Bauhaus <rm.dash-bauhaus@futureapps.de>
User-Agent: Thunderbird 2.0.0.23 (Macintosh/20090812)
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Specifying the order of ops on an ADT with aspects
Content-Type: text/plain; charset=ISO-8859-15
Content-Transfer-Encoding: 7bit
Message-ID: <4b6aaed4$0$7625$9b4e6d93@newsspool1.arcor-online.net>
Organization: Arcor
NNTP-Posting-Date: 04 Feb 2010 12:26:12 CET
NNTP-Posting-Host: 8464ac55.newsspool1.arcor-online.net
X-Trace: 
 DXC=0M5__bNST49^8FBo0_81f>ic==]BZ:af>4Fo<]lROoR1<`=YMgDjhg2@:>SDEfdW76nc\616M64>:Lh>_cHTX3j=VEFc^>@X7B0
X-Complaints-To: usenet-abuse@arcor.de
Xref: g2news1.google.com comp.lang.ada:8884
Date: 2010-02-04T12:26:12+01:00
List-Id: <comp.lang.ada>

Defining a private type, I'd like to know whether
it is possible to specify, with the help of the new
aspects, possible orders of calling the operations.
Showing my ignorance, to which extent might it be
possible to analyse the order of calls at compile time?

(AI05-0145-{1,2}, AI05-0183)

generic
   type P is private;
package Order is


   pragma Pure (Order);
   -- ascertain that Pre functions do not have side effects




   type States is (S0, S1, S2, S3);

   type T is tagged private;

   function State_Of (Object : in T) return States;


   procedure Op1 (Object : in out T; Param : in P)
     with
       Pre => State_Of (Object) = S0;

   procedure Op2 (Object : in out T; Param : in P)
     with
       Pre => State_Of (Object) = S1 and Knoptuous (Object);

   procedure Op3 (Object : in out T; Param : in P)
     with
       Pre => State_Of (Object) in S1 .. S2;


   function Knoptuous (Object : in T) return Boolean;

private
   type T is tagged
      record
         State_Of : States := S0;
      end record;

end Order;