Require / ensure clauses

Require / ensure clauses

[Hibou57 (Yannick Duchêne)]

Hello dear all of you,

A simple question which live into my mind for sometimes (let say a bit
long) is about the require and ensure clauses of the Eiffel lanuage.
For people who do not known, let say that these are predicate which
assert property on a language or function execution (and returned
result for a function). Well, to be honest, Eiffel also knows things
like invariant (for classes) and variant (for loops), but let keep it
simple (the question) and just talk about require/ensure, .. no more.

So... what about require / ensure clauses in the Ada world ?

How does Ada developpers feel about it ? Does any one of you miss it ?
How do you do ? Use comments whith similar meanings ? Others ?

... here we are... let's simply talk about design by contract with
Ada :)

Re: Require / ensure clauses

[Hibou57 (Yannick Duchêne)]

Sorry... a mistake one may not read “ are predicate which assert
property on a language or function ” but rather “ are predicates which
assert properties on a procedure or function ” instead

I apology

Re: Require / ensure clauses

[Georg Bauhaus]

Hibou57 (Yannick Duch�ne) wrote:

> ... here we are... let's simply talk about design by contract with
> Ada :)

Ada DbC seems to be work in progress, to be integrated possibly
with Ada type constraints (yielding type based invariants in
addition to pre/post for subprograms). At this time GNAT GPL
offers a semi-solution for subprograms (excluding inheritance AFAICT).
Use pragmas Precondition and Postcondition, specified next to the
preceding subprogram declaration. Use pragma Assert for Eiffel's
"check" instruction.
Exception handlers can be made to act like Eiffel's "rescue"
clauses.

I'd speculate that adding constraints for types and operations
is not an easy job because Ada is not as simple a language as
Eiffel sometimes appears to be. At least as regards integration
of Ada with DbC or with that other one, requires/modifies/ensures
etc.

If the SPARK subset of Ada is not a heavy restriction,
it offers Eiffel DbC and more, at program analysis (compile) time.
I think it was advertised it as Eiffel on Steroids once.