Specifying the order of ops on an ADT with aspects

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

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;