next up previous
Next: References Up: Developing Provably Correct Programs Previous: 4 Comparison

5 Conclusion

Object-oriented languages support the development of software components by means of composition, code inheritance, and genericity. We summarized the problems caused by these techniques in the context of formal specification and verification based on a formal semantics of specifications. Solutions to these problems require further research in the fields of specification, verification, and language support. This will lead to contributions in the following areas: (1) Advanced specification techniques will enable to specify sharing and invariance properties on a high level. (2) Experiences in specification and verification methodology will improve the education of developers and enable the construction of automated verification tools for realistic programs. (3) Semantical module concepts will lead to a better understanding of dependencies between different modules and their specifications and provide more elaborated support of encapsulation. (4) The precise semantical understanding of software components will help to improve constructs for code inheritance and genericity.



Peter Mueller and Arnd Poetzsch-Heffter
Sept. 2, 1997