home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1993 #3 / NN_1993_3.iso / spool / comp / lang / eiffel / 1449 < prev    next >
Encoding:
Internet Message Format  |  1993-01-23  |  2.7 KB
  1. Path: sparky!uunet!mcsun!uknet!mucs!cs.man.ac.uk!mod
  2. From: mod@cs.man.ac.uk (Mike O'Docherty (Teaching Company Associate))
  3. Newsgroups: comp.lang.eiffel
  4. Subject: Re: creation
  5. Message-ID: <mod.727716406@cs.man.ac.uk>
  6. Date: 22 Jan 93 15:26:46 GMT
  7. References: <memo.879182@cix.compulink.co.uk> <175@eiffel.eiffel.com>
  8. Sender: news@cs.man.ac.uk
  9. Lines: 52
  10.  
  11. bertrand@eiffel.com (Bertrand Meyer) writes:
  12.  
  13. >From <mod.727464101@cs.man.ac.uk> by mod@cs.man.ac.uk
  14. >(Mike O'Docherty (Teaching Company Associate)):
  15.  
  16. >> On page 128 of "Eiffel: The Language", it is stated (in the definition of
  17. >> consistency) that postconditions need not be checked on return from a
  18. >> creation procedure. I see no reason why they they should be let off the hook;>> is this a mistake?
  19.  
  20. >Actually the extract does not address what should be checked.
  21. >It defines class consistency, which is a static
  22. >(i.e. mathematical) concept.
  23.  
  24. Point taken. Ok, I'll have to plead ignorance on the *true* meaning of Section
  25. 9.1.2., but it still seems to me that condition 1 should be
  26.  
  27.         {pre } do  {post  ^  INV }
  28.             p    p      p       C
  29.  
  30. >The discussion of run-time assertion monitoring on page 133
  31. >does say what should be checked at run time, and makes no
  32. >distinction between creation procedures and other routines.
  33.  
  34. My point is that it *should* make a distinction, because you *shouldn't* check
  35. invariants on entry to creation procedures *when they are called from a
  36. creation instruction*.
  37.  
  38. Maybe I can stop this going any further by summarising the run-time situation
  39. with assertions switched on, as described by Raphael Manfredi in his message
  40. (for the benefit of anyone else confused so far :-) )
  41.  
  42. 1) Invariants are checked on entry to *every* routine *unless*
  43.     a) That routine is a creation procedure *called from a creation
  44.        instruction*.
  45.     b) that routine call is local (ie. an object calls one of its own
  46.        routines).
  47. 2) Invariants are checked on exit from *every* remote routine call (ie. an
  48.    object's routine called by another object).
  49. 3) Preconditions are checked on entry to *every* routine.
  50. 4) Postconditions are checked on exit from *every* routine.
  51.  
  52. I can't speak for loop variants, loop invariants or check instructions because
  53. I haven't used them (so shoot me :-) ).
  54.  
  55. Mike.
  56.  
  57. -------------------------------------------------------------------------
  58. "Lou Reed was singing about scoring drugs. Tom Robinson was singing about
  59. scoring sex. I don't know what she's singing about, Dolly Mixtures
  60. probably." --- Nicky Campbell on Vanessa Paradis' cover of "Waiting for
  61. the man"   => => => => => => => => => => => => => => =>  mod@cs.man.ac.uk
  62. -------------------------------------------------------------------------
  63.