Higher-order UTP for a theory of methods

DOI10.1007/978-3-642-35705-3_10MaRDI QIDQ3455652zbMATH OpenOpenAlexFDO

Authors Frank Zeyda, Ana Cavalcanti

Publication date 11 December 2015

Published in Unifying Theories of Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-35705-3_10

zbMATH Keywords

consistencysemanticsrecursionobject-orientation

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) Semantics in the theory of computing (68Q55)

Recommendations

• Object-Orientation in the UTP
• UTP and Sustainability
• A Theory of Pointers for the UTP
• Unifying Theories of Objects
• Mechanical reasoning about families of UTP theories

Cites work

• A Theory of Pointers for the UTP
• Isabelle/HOL. A proof assistant for higher-order logic
• Mechanical reasoning about families of UTP theories
• Mechanising a Unifying Theory
• Object-Orientation in the UTP
• Predicate transformers and higher-order programs
• The consistency theorem for free type definitions in \(Z\)
• Unifying Theories in ProofPower-Z
• rCOS: a refinement calculus of object systems

Cited in

(4)

• Mechanical Reasoning about Families of UTP Theories
• Object-Orientation in the UTP
• An Axiomatic Value Model for Isabelle/UTP
• Higher order programming in Java: introspection, subsumption and extraction

Describes a project that uses

Uses Software

• Z
• ProofPower

This page was built for publication: Higher-order UTP for a theory of methods

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