A refinement methodology for object-oriented programs

DOI10.1007/978-3-642-18070-5_11zbMATH Open1308.68048OpenAlexW1823684783MaRDI QIDQ3067544FDOQ3067544

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

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

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)

Cites Work

• Title not available (Why is that?)
• Refinement Calculus
• The B-Book
• Polymorphic type, region and effect inference
• Specification and verification challenges for sequential object-oriented programs
• Programming Languages and Systems
• Region-based memory management
• A refinement methodology for object-oriented programs

Cited In (6)

• Refinement and retrenchment for programming language data types
• Title not available (Why is that?)
• Deferring elimination of design alternatives in object-oriented methods
• Stepwise refinement of heap-manipulating code in Chalice
• Title not available (Why is that?)
• A refinement methodology for object-oriented programs

Uses Software

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

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)