[comp.specification] How does formal specification tie in with OOD/OOP?

stuarth@arp.anu.oz.au (Stuart Hungerford) (07/11/90)

I have recently begun to explore the worlds of OOD and OOP and in doing so
the same question keeps occuring to me: How does formal specification
tie in with OOD?

I'm aware of the benefits of rigorous specification for functionally
oriented design so how many of these benefits carry across to OOD?  I'm
not sure how a specification approach would cope with OOD issues like
name clashes in multiple inheritance, polymorphism, etc etc.  If you
have seen any papers, articles, or books describing specification
approaches for OOD/OOP I'd really like to hear about them.

I like the approach taken in Eiffel where class invariants and pre/post 
conditions are used in an attempt to formalize the behaviour of a class to its 
clients and descendants, however these expressions are often couched in terms
of implementation features (which you can see but may not be able to use).

I wonder how appropriate this "look but can't touch" type of specification 
is to OOD in general. 

Thanks if you can enlighten me,


				Stuart Hungerford.
				stuarth@arp.anu.oz.au