Reasoning about pointers in refinement calculus

Ralph Johan Back, Xiaocong Fan, Viorel Preoteasa

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Scopus citations


Pointers are an important programming concept. They are used explicitely or implicitly in many programming languages. In particular, the semantics of object-oriented programming languages rely on pointers. We introduce a semantics for pointer structures. Pointers are seen as indexes and pointer fields are functions from these indexes to values. Using this semantics we turn all pointer operations into simple assignments and then we use refinement calculus techniques to construct a pointer-manipulating program that checks whether or not a single linked list has a loop. We also introduce an induction principle on pointer structures in order to reduce complexity of the proofs.

Original languageEnglish (US)
Title of host publication10th Asia-Pacific Software Engineering Conference, APSEC 2003
PublisherIEEE Computer Society
Number of pages10
ISBN (Electronic)0769520111
StatePublished - Jan 1 2003
Event10th Asia-Pacific Software Engineering Conference, APSEC 2003 - Chiang Mai, Thailand
Duration: Dec 10 2003Dec 12 2003

Publication series

NameProceedings - Asia-Pacific Software Engineering Conference, APSEC
ISSN (Print)1530-1362


Other10th Asia-Pacific Software Engineering Conference, APSEC 2003
CityChiang Mai

All Science Journal Classification (ASJC) codes

  • Software


Dive into the research topics of 'Reasoning about pointers in refinement calculus'. Together they form a unique fingerprint.

Cite this