From: Richard D Riehle <laoXhai@ix.netcom.com>
Subject: Re: Assertions
Date: 1999/05/19
Date: 1999-05-19T15:18:51-05:00 [thread overview]
Message-ID: <7hv6bb$1l9@dfw-ixnews6.ix.netcom.com> (raw)
In-Reply-To: 3742eba6@eeyore.callnetuk.com
In article <3742eba6@eeyore.callnetuk.com>,
"Nick Roberts" <nickroberts@callnetuk.com> wrote:
>Richard D Riehle wrote in message <7hqe7m$q7i@sjx-ixn1.ix.netcom.com>...
>[...]
>| pragma Pre_condition (boolean_expression [ ... ]);
>| pragma Post_condition (boolean_expression [ ... ]);
>| pragma Invariant (boolean_expression [ ... ]);
>What would these actually do that Assert would not?
A pre-condition test (Eiffel Require assertion) guarantees
that a subprogram will not be entered unless the assertion is
satisfied. It can, in some environments, be applied at the
class/type level, but is more often at the subprogram level.
An example of this assertion is the "barrier" on a protected
entry. The barrier is a lot like a pre-condition since it also
evaluates a boolean expression before we can begin execution of
the routine. The barrier is not precisely identical to a pre-
condition, but it should give you the general idea.
A post-condition (Eiffel Ensure) guarantees that a certain set
of circumstances will be true before exiting a subprogram. If
the post-condition fails, an exception may be raised.
An invariant is much as it might seem to be from its name. During
the life of the entity given an invariant condition, the invariant
must be true.
The Require, Ensure, and Invariant conditions may be applied to
a subprogram, a type, or a even some variable. The designer of
Eiffel (who did not invent these ideas but incorporated them into
the design of his language), calls this "design by contract." It
is important to understand that this is a run-time contract. Many
safety-critical software practitioners feel this is the wrong place
to evaluate assertions. The SPARK language takes a more conservative
approach to the same idea. Ada probably needs an approach somewhere
between SPARK and Eiffel.
>This construct (I think) could be replaced by an Assert repeated in several
>places. Would it be so useful as to be worthwhile? (Perhaps it would.)
The Require, Ensure, and Invariant are part of the contract and would
appear in the package specification (in Ada) not in the code. The Ada
package specification can already be thought of as some kind of contract.
Because of that, reinforcing the contract with publicly defined assertions
would make sense. The public assertions should state explicitly the
place where the assertion applies. Therefore, pre-condition or post-
condition would be a clear indication to the client of the contract.
Assertions are independent of the implementing code. In Ada this would
make especially good sense because of the full separation between the
definition of what to do (specification) and implementing code to do
it (body). We may want to modify the assertions without touching the
algorithms. In fact, we probably want the assertions to be independent
of the algorithms. Therefore, it makes sense to differentiate between
assertions required to enter the routine, those require for successful
completion, and those required to remain unchanged for the life of each
entity in the design.
I hope this helps to clarify the thinking behind some of my earlier
points. Let me be clear that I am not interested in turning Ada into
Eiffel. I am interested in seeing Ada learn from other language designs.
I know that Tucker explored this idea in great depth during the design
of Ada 95 and understands the pros and cons. He did not lightly dismiss
the notion of pre-, post, and invariant conditions. It was a decision
seriously studied and excluded from Ada 95 for very good reasons.
Richard Riehle
richard@adaworks.com
http://www.adaworks.com
next prev parent reply other threads:[~1999-05-19 0:00 UTC|newest]
Thread overview: 35+ messages / expand[flat|nested] mbox.gz Atom feed top
1999-05-10 0:00 Assertions J & A Richardson
1999-05-10 0:00 ` Assertions Marin David Condic
1999-05-11 0:00 ` Assertions Robert Dewar
1999-05-11 0:00 ` Assertions Nick Roberts
1999-05-11 0:00 ` Assertions Robert Dewar
1999-05-12 0:00 ` Assertions Dale Stanbrough
1999-05-12 0:00 ` Assertions Robert Dewar
1999-05-12 0:00 ` Assertions Tucker Taft
1999-05-12 0:00 ` Assertions Marin David Condic
1999-05-12 0:00 ` Assertions Larry Kilgallen
1999-05-12 0:00 ` Assertions Tucker Taft
1999-05-13 0:00 ` Assertions Nick Roberts
1999-05-17 0:00 ` Assertions Dale Stanbrough
1999-05-19 0:00 ` Assertions Nick Roberts
1999-05-22 0:00 ` Assertions Dale Stanbrough
1999-05-22 0:00 ` Assertions Robert Dewar
1999-05-22 0:00 ` Assertions Ray Blaak
1999-05-22 0:00 ` Assertions Robert Dewar
1999-05-23 0:00 ` Assertions Nick Roberts
1999-05-24 0:00 ` Assertions Dale Stanbrough
1999-05-24 0:00 ` Assertions Ray Blaak
1999-05-23 0:00 ` Assertions Nick Roberts
1999-05-18 0:00 ` Assertions Richard D Riehle
1999-05-19 0:00 ` Assertions Nick Roberts
1999-05-19 0:00 ` Richard D Riehle [this message]
1999-05-20 0:00 ` Assertions stimuli
1999-05-21 0:00 ` Assertions Richard D Riehle
1999-05-21 0:00 ` Assertions Robert Dewar
1999-05-20 0:00 ` Assertions Ehud Lamm
1999-05-21 0:00 ` Assertions Robert Dewar
1999-05-21 0:00 ` Assertions Ehud Lamm
1999-05-21 0:00 ` Assertions Tucker Taft
1999-05-20 0:00 ` Assertions stimuli
1999-05-12 0:00 ` Assertions Peter Amey
1999-05-12 0:00 ` Assertions Robert Dewar
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox