View mode: basic / threaded / horizontal-split · Log in · Help
March 08, 2003
Contracts
Hi,

   There are some features needed in contracts, copied shamelessly from
Eiffel.


1. Function called in contracts shouldn't have their contracts verified, to
avoid recursion in contracts. It's in the Eiffel standard (ETL 2) and AFAIK
all compilers support this. SmartEiffel goes a little further and supports
one level of recursion on contracts. Eiffel libraries are very robust, with
elegant contracts supporting symmetrical properties and all relevant
contracts written down (check the ELKS 2002 String
http://www.eiffel-nice.org/standards/wip/string/string2002proposal.txt for
more details).

2. There is no "old" expression available. Such expressions are useful to
define contracts for operations with side-effects. Defining a complete
mutable stack ADT requires old expressions:

template TStack(T) {
   class Stack {
       public int size();
       public boolean isEmpty()
       out(result) {
           assert(result == (size() == 0));
       }
       public void push(T item)
       out {
           assert(top() == item);
           assert(size() == old(size() + 1));
       } body {}
       public T pop()
       in {
           assert(!isEmpty());
       } out(result) {
           assert(result == old(top()));
           assert(size() == old(size() - 1));
       } body {}
       public T top()
       in {
           assert(!isEmpty());
       } out(result) {
           assert(size() == old(size()));
       } body {}
   }
}

Old expressions may lead to subtle bugs in contracts, because some people
may write "old(this.data) != this.data" without realizing that a deep copy
operation was needed to get the correct data change "old(this.data.clone())
!= this.data".

3. Contracts aren't inherited but they should.


   When will these features be available?

   Best regards,
   Daniel Yokomiso.

"Experts are people who successfully calibrated their intuition."
- Thomas K├╝hne


---
Outgoing mail is certified Virus Free.
Checked by AVG anti-virus system (http://www.grisoft.com).
Version: 6.0.459 / Virus Database: 258 - Release Date: 25/2/2003
March 11, 2003
Re: Contracts
"Daniel Yokomiso" <daniel_yokomiso@yahoo.com.br> wrote in message
news:b4d1s9$e8s$1@digitaldaemon.com...
> 1. Function called in contracts shouldn't have their contracts verified,
to
> avoid recursion in contracts. It's in the Eiffel standard (ETL 2) and
AFAIK
> all compilers support this. SmartEiffel goes a little further and supports
> one level of recursion on contracts. Eiffel libraries are very robust,
with
> elegant contracts supporting symmetrical properties and all relevant
> contracts written down (check the ELKS 2002 String
> http://www.eiffel-nice.org/standards/wip/string/string2002proposal.txt for
> more details).

Sounds like a good idea.

> 2. There is no "old" expression available. Such expressions are useful to
> define contracts for operations with side-effects. Defining a complete
> mutable stack ADT requires old expressions:
>
> template TStack(T) {
>     class Stack {
>         public int size();
>         public boolean isEmpty()
>         out(result) {
>             assert(result == (size() == 0));
>         }
>         public void push(T item)
>         out {
>             assert(top() == item);
>             assert(size() == old(size() + 1));
>         } body {}
>         public T pop()
>         in {
>             assert(!isEmpty());
>         } out(result) {
>             assert(result == old(top()));
>             assert(size() == old(size() - 1));
>         } body {}
>         public T top()
>         in {
>             assert(!isEmpty());
>         } out(result) {
>             assert(size() == old(size()));
>         } body {}
>     }
> }
>
> Old expressions may lead to subtle bugs in contracts, because some people
> may write "old(this.data) != this.data" without realizing that a deep copy
> operation was needed to get the correct data change
"old(this.data.clone())
> != this.data".

I'll have to investigate that.

> 3. Contracts aren't inherited but they should.

I agree.

>     When will these features be available?

I don't know!
Top | Discussion index | About this forum | D home