Specification and verification of object-oriented software components

• 1. autor: Roth, Andreas (auth)
• Format: Elektroniczne Rozdział
• Wydane: KIT Scientific Publishing 2006
• Hasła przedmiotowe: proof obligations; encapsulation; components; context specification; deductive verification; modular proofs; formal specification; object-orientation
• Dostęp online: 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.