A refinement methodology for object-oriented programs
Tafat , Asma
Boulmé , Sylvain
Marché , Claude
- Publisher: Karlsruhe University
[ INFO.INFO-LO ] Computer Science [cs]/Logic in Computer Science [cs.LO]
International audience; Refinement is a well-known approach for developing correct-byconstruction software. It has been very successful for producing high quality code e.g., as implemented in the B tool. Yet, such refinement techniques are restricted in the sense that they forbid aliasing (and more generally sharing of data-structures), which often happens in usual programming languages. We propose a sound approach for refinement in presence of aliases. Suitable abstractions of programs are defined by algebraic data types and the so-called model fields. These are related to concrete program data using coupling invariants. The soundness of the approach relies on methodologies for (1) controlling aliases and (2) checking side-effects, both in a modular way.