Re: Require / ensure clauses

[Georg Bauhaus <rm.tsoh.plus-bug.bauhaus@maps.futureapps.de>]

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.