Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!uunet!math.fu-berlin.de!opal!mailgzrz!duns1222
From: duns1222@w203zrz.zrz.tu-berlin.de (Martin Dunschen)
Newsgroups: comp.lang.eiffel
Subject: have you ever tried postconditions or invariants?
Keywords: class invariant, postcondition, ensure
Message-ID: <293@mailgzrz.tu-berlin.de>
Date: 22 Mar 91 16:10:44 GMT
Sender: news@mailgzrz.tu-berlin.de
Organization: TUBerlin
Lines: 28
Nntp-Posting-Host: w203zrz.zrz.tu-berlin.de

We just tried to use postconditions to check an inconsistency
in a class. I include a small example, which does not work the way we
expect it (with an exception like: "postcondition test violated").
As a precondition everything is fine. Similar problems occured using
class invariants. So, where's the mistake? (We use Version 2.3 Level 4)

class dum1

feature
    create is
    do
       push;
    end; -- create

    full: BOOLEAN is
    do
        Result := false
    end;-- full

    push is
--     require
--       test: full
    do
       ensure
         test: full
    end -- push

end -- class DUM1