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

[Colin Paul Gloster <Colin_Paul_Gloster@ACM.org>]

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