Anzeige
Erschienen in:
2008 | OriginalPaper | Buchkapitel
A Theory of Pointers for the UTP
verfasst von : Will Harwood, Ana Cavalcanti, Jim Woodcock
Erschienen in: Theoretical Aspects of Computing - ICTAC 2008
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Hoare and He’s unifying theories of programming (UTP) provide a collection of relational models that can be used to study and compare several programming paradigms. In this paper, we add to the UTP a theory of pointers and records that provides a model for objects and sharing in languages like Java and C++. Our work is based on the hierarchical addressing scheme used to refer to record fields (or object attributes) in conventional languages, rather than explicit notions of location. More importantly, we support reasoning about the structure and sharing of data, as well as their, possibly infinite, values. We also provide a general account of UTP theories characterised by conjunctive healthiness conditions, of which our theory is an example.