Re: [Liberty-eiffel] DbC - Ensure clause....

[Cyril ADRIAN]

Hans,

Sorry to be late in that discussion but my week was quite busy in the office.

You are mixing contracts and unit tests.

Contracts specify behaviour. How would you ensure that your contract is "less" buggy than the code?

example:

feature
   multiply(a, b: INTEGER): INTEGER
      do
         Result = a * a
   ensure
      both_args_used:  Result DEPENDS_ON(a, a)
end

Unit tests catch specific mistakes such as the one you describe.

feature

   test do

      assert(multiply(5,5) = 25)

      assert(multiply(2,4) = 8)
   end

-- but obviously even unit tests can be wrong... Only test redundancy will catch that (code redundancy, but also "eyeballs" redundancy). And adding tests for each problem found by your users :-)

A good program should be equiped with both contracts and unit tests (the latter running with contracts full checked).

Cheers,

Cyril

2014-09-03 18:10 GMT+02:00 Hans Zwakenberg | Ocean Consulting GmbH <address@hidden>:

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
> *********************************************
>