A Theory of Pointers for the UTP

DOI10.1007/978-3-540-85762-4_10zbMATH Open1161.68388OpenAlexW134026565MaRDI QIDQ5505599FDOQ5505599

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

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

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)

Cites Work

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

Cited In (25)

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

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)