• Daniel Yokomiso (55/55) Mar 08 2003 Hi,
• Walter (10/54) Mar 11 2003 to

"Daniel Yokomiso" <daniel_yokomiso yahoo.com.br> writes:

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

"Walter" <walter digitalmars.com> writes:

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