Encoding object-Z in Isabelle/HOL

DOI10.1007/3-540-45648-1_5MaRDI QIDQ4472177zbMATH OpenFDO

Authors Graeme Smith, Florian Kammüller, Thomas Santen

Publication date 3 August 2004

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

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2272/22720082.htm

zbMATH Keywords

higher-order logicIsabelleObject-Zreference semantics

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A proposal for a formal OCL semantics in Isabelle/HOL
• An extensible encoding of object-oriented data models in HOL. With an application to IMP++
• A Mechanized Model of the Theory of Objects
• Semantics, calculi, and analysis for object-oriented specifications
• The Isabelle Framework

Cited in

(9)

• An extensible encoding of object-oriented data models in HOL. With an application to IMP++
• Representing object code
• On the Formalization of Z-Transform in HOL
• Theoretical Aspects of Computing – ICTAC 2005
• A Mechanized Model of the Theory of Objects
• A structure preserving encoding of Z in Isabelle/HOL
• The HOL-CSP Refinement Toolkit
• HOL-CSP Version 2.0
• A Sound Type System for Physical Quantities, Units, and Measurements

Describes a project that uses

Uses Software

• Isabelle
• Isabelle/HOL

This page was built for publication: Encoding object-Z in Isabelle/HOL

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