home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #30 / NN_1992_30.iso / spool / comp / lang / eiffel / 1384 < prev    next >
Encoding:
Text File  |  1992-12-20  |  2.2 KB  |  66 lines
  1. Newsgroups: comp.lang.eiffel
  2. Path: sparky!uunet!psinntp!bony1!richieb
  3. From: richieb@bony1.bony.com (Richard Bielak)
  4. Subject: Re: Semantics of invariants
  5. Message-ID: <1992Dec17.190450.24798@bony1.bony.com>
  6. Organization: multi-cellular
  7. References: <1992Dec15.213603.16406@bony1.bony.com> <1992Dec16.163847.17559@nrao.edu>
  8. Date: Thu, 17 Dec 92 19:04:50 GMT
  9. Lines: 55
  10.  
  11. In article <1992Dec16.163847.17559@nrao.edu> cflatter@nrao.edu writes:
  12. >In article 16406@bony1.bony.com, richieb@bony1.bony.com (Richard Bielak) writes:
  13. >>Is the invariant supposed to be true *ALL* the time, once the object is
  14. >>created? 
  15.  
  16. [...]
  17.  
  18. >
  19. >You can invalidate a class invariant inside a function or procedure
  20. >provided that it is true on exit.  In other words the class invariant
  21. >is an implicit conjunct of both the precondition and the postcondition
  22. >of a function or procedure.  Suppose that the class invariant is I and
  23. >the P is the precondition of a procedure of the class as given in the
  24. >require clause and Q is the postcondition as given in the ensure clause:
  25. >then (P and I) is also a precondition of the procedure and (Q and I) is
  26. >also a postcondition of the procedure.
  27. >
  28.  
  29. [...]
  30.  
  31. OK. I understand all this, but consider this situation (in pseudo-Eiffel):
  32.  
  33.         class FOO is
  34.                 export r1, r2
  35.  
  36.             r1 is
  37.                do
  38.                   [...do something here to make the invariant false...]
  39.                   r2;
  40.                end; -- r1
  41.  
  42.             r2 is
  43.                do
  44.                  [... some stuff ...]
  45.                end; -- r2
  46.  
  47.         invariant
  48.                 inv_condition
  49.  
  50.         end; -- FOO
  51.  
  52.  
  53. If we have "x" of type FOO, does the call "x.r1" work or does it fail?
  54. Note that the invariant is false, when routine "r2" is called.
  55.  
  56. One way to deal with this is to insist that the invariant should
  57. always be true - I mean it is an *INVARIANT*.
  58.  
  59. ...richie
  60.  
  61. -- 
  62. * Richie Bielak   (212)-815-3072   |                                          *
  63. * Internet:       richieb@bony.com | Rule #1: Don't sweat the small stuff.    *
  64. * Bang {uupsi,uunet}!bony1!richieb | Rule #2: It's all small stuff.           *
  65. *    - Strictly my opinions -      |                                          *
  66.