Verifying Executable Object-Oriented Specifications with Separation Logic

Specifications of Object-Oriented programs conventionally employ Boolean expressions of the programming language for assertions. Programming errors can be discovered by checking at runtime whether an assertion, such as a precondition or class invariant, holds. In this work, we show how separation logic can be used to verify that these executable specifications will always hold at runtime. Both the program and its executable assertions are verified with respect to separation logic specifications. A novel notion called relative purity embraces historically problematic side-effects in executable specifications, and verification boils down to proving connecting implications. Even model-based specifications can be verified. The framework is also well-suited to separation logic proof tools and now implemented in jStar. Numerous automatically verified examples illustrate the framework's use and utility. Key words: Object-orientation, Specification, Verification, Separation logic, Executa...

• Type: Conference
• Year: 2010
• Where: ECOOP
• Authors: Stephan van Staden, Cristiano Calcagno, Bertrand Meyer
• Keywords: ECOOP 2010, Executable Assertions, Executable Specifications, Programming Languages, Separation Logic