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

"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!