Re: [Liberty-eiffel] Question about DBC / ensure clause

[Raphael Mack]

Hi Hans,

I fear this is not expressible. Assume

feature
max(a, b: INTEGER): INTEGER
   do
      Result = magic
   ensure
      a >= b implies Result = a
      a <= b implies Result = b
end

at the end it doesn't matter HOW a feature calculates its Result. The  
only thing that matters in the world of DbC is, that a feature gives a  
Result which satisfies its postcondition, if it is called with input  
satisfying its precondition. And this has some beauty, because it this  
interpretation totally abstracts from the implementation and if a  
client (caller) only relies on the contract, it is possible to  
exchange the implementation by something totally different (may it be  
a faster implementation of a simple function or even the replacement  
of a complete object by one of another type (with the same interface -  
and therefore contract.)

On the other side you have a point when you say: a feature  
implementation which doesn't use one of its arguments has defect or at  
least some design flaw. But that's the job of a compiler warning then.

Cheers,
Rapha
Zitat von Hans Zwakenberg  |  Ocean Consulting GmbH <address@hidden>:

> Hi,
>
> how do I formulate an ensure-clause that ascertains that an object's feature
> indeed used each of the parameters to calculate the result, i.e. result
> 'depends' on arg1 and arg2 and that both have indeed been used to arrive at
> result?
>
> confused,
> Hans