Re: On pragma Precondition etc.

[Martin Krischik <krischik@users.sourceforge.net>]

Alex R. Mosteo schrieb:

> Piling more suggestions: I understand the point of using pragmas by Gnat at
> this stage, but if this is going to be standardized perhaps the syntax of a
> declaration could be changed. For example:
> 
> function Foo (X, Y : Something) return Whatever with
>   Precondition (Blah) and
>   Postcondition (Urgh);

It too think a dedicated syntax would be best. However, I suggest to 
take a good look at task and protected types for guidance.

Protected types already have an precondition. I know they are attached 
to the body and a protected type blocks until the condition becomes true.

But the idea behind is still similar and so should be the syntax. Now 
let me think:

Option 1:

using when - just like protected types.

function Foo (
    Integer X,Y)
entry when
    X > Y
exit when
    Foo  > X + Y
return
    Integer;

Option 2:

using nicer English.

function Foo (
    Integer X,Y)
on entry
    X > Y
on exit
    Foo  > X + Y
return
    Integer;

Both options would not need new keywords ;-)

And how about Invariants (http://en.wikipedia.org/wiki/Class_invariant)?

Martin

-- 
mailto://krischik@users.sourceforge.net
Ada programming at: http://ada.krischik.com