[comp.lang.eiffel] have you ever tried postconditions or invariants?

duns1222@w203zrz.zrz.tu-berlin.de (Martin Dunschen) (03/23/91)

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

rick@tetrauk.UUCP (Rick Jones) (03/25/91)

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

giddy@astrix.trl.oz.au (David Giddy) (03/28/91)

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