Hi Rapha,
thanks for the explanation, too bad that this postcondition cannot
be expressed
at the moment.
I beg to differ with "in the end it doesn't matter how Result is calculated".
Consider a very trivial and admittedly somewhat contrived snippet that
illustrates my point, the smallest I could come up with:
feature
multiply(a, b: INTEGER): INTEGER
do
Result = a * a
end
and assume that you test this code by invoking it with two equal valued
arguments, like x = multiply(5,5).
The answer will be correct, 5 squared = 25, and the test will not be able to
flag an error.
Unfortunately, multiply() arrived at that result the wrong way, one that will
bite you in the butt somewhere else.
Clearly the above feature should multiply a and b. I feel we should
have a way
to express that intention.
To improve formal static proofing, it would be nice to have an
extended ensure
clause syntax, something like:
feature
multiply(a, b: INTEGER): INTEGER
do
Result = a * a
ensure
both_args_used: Result DEPENDS_ON(a, b)
end
or something along these lines. It would flag an error message that
'b' was not
used at all. It could provide positive static proof that both our arguments
were indeed used to calculate Result.
Deferring this formal static proof to the backend compiler is something I see
critically, after all: it's Eiffel's promise and aspiration to foster
correctness, robustness, etc., isn't it?
cheers
Hans
Message: 2
Date: Tue, 02 Sep 2014 17:46:17 +0000
From: Raphael Mack <address@hidden>
To: address@hidden
Subject: Re: [Liberty-eiffel] Question about DBC / ensure clause
Message-ID:
<address@hidden>
Content-Type: text/plain; charset=UTF-8; format=flowed; DelSp=Yes
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
------------------------------
_______________________________________________
Liberty-eiffel mailing list
address@hidden
https://lists.gnu.org/mailman/listinfo/liberty-eiffel
End of Liberty-eiffel Digest, Vol 16, Issue 2
*********************************************