home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #16 / NN_1992_16.iso / spool / comp / object / 3071 < prev    next >
Encoding:
Internet Message Format  |  1992-07-23  |  2.7 KB
  1. Xref: sparky comp.object:3071 comp.specification:334
  2. Path: sparky!uunet!cis.ohio-state.edu!pacific.mps.ohio-state.edu!linac!att!att!drutx!abasin!weh
  3. From: weh@abasin.dr.att.com (William E. Hopkins)
  4. Newsgroups: comp.object,comp.specification
  5. Subject: Current OOA/OOD and formal methods
  6. Keywords: A++, Z, VDM, formal methods, OOA/OOD
  7. Message-ID: <18822@drutx.ATT.COM>
  8. Date: 30 Jul 92 15:54:51 GMT
  9. Sender: news@drutx.ATT.COM
  10. Reply-To: william.e.hopkins@att.com
  11. Organization: AT&T Bell Laboratories
  12. Lines: 40
  13.  
  14.  
  15. Having just read two papers on Annotated C++ (a.k.a., A++; thanks Rich!),
  16. which describes a notational extension for specifying invariants,
  17. constraints, pre- and post-conditions, etc., on C++ classes and functions,
  18. I'd like to see some inter-mixing of the OOA/OOD (object-oriented analysis
  19. and design) and formal methods ideas.
  20.  
  21. In particular, OOA methods seem to focus on specifying behavior via state
  22. transition diagrams and DFDs, while the formal methods community (e.g., Z
  23. and VDM) specify behavior via predicates (more or less).  On the formal
  24. methods side, I am encouraged by the progress made in both formal
  25. specification and formal verification/derivation, and its application in
  26. a Cleanroom Approach setting.  A++ is a notation and tool set that helps
  27. apply formal techniques to C++.
  28.  
  29. On the other hand, OOA/OOD methods (e.g., Shlaer/Mellor, Rumbaugh et al.)
  30. have a nice intuitive ``feel'' to them, describing via graphical techniques
  31. both structure and behavior.  Unfortunately, they don't provide a formal
  32. enough specification to be able to go on to coding and formally derive the
  33. code from it.  In addition, there seems to be a disconnect between behavior
  34. specified by predicates and behavior specified by state transition diagram.
  35.  
  36. I've used techniques from both areas to accomplish some real ends (e.g.,
  37. Gries' technique enabled me to derive a complex piece of code that
  38. implemented a complex transformation specification and get it right, i.e.,
  39. no bugs ever encountered).  Unfortunately, using OOA/OOD for
  40. higher-level design does not feed into formal code derivation.
  41.  
  42. I like the property formal methods offer of unambiguously specifying
  43. behavior via formal specification and the assurance of derving code
  44. consistent with the specification.  For high-level design, though, manipulating
  45. text just doesn't help construct an overall view of the system components
  46. and behavior.
  47.  
  48. My question to the net: is there a common ground?  Can the formal methods
  49. and graphical methods be brought together?  How do predicates compare to
  50. state transition diagrams in describing and specifying behavior?
  51.  
  52. ------------------------------------------------------------------------------
  53. Bill Hopkins          AT&T Bell Laboratories       william.e.hopkins@att.com
  54.