A graph-based implementation for mechanized refinement calculus of OO programs

DOI10.1007/978-3-642-19829-8_17MaRDI QIDQ2999325zbMATH OpenOpenAlexFDO

Authors Zhiming Liu, Charles Morisset, Shu-Ling Wang

Publication date 12 May 2011

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-19829-8_17

zbMATH Keywords

theorem provingIsabelleproof obligationsrCOS

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Graph transformations for object-oriented refinement
• scientific article; zbMATH DE number 1104377
• ERC -- an object-oriented refinement calculus for Eiffel
• A program refinement tool
• A Mechanized Model of the Theory of Objects

Cites work

• scientific article; zbMATH DE number 1701766 (Why is no real title available?)
• scientific article; zbMATH DE number 605806 (Why is no real title available?)
• A program refinement tool
• ERC -- an object-oriented refinement calculus for Eiffel
• Harnessing rCOS for Tool Support —The CoCoME Experience
• Refinement and verification in component-based model-driven design
• Unifying theories for logic programming
• rCOS: a refinement calculus of object systems

Cited in

(1)

• Graph transformations for object-oriented refinement

Describes a project that uses

Uses Software

• LOOP
• rCOS

This page was built for publication: A graph-based implementation for mechanized refinement calculus of OO programs

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