Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!uunet!mcsun!ukc!pyrltd!tetrauk!rick
From: rick@tetrauk.UUCP (Rick Jones)
Newsgroups: comp.lang.eiffel
Subject: Re: have you ever tried postconditions or invariants?
Keywords: class invariant, postcondition, ensure
Message-ID: <1118@tetrauk.UUCP>
Date: 25 Mar 91 09:53:56 GMT
References: <293@mailgzrz.tu-berlin.de>
Reply-To: rick@tetrauk.UUCP (Rick Jones)
Organization: Tetra Ltd., Maidenhead, UK
Lines: 42

In article <293@mailgzrz.tu-berlin.de> duns1222@w203zrz.zrz.tu-berlin.de (Martin Dunschen) writes:
|>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
		 ^^^^		this is always false!
|>    end -- push
|>
|>end -- class DUM1

Given that your routine "push" has a postcondition which is always false, I
would never expect it to succeed.  The same is true for your (commented out)
precondition.  That will always fail as well.

Or have I misunderstood the question?

-- 
Rick Jones, Tetra Ltd.  Maidenhead, Berks, UK
rick@tetrauk.uucp

The dynamics of a freeway approximates to a shoal of fish in 1.5 dimensions