A formal approach to object-oriented software engineering

We show how formal specifications can be integrated into one of the current pragmatic object-oriented software development methods. Jacobson's "Object-Oriented Software Engineering" (OOSE) process is combined with object-oriented algebraic specifications by extending object and interaction diagrams with formal annotations. The specifications are based on Meseguer's rewriting logic and are written in a meta-level extension of the language Maude by process expressions. As a result any such diagram can be associated with a formal specification, proof obligations ensuring invariant properties can be automatically generated, and the refinement s between documents at different abstraction levels can be formally stated and proved.

• Type: Journal
• Year: 2002
• Where: TCS
• Authors: Martin Wirsing, Alexander Knapp
• Keywords: Formal Specification, Object-oriented Software, Pragmatic Object-oriented Software, TCS 2002, Theoretical Computer Science