Reasoning about pointers in refinement calculus

Ralph Johan Back, Xiaocong Fan, Viorel Preoteasa

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

3 Scopus citations

Abstract

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
Pages425-434
Number of pages10
ISBN (Electronic)0769520111
DOIs
Publication statusPublished - 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
Volume2003-January
ISSN (Print)1530-1362

Other

Other10th Asia-Pacific Software Engineering Conference, APSEC 2003
CountryThailand
CityChiang Mai
Period12/10/0312/12/03

    Fingerprint

All Science Journal Classification (ASJC) codes

  • Software

Cite this

Back, R. J., Fan, X., & Preoteasa, V. (2003). Reasoning about pointers in refinement calculus. In 10th Asia-Pacific Software Engineering Conference, APSEC 2003 (pp. 425-434). [1254398] (Proceedings - Asia-Pacific Software Engineering Conference, APSEC; Vol. 2003-January). IEEE Computer Society. https://doi.org/10.1109/APSEC.2003.01254398