home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #30 / NN_1992_30.iso / spool / comp / lang / eiffel / 1375 < prev    next >
Encoding:
Text File  |  1992-12-16  |  1.7 KB  |  39 lines
  1. Newsgroups: comp.lang.eiffel
  2. Path: sparky!uunet!haven.umd.edu!purdue!ames!agate!spool.mu.edu!caen!uvaarpa!cv3.cv.nrao.edu!laphroaig!cflatter
  3. From: cflatter@nrao.edu (Chris Flatters)
  4. Subject: Re: Semantics of invariants
  5. Message-ID: <1992Dec16.163847.17559@nrao.edu>
  6. Sender: news@nrao.edu
  7. Reply-To: cflatter@nrao.edu
  8. Organization: NRAO
  9. References: <1992Dec15.213603.16406@bony1.bony.com>
  10. Date: Wed, 16 Dec 1992 16:38:47 GMT
  11. Lines: 26
  12.  
  13. In article 16406@bony1.bony.com, richieb@bony1.bony.com (Richard Bielak) writes:
  14. >Is the invariant supposed to be true *ALL* the time, once the object is
  15. >created? 
  16. >
  17. >If this is so, you can imagine each object having an "invariant-checker"
  18. >running continously on another processor.
  19. >
  20. >Or is it OK to invalidate the invariant while inside the object's routines,
  21. >as long as the invariant is true on exit.
  22.  
  23. You can invalidate a class invariant inside a function or procedure
  24. provided that it is true on exit.  In other words the class invariant
  25. is an implicit conjunct of both the precondition and the postcondition
  26. of a function or procedure.  Suppose that the class invariant is I and
  27. the P is the precondition of a procedure of the class as given in the
  28. require clause and Q is the postcondition as given in the ensure clause:
  29. then (P and I) is also a precondition of the procedure and (Q and I) is
  30. also a postcondition of the procedure.
  31.  
  32. If the values of class attributes are not modified outside of the procedures
  33. and functions of that class it is sufficient to check the class invariant
  34. on exit from each function or procedure since the invarient will not
  35. change between exit from one function/procedure and entry into the next.
  36.  
  37.     Chris Flatters
  38.     cflatter@nrao.edu
  39.