A refinement methodology for object-oriented programs

Conference object English OPEN
Tafat, Asma; Boulmé, Sylvain; Marché, Claude;
  • 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 t... View more
  • 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
Share - Bookmark