A Theory of Pointers for the UTP

DOI10.1007/978-3-540-85762-4_10MaRDI QIDQ5505599zbMATH OpenOpenAlexFDO

Authors Will Harwood, Ana Cavalcanti, Jim Woodcock

Publication date 27 January 2009

Published in Theoretical Aspects of Computing - ICTAC 2008 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-85762-4_10

zbMATH Keywords

relationssemanticsrefinementobject models

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• Pointers and Records in the Unifying Theories of Programming
• Unifying theories of locations
• Object-Orientation in the UTP
• UTP and Sustainability
• Unifying Theories of Objects

Cites work

• scientific article; zbMATH DE number 4011906 (Why is no real title available?)
• scientific article; zbMATH DE number 108549 (Why is no real title available?)
• scientific article; zbMATH DE number 3557184 (Why is no real title available?)
• scientific article; zbMATH DE number 2013592 (Why is no real title available?)
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• scientific article; zbMATH DE number 3410595 (Why is no real title available?)
• A Theory of Pointers for the UTP
• BI as an assertion language for mutable data structures
• Compositional Reasoning for Pointer Structures
• ERC -- an object-oriented refinement calculus for Eiffel
• Object-Orientation in the UTP
• Pointers and Records in the Unifying Theories of Programming
• Predicate transformer semantics of a higher-order imperative language with record subtyping

Cited in

(25)

• Unifying theories of programming in Isabelle
• Safety-critical Java programs from \textsf{Circus} models
• The safety-critical Java memory model formalised
• Mechanical reasoning about families of UTP theories
• Correct hardware synthesis
• Denotational semantics of channel mobility in UTP-CSP
• A local-time-induced unique pointer basis
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Mathematics of Program Construction
• scientific article; zbMATH DE number 1390329 (Why is no real title available?)
• A stepwise approach to linking theories
• An algebraic approach to the design of compilers for object-oriented languages
• UTP semantics of reactive processes with continuations
• UTP, \textsf{\textit{Circus}}, and Isabelle
• Angelic processes for CSP via the UTP
• A Theory of Pointers for the UTP
• scientific article; zbMATH DE number 1949583 (Why is no real title available?)
• Pointers and Records in the Unifying Theories of Programming
• Unifying theories of locations
• The dynamic frames theory
• Object-Orientation in the UTP
• Higher-order UTP for a theory of methods
• Semantic inheritance in unifying theories of programming
• Towards a UTP semantics for Modelica
• Unifying theories of confidentiality

This page was built for publication: A Theory of Pointers for the UTP

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