A Graph-Based Implementation for Mechanized Refinement Calculus of OO Programs

DOI10.1007/978-3-642-19829-8_17zbMath1325.68066OpenAlexW1882245948MaRDI QIDQ2999325

Zhi-Ming 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)

Uses Software

• rCOS
• LOOP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• rCOS: a refinement calculus of object systems
• Refinement and verification in component-based model-driven design
• A program refinement tool
• ERC -- an object-oriented refinement calculus for Eiffel
• Harnessing rCOS for Tool Support —The CoCoME Experience

This page was built for publication: A Graph-Based Implementation for Mechanized Refinement Calculus of OO Programs