A Theory of Pointers for the UTP

DOI10.1007/978-3-540-85762-4_10zbMath1161.68388OpenAlexW134026565MaRDI QIDQ5505599

Will Harwood, Ana Cavalcanti, J. C. P. 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

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

Related Items (14)

Higher-Order UTP for a Theory of Methods ⋮ An algebraic approach to the design of compilers for object-oriented languages ⋮ Unifying Theories of Programming in Isabelle ⋮ The safety-critical Java memory model formalised ⋮ Mechanical reasoning about families of UTP theories ⋮ Automated verification of shape, size and bag properties via user-defined predicates in separation logic ⋮ Towards a UTP Semantics for Modelica ⋮ A Stepwise Approach to Linking Theories ⋮ Safety-critical Java programs from \textsf{Circus} models ⋮ Denotational semantics of channel mobility in UTP-CSP ⋮ Angelic processes for CSP via the UTP ⋮ The dynamic frames theory ⋮ Correct hardware synthesis ⋮ A Theory of Pointers for the UTP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• ERC -- an object-oriented refinement calculus for Eiffel
• Compositional Reasoning for Pointer Structures
• BI as an assertion language for mutable data structures
• Object-Orientation in the UTP
• Pointers and Records in the Unifying Theories of Programming
• A Theory of Pointers for the UTP
• Predicate transformer semantics of a higher-order imperative language with record subtyping

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