Re: Specifying the order of ops on an ADT with aspects

["Hibou57 (Yannick Duchêne)" <yannick_duchene@yahoo.fr>]

On 4 fév, 12:26, Georg Bauhaus <rm.dash-bauh...@futureapps.de> wrote:
> 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?

Your package example looks good to me, except the assumption you've
made about “ analyse the order of calls at compile time ”

The new pre-post-condition which will comes for 2015 (I suppose), is
not intended to be checked at compile time nor even at runtime. I
gonna miss this last one (the first one would be a heavy pain to
implement), but I suppose some compiler vendors will probably have an
option for that and will go the Eiffel way with this contract
clauses : enable or disable clauses-check, just like you can enable or
disable generation of debugging information with any compiler.

AI05-0145-2 says
http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai05s/ai05-0145-2.txt?rev=1.4
> This is based on the previous alternative AI05-0145-1. The
> Pre/Post aspects are specified using the aspect_specification
> syntax defined in AI05-0183-1. There is no message associated
> with the failure of a precondition or postcondition check: it
> was deemed that these annotations are intended for verification,
> and that for debugging purposes the Assert pragma is sufficient.
The last sentence is the most important for you topic.

All providing I've really understood your question

“ intended for verification, and that for debugging purposes the
Assert pragma is sufficient ”

I was exactly feeling the opposite, that Assert pragmas are not
sufficient and are hard to maintain and copy in implementations
accordingly to contracts in specifications.