Difference between require and ensure just syntactic sugar? 
Author Message
 Difference between require and ensure just syntactic sugar?

Is there any difference in the evaluation of require expressions
(Eiffel keyword for pre-condition expressions) and ensure expressions
(Eiffel keyword for post-condition expressions), beyond:

* A require expression can only be evaluated before execution of the
routine (method) body.

* An ensure expression can only be evaluated after the routine
(method) body completes execution.

* The keywords "old" (value of a variable at entry) and "nochange"
(true if the referent is unchanged from entry to exit) are restricted
to ensure expressions (I think one of these may be deprecated.)

* Require and ensure can be enabled/disabled individually at compile
time.

* Behavior of both with repsect to percolation and exceptions appears
to the same.

Can anyone add to the above list of differences? To be clear, I'm
*not* asking about the general difference/usage between pre and post
conditions, just the implementation details.

The mechanics of expression evaluation for both appear to be
identical. In this sense, are the require and ensure keywords just
syntactic sugar?

Tia
Bob Binder



Mon, 16 May 2005 03:38:55 GMT  
 Difference between require and ensure just syntactic sugar?

Quote:

> Is there any difference in the evaluation of require expressions
> (Eiffel keyword for pre-condition expressions) and ensure expressions
> (Eiffel keyword for post-condition expressions), beyond:

[...]

Quote:
> Can anyone add to the above list of differences?

Preconditions can only be weakened in descendant classes,
and postconditions can only be strengthened. This is
an important property of Design By Contract.

--
Eric Bezault

http://www.gobosoft.com



Mon, 16 May 2005 03:46:25 GMT  
 Difference between require and ensure just syntactic sugar?

Quote:

> Is there any difference in the evaluation of require expressions
> (Eiffel keyword for pre-condition expressions) and ensure expressions
> (Eiffel keyword for post-condition expressions), beyond:
>   [snip]
> * Behavior of both with repsect to percolation and exceptions appears
> to the same.
>   [snip]

> Can anyone add to the above list of differences? To be clear, I'm
> *not* asking about the general difference/usage between pre and post
> conditions, just the implementation details.

This seems like an odd request. One of the nice things about Eiffel is
that we can leave "the implementation details" to the compiler.

Require and ensure are two very different mechanisms, and they serve
very different purposes. They do share the bulk of their of syntax
(being mainly boolean expressions), but the semantics are quite
different.

"Require" is always processed on every entry to the method. It is
processed after the class invariant has been processed (if any, and if
the call was a qualified call). If any Assertion_clause of the
precondition evaluates to "false" and the precondition was introduced
with "require else", then the precondition of the precursor
implementation will be applied instead. If the joint precondition
(from the current implementation and its precursors) fails, an
exception with the exception code "Precondition" is thrown to the
caller. This exception is not presented to the method whose
precondition failed, nor to the default_rescue feature of the object
(if present), because preconditions are binding solely on the caller.
Because the called method does not receive the exception, it cannot
retry.

"Ensure" is processed on every non-exceptional exit from the method.
It is processed before the class invariant (if any, and if the call
was a qualified call). If the postcondition succeeds and it was
introduced with "ensure then", the postcondition of the precursor
implementation will then be applied as well. If the joint
postcondition (from the current implementation and its precursors)
fails, an exception with the exception code "Postcondition" is thrown
to the failing method. The exception is presented to the failing
method because postconditions are binding solely on the method (since
it has accepted its preconditions), not on the caller. Because the
called method receives the exception, it can retry the operation if it
wishes. If the called method has no rescue clause, the exception is
presented to the default_rescue feature of the object containing the
called method, if it has a default_rescue feature.

So... other than the syntax, when they're called, how they combine
with precursors, what exception they throw, and who the exception is
presented to, they're almost the same :-)



Mon, 16 May 2005 12:28:49 GMT  
 Difference between require and ensure just syntactic sugar?
[...]

Quote:

> Can anyone add to the above list of differences? To be clear, I'm
> *not* asking about the general difference/usage between pre and post
> conditions, just the implementation details.

> The mechanics of expression evaluation for both appear to be
> identical. In this sense, are the require and ensure keywords just
> syntactic sugar?

'Require' statements can only reference public features or input
parameters. In other words, a client class can execute everything that
a requre clause can.

'Ensure' statements can access private features. This is necessary to
guarantee that the feature has fulfilled it's contract, which may
include results not visible to the client.

Greg C



Mon, 16 May 2005 23:39:05 GMT  
 Difference between require and ensure just syntactic sugar?

Quote:

> Is there any difference in the evaluation of require expressions
> (Eiffel keyword for pre-condition expressions) and ensure expressions
> (Eiffel keyword for post-condition expressions), beyond:
>  [snip]

Oh yeah, and one more thing:

If a feature which is a function with no arguments in a parent class
is redefined into an attribute in a subclass, the postcondition for
that feature (including its precursors) is moved into the class
invariant for the redefining class, with each occurrence of "Result"
being replaced by the name of the attribute feature.

Any precondition for the feature merely becomes irrelevant.



Fri, 20 May 2005 07:10:17 GMT  
 
 [ 5 post ] 

 Relevant Pages 

1. need quote about syntactic sugar

2. Origin of the term "syntactic sugar"

3. Syntactic Sugar Question

4. Templating and syntactic sugar

5. syntactic sugar for filesystem access in Python

6. Is it just Syntactic Sugar ?

7. string interpolation syntactic sugar

8. how to define quote-like operators? (syntactic sugar)

9. Syntactic sugar for constructing arrays

10. need quote about syntactic sugar

11. a = b = 1 just syntactic sugar?

12. Hugs: syntactic differences and polymorphic types...

 

 
Powered by phpBB® Forum Software