Reasoning about pointers in refinement calculus

Ralph Johan Back, Xiaocong Fan, Viorel Preoteasa

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

3 Citations (Scopus)

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
Volume2003-January
ISBN (Electronic)0769520111
DOIs
StatePublished - Jan 1 2003
Event10th Asia-Pacific Software Engineering Conference, APSEC 2003 - Chiang Mai, Thailand
Duration: Dec 10 2003Dec 12 2003

Other

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

Fingerprint

Semantics
Computer programming languages
Object oriented programming

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 (Vol. 2003-January, pp. 425-434). [1254398] IEEE Computer Society. https://doi.org/10.1109/APSEC.2003.01254398
Back, Ralph Johan ; Fan, Xiaocong ; Preoteasa, Viorel. / Reasoning about pointers in refinement calculus. 10th Asia-Pacific Software Engineering Conference, APSEC 2003. Vol. 2003-January IEEE Computer Society, 2003. pp. 425-434
@inproceedings{ee767142d1dc4515a9646c20e706bf28,
title = "Reasoning about pointers in refinement calculus",
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.",
author = "Back, {Ralph Johan} and Xiaocong Fan and Viorel Preoteasa",
year = "2003",
month = "1",
day = "1",
doi = "10.1109/APSEC.2003.01254398",
language = "English (US)",
volume = "2003-January",
pages = "425--434",
booktitle = "10th Asia-Pacific Software Engineering Conference, APSEC 2003",
publisher = "IEEE Computer Society",
address = "United States",

}

Back, RJ, Fan, X & Preoteasa, V 2003, Reasoning about pointers in refinement calculus. in 10th Asia-Pacific Software Engineering Conference, APSEC 2003. vol. 2003-January, 1254398, IEEE Computer Society, pp. 425-434, 10th Asia-Pacific Software Engineering Conference, APSEC 2003, Chiang Mai, Thailand, 12/10/03. https://doi.org/10.1109/APSEC.2003.01254398

Reasoning about pointers in refinement calculus. / Back, Ralph Johan; Fan, Xiaocong; Preoteasa, Viorel.

10th Asia-Pacific Software Engineering Conference, APSEC 2003. Vol. 2003-January IEEE Computer Society, 2003. p. 425-434 1254398.

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

TY - GEN

T1 - Reasoning about pointers in refinement calculus

AU - Back, Ralph Johan

AU - Fan, Xiaocong

AU - Preoteasa, Viorel

PY - 2003/1/1

Y1 - 2003/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=33746087237&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33746087237&partnerID=8YFLogxK

U2 - 10.1109/APSEC.2003.01254398

DO - 10.1109/APSEC.2003.01254398

M3 - Conference contribution

AN - SCOPUS:33746087237

VL - 2003-January

SP - 425

EP - 434

BT - 10th Asia-Pacific Software Engineering Conference, APSEC 2003

PB - IEEE Computer Society

ER -

Back RJ, Fan X, Preoteasa V. Reasoning about pointers in refinement calculus. In 10th Asia-Pacific Software Engineering Conference, APSEC 2003. Vol. 2003-January. IEEE Computer Society. 2003. p. 425-434. 1254398 https://doi.org/10.1109/APSEC.2003.01254398