A refinement methodology for object-oriented programs

DOI10.1007/978-3-642-18070-5_11MaRDI QIDQ3067544zbMATH OpenOpenAlexFDO

Authors Asma Tafat, Sylvain Boulmé, Claude Marché

Publication date 21 January 2011

Published in Formal Verification of Object-Oriented Software (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-18070-5_11

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Abstract data types; algebraic specification (68Q65)

Recommendations

• A calculus of refinements for program derivations
• Refinement
• Stepwise refinement of heap-manipulating code in Chalice
• Refinement and retrenchment for programming language data types
• A program refinement tool

Cites work

• scientific article; zbMATH DE number 605806 (Why is no real title available?)
• A refinement methodology for object-oriented programs
• Polymorphic type, region and effect inference
• Programming Languages and Systems
• Refinement Calculus
• Region-based memory management
• Specification and verification challenges for sequential object-oriented programs
• The B-Book

Cited in

(6)

• Refinement and retrenchment for programming language data types
• scientific article; zbMATH DE number 2080628 (Why is no real title available?)
• Deferring elimination of design alternatives in object-oriented methods
• Stepwise refinement of heap-manipulating code in Chalice
• scientific article; zbMATH DE number 1002576 (Why is no real title available?)
• A refinement methodology for object-oriented programs

Describes a project that uses

Uses Software

• Boogie
• Caduceus
• Spec#
• JML
• Why3
• ACSL
• KRAKATOA

This page was built for publication: A refinement methodology for object-oriented programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3067544)