Specifying the order of ops on an ADT with aspects

Specifying the order of ops on an ADT with aspects

[Georg Bauhaus]

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;

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

[Hibou57 (Yannick Duchêne)]

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.

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

[Colin Paul Gloster]

[-- Attachment #1: Type: TEXT/PLAIN, Size: 1797 bytes --]

On Thu, 4 Feb 2010, Hibou57 (Yannick Duchêne) sent:

|------------------------------------------------------------------------|
|"[..]                                                                   |
|                                                                        |
|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, [..]                                |
|[..]"                                                                   |
|------------------------------------------------------------------------|

I agree that no message for a failing precondition or postcondition
check is bad. A newer Ada standard does not necessitate a better
language.

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

[Hibou57 (Yannick Duchêne)]

On 5 fév, 17:44, Colin Paul Gloster <Colin_Paul_Glos...@ACM.org>
wrote:
> I agree that no message for a failing precondition or postcondition
> check is bad. A newer Ada standard does not necessitate a better
> language.
Don't be sad, pretty sure most of vendors will provide it ;)
After all, the Ada standard does not specify anything either about
debugging informations and the like, and indeed, that's not its area.
This may be the reason why of the actual ARG vote.

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

[Dmitry A. Kazakov]

On Fri, 5 Feb 2010 08:55:31 -0800 (PST), Hibou57 (Yannick Duch�ne) wrote:

> On 5 f�v, 17:44, Colin Paul Gloster <Colin_Paul_Glos...@ACM.org>
> wrote:
>> I agree that no message for a failing precondition or postcondition
>> check is bad. A newer Ada standard does not necessitate a better
>> language.
> Don't be sad, pretty sure most of vendors will provide it ;)
> After all, the Ada standard does not specify anything either about
> debugging informations and the like, and indeed, that's not its area.
> This may be the reason why of the actual ARG vote.

Whatever, but I see no need in yet another syntax for run-time assertions.
Statically checked contracts in the form of pre- and postconditions would
be a great language improvement, what we will get obviously to me will not.

And my painful experience tells me that no check is optional. There is
either one or none. I bet that any suppressed check will eventually fail in
the production code [*].

------------------
* Unless you do things like code coverage etc, but these would eliminate
the very need to check something that you already proved to hold.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Randy Brukardt]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 1957 bytes --]

"Hibou57 (Yannick Duch�ne)" <yannick_duchene@yahoo.fr> wrote in message 
news:91ab6070-fc9e-4575-a967-8fe43353ba26@36g2000yqu.googlegroups.com...
>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 think you guys miss the point of that statement. A Precondition that fails 
raises Assert_Error (unless suppressed, of course). That gets handled in the 
normal way, whatever your implementation does for unhandled exceptions. 
Nothing new here.

But the original proposal included an optional message string, similar to 
the one the Assert pragma has. We decided to drop that because programs that 
fail Preconditions are just wrong, and there is no need to go into detail 
*why* they're wrong.

I'd expect Janus/Ada to report something like:

** Unhandled Assert_Error - precondition check failed

In any case, Ada has nothing to say about how unhandled exceptions are 
reported.

We're working hard on a proposal to give the compiler enough information to 
be able to do static analysis of preconditions/postconditions, etc. We won't 
mandate that this time, but we surely want the possibility to exist --  
otherwise there is little value to specifying these over plain old Assert 
pragmas. (Perhaps next time we'll be able to mandate some static checking.)

                                  Randy.

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

[Hibou57 (Yannick Duchêne)]

On 5 fév, 23:15, "Randy Brukardt" <ra...@rrsoftware.com> wrote:
> I think you guys miss the point of that statement. A Precondition that fails
> raises Assert_Error (unless suppressed, of course).
OK

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

[Hibou57 (Yannick Duchêne)]

Side comment.

There is another good side effect of pre-post-conditions, apart their
abilities to better express contracts and to check usages and
implementations conformance : as you define pre-post-conditions, you
see what's needed to define these, so it enforce completeness of ADTs.
With this kind of design, one is less likely to miss a required
function to test an instance of an ADT. Last and although indirectly,
these functions, in turn sometimes makes the need of some associated
procedures more clear.

This is an aid in setting up specifications.

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

[Colin Paul Gloster]

On Fri, 5 Feb 2010, Dmitry A. Kazakov sent:

|---------------------------------------------------------------------------|
|"[..]                                                                      |
|                                                                           |
|And my painful experience tells me that no check is optional. There is     |
|either one or none. I bet that any suppressed check will eventually fail in|
|the production code [*].                                                   |
|                                                                           |
|------------------                                                         |
|* Unless you do things like code coverage etc, but these would eliminate   |
|the very need to check something that you already proved to hold."         |
|---------------------------------------------------------------------------|

J. Fleuriot (
WWW.inf.Ed.ac.UK/people/staff/Jacques_Fleuriot.html
) asserted on January 24th, 2008:
"[..] there's no such thing as one hundred per cent guarantees [..]"