A refinement methodology for object-oriented programs

Conference object English OPEN
Tafat , Asma ; Boulmé , Sylvain ; Marché , Claude (2010)
  • Publisher: Karlsruhe University
  • Subject: [ 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.
  • References (29)
    29 references, page 1 of 3

    1. J.-R. Abrial. The B-Book, assigning programs to meaning. Cambridge University Press, 1996.

    2. R.-J. Back and J. von Wright. Refinement Calculus: A Systematic Introduction. SpringerVerlag, 1998.

    3. A. Banerjee, D. A. Naumann, and S. Rosenberg. Regional logic for local reasoning about global invariants. In European Conference on Object-Oriented Programming (ECOOP'08), Paphos, Cyprus, July 2008.

    4. M. Barnett, R. DeLine, M. Fähndrich, K. R. M. Leino, and W. Schulte. Verification of object-oriented programs with invariants. Journal of Object Technology, 3(6):27-56, June 2004.

    5. M. Barnett, R. DeLine, B. Jacobs, B.-Y. E. Chang, and K. R. M. Leino. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In FMCO'05, volume 4111 of LNCS, pages 364-387, 2005.

    6. M. Barnett, K. R. M. Leino, and W. Schulte. The Spec# Programming System: An Overview. In Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS'04), volume 3362 of LNCS, pages 49-69. Springer, 2004.

    7. P. Baudin, J.-C. Filliâtre, C. Marché, B. Monate, Y. Moy, and V. Prevosto. ACSL: ANSI/ISO C Specification Language, 2008. http://frama-c.cea.fr/acsl.html.

    8. P. Behm, P. Benoit, A. Faivre, and J.-M. Meynadier. Météor: A successful application of B in a large project. In Formal Methods'99, volume 1708 of LNCS, pages 348-387. Springer, Sept. 1999.

    9. S. Boulmé and M.-L. Potet. Interpreting invariant composition in the B method using the Spec# ownership relation: a way to explain and relax B restrictions. In J. Julliand and O. Kouchnarenko, editors, B 2007, volume 4355 of LNCS. Springer, 2007.

    10. C.-B. Breunesse and E. Poll. Verifying JML specifications with model fields. In FTfJP'03, 2003.

  • Metrics
    No metrics available
Share - Bookmark