Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!samsung!munnari.oz.au!astrix!giddy
From: giddy@astrix.trl.oz.au (David Giddy)
Newsgroups: comp.lang.eiffel
Subject: Re: have you ever tried postconditions or invariants?
Keywords: class invariant, postcondition, ensure
Message-ID: <7189@munnari.oz.au>
Date: 27 Mar 91 23:27:59 GMT
References: <293@mailgzrz.tu-berlin.de>
Sender: news@cs.mu.oz.au
Reply-To: d.giddy@trl.oz.au
Organization: Telecom Research Laboratories
Lines: 25

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)
> 


I agree that you should be getting a postcondition violation. As you mention
that the problem also occurs with invariants, but not with preconditions,
I am left wondering if you have enabled all assertion checking in your
SDF (.eiffel). The default is to ONLY check preconditions. This would be 
consistent with your results.

Regards,

David.

______________________________________________________________________________
David Giddy,			Voice: +61 3 541 6388	   Fax: +61 3 543 1944
Telecom Research Laboratories, P.O. Box 249, Clayton, Victoria 3168, AUSTRALIA
Internet: d.giddy@trl.oz.au
X400:    g=david s=giddy ou=trl o=telecom prmd=telecom006 admd=telememo c=au