redefining require and ensure clauses 
Author Message
 redefining require and ensure clauses


> ... The ensure
> clause of externalise should have the same logic as the require clause of
> the internalise feature, each one parsing the data to check that it
> correctly specifies a consistent state for an object of the Current class.

> If this is done using a further function, check_external_data(), redefined
> suitably on each descendant, very little problem arises.  In fact, this
> seems a good way to allow the preconditions and postconditions to be
> checked.

> My problem is this:  What I have done seems to sidestep, albeit neatly,
> the rules built in to Eiffel restricting how assertions may vary in
> redefined inherited features.

> Is what I propose bad SE practice? Are there inherent dangers in this
> sidestepping?

What you have done is fine, and has no "gotchas" that I'm aware of.
Your assertions are at a higher level of abstraction than the program
code of 'externalise' and 'internalise'. You are using feature
'check_external_data' to supply that higher level of abstraction,
and _at_that_level_of_abstraction_ you are not weakening the precondition
or strengthening the postcondition.

> N.B. 1) I use the term covariance, but I cannot remember if this is
> correct. Please advise me of the correct term(s) for what happens to
> redefined require and ensure clauses.

I would probably refer to "weakening the precondition in a descendant"
and "strengthening the postcondition in a descendant".

"Covariance" refers to types (e.g. argument and function return types).

> 2) I have used C-style function
> names, for which I am deeply sorry.  I simply regard these as easier to
> discern from normal text than Eiffel feature names without specified
> types.

I can cope with that, though I'd probably name the function
'is_valid_external_data' because 'check_external_data' sounds like
a procedure to me.

> 3) I refer vaguely to a bitstream class, but I do not know if one
> exists in Eiffel, nor if it is what I want.  I mean a class allowing an
> array of bits.

Class "BIT n" is a bit vector, good for low-level bit manipulation.
However, it's not a stream. The "BIT n" class is not mentioned in
the Eiffel Library Standard (95 Vintage) but it's supplied by all

-- Roger Browne, 6 Bambers Walk, Wesham, PR4 3DG, UK | Ph 01772-687525
-- Everything Eiffel: http://www.*-*-*.com/ | +44-1772-687525

Sun, 30 Jul 2000 03:00:00 GMT  
 [ 2 post ] 

 Relevant Pages 

1. Difference between require and ensure just syntactic sugar?

2. require, ensure, and Design by Contract

3. On REDEFINES clause

4. Incorrect data-name in REDEFINES clause

5. Beyond assert-- require, ensure Eiffelisms

6. Newbie: Ensuring a Required Argument for Constructor?

7. testing runtime class in require clause

8. with System still required for address clauses ?

9. Cut in a Clause -- Global to the Clause?

10. binary clauses,n-ary to binary clauses

11. require, require-library in PLT-scheme


Powered by phpBB® Forum Software