An inheritance-based technique for building simulation proofs incrementally

This paper presents a technique for incrementally constructing safety specifications, abstract algorithm descriptions, and simulation proofs showing that algorithms meet their specifications. The technique for building specifications (and algorithms) allows a child specification (or algorithm) to inherit from its parent by two forms of incremental modification: (a) interface extension, where new forms of interaction are added to the parent's interface, and (b) specialization (subtyping), where new data, restrictions, and effects are added to the parent's behavior description. The combination of interface extension and specialization constitutes a powerful and expressive incremental modification mechanism for describing changes that do not override the behavior of the parent, although it may introduce new behavior. Consider the case when incremental modification is applied to both a parent specification S and a parent algorithm A. A proof that the child algorithm A implements...

• Type: Conference
• Year: 2000
• Where: ICSE
• Authors: Idit Keidar, Roger Khazan, Nancy A. Lynch, Alexander A. Shvartsman
• Keywords: ICSE 2000, Incremental Modification, Interface Extension, Simulation Proof, Software Engineering