Specification and verification of object-oriented software components

• Päätekijä: Roth, Andreas (auth)
• Aineistotyyppi: Elektroninen Kirjan osa
• Julkaistu: KIT Scientific Publishing 2006
• Aiheet: proof obligations; encapsulation; components; context specification; deductive verification; modular proofs; formal specification; object-orientation
• Linkit: DOAB: download the publication; DOAB: description of the publication

This work presents a flexible methodology for formally specifying and deductively verifying object-oriented components.It is based on a simple notion of program correctness. Correctness can be achieved with a novel system of proof obligations, which serve as input to a suitable theorem prover.