Weak Arithmetic Completeness of Object-Oriented First-Order Assertion Networks

Stijn de Gouw, Frank S. de Boer, Wolfgang Ahrendt, Richard Bubel

Research output: Chapter in Book/Report/Conference proceedingConference article in proceedingAcademicpeer-review

Abstract

We present a completeness proof of the inductive assertion method for object-oriented programs extended with auxiliary variables. The class of programs considered are assumed to compute over structures which include the standard interpretation of Presburger arithmetic. Further, the assertion language is first-order, i.e., quantification only ranges over basic types like that of the natural numbers, Boolean and Object.
Original languageEnglish
Title of host publicationSOFSEM 2013: Theory and Practice of Computer Science
Subtitle of host publication39th International Conference on Current Trends in Theory and Practice of Computer Science, Spindleruv Mlýn, Czech Republic, January 26-31, 2013. Proceedings
EditorsPeter van Emde Boas , Frans C. A. Groen , Giuseppe F. Italiano , Jerzy Nawrocki , Harald Sack
PublisherSpringer
Pages207-219
Number of pages13
ISBN (Electronic)978-3-642-35843-2
ISBN (Print)978-3-642-35842-5
DOIs
Publication statusPublished - 2013
Externally publishedYes
Event39th International Conference on Current Trends in Theory and Practice of Computer Science - Špindlerův Mlýn, Czech Republic
Duration: 26 Jan 201331 Jan 2013
http://www.sofsem.cz/sofsem13/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume7741
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference39th International Conference on Current Trends in Theory and Practice of Computer Science
Abbreviated titleSOFSEM 2013
CountryCzech Republic
CityŠpindlerův Mlýn
Period26/01/1331/01/13
Internet address

Fingerprint

Assertion
Object-oriented
Completeness
First-order
Auxiliary Variables
Natural number
Quantification
Range of data
Object
Class
Standards
Language
Interpretation

Cite this

Gouw, S. D., Boer, F. S. D., Ahrendt, W., & Bubel, R. (2013). Weak Arithmetic Completeness of Object-Oriented First-Order Assertion Networks. In P. V. E. B., F. C. A. G., G. F. I., J. N., & H. S. (Eds.), SOFSEM 2013: Theory and Practice of Computer Science: 39th International Conference on Current Trends in Theory and Practice of Computer Science, Spindleruv Mlýn, Czech Republic, January 26-31, 2013. Proceedings (pp. 207-219). (Lecture Notes in Computer Science; Vol. 7741). Springer. https://doi.org/10.1007/978-3-642-35843-2_19
Gouw, Stijn de ; Boer, Frank S. de ; Ahrendt, Wolfgang ; Bubel, Richard. / Weak Arithmetic Completeness of Object-Oriented First-Order Assertion Networks. SOFSEM 2013: Theory and Practice of Computer Science: 39th International Conference on Current Trends in Theory and Practice of Computer Science, Spindleruv Mlýn, Czech Republic, January 26-31, 2013. Proceedings. editor / Peter van Emde Boas ; Frans C. A. Groen ; Giuseppe F. Italiano ; Jerzy Nawrocki ; Harald Sack. Springer, 2013. pp. 207-219 (Lecture Notes in Computer Science).
@inproceedings{8cce2acc511243128e4574affd134e2c,
title = "Weak Arithmetic Completeness of Object-Oriented First-Order Assertion Networks",
abstract = "We present a completeness proof of the inductive assertion method for object-oriented programs extended with auxiliary variables. The class of programs considered are assumed to compute over structures which include the standard interpretation of Presburger arithmetic. Further, the assertion language is first-order, i.e., quantification only ranges over basic types like that of the natural numbers, Boolean and Object.",
author = "Gouw, {Stijn de} and Boer, {Frank S. de} and Wolfgang Ahrendt and Richard Bubel",
year = "2013",
doi = "10.1007/978-3-642-35843-2_19",
language = "English",
isbn = "978-3-642-35842-5",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "207--219",
editor = "{Peter van Emde Boas} and {Frans C. A. Groen} and {Giuseppe F. Italiano} and {Jerzy Nawrocki} and {Harald Sack}",
booktitle = "SOFSEM 2013: Theory and Practice of Computer Science",

}

Gouw, SD, Boer, FSD, Ahrendt, W & Bubel, R 2013, Weak Arithmetic Completeness of Object-Oriented First-Order Assertion Networks. in PVEB, FCAG, GFI, JN & HS (eds), SOFSEM 2013: Theory and Practice of Computer Science: 39th International Conference on Current Trends in Theory and Practice of Computer Science, Spindleruv Mlýn, Czech Republic, January 26-31, 2013. Proceedings. Lecture Notes in Computer Science, vol. 7741, Springer, pp. 207-219, 39th International Conference on Current Trends in Theory and Practice of Computer Science, Špindlerův Mlýn, Czech Republic, 26/01/13. https://doi.org/10.1007/978-3-642-35843-2_19

Weak Arithmetic Completeness of Object-Oriented First-Order Assertion Networks. / Gouw, Stijn de; Boer, Frank S. de; Ahrendt, Wolfgang; Bubel, Richard.

SOFSEM 2013: Theory and Practice of Computer Science: 39th International Conference on Current Trends in Theory and Practice of Computer Science, Spindleruv Mlýn, Czech Republic, January 26-31, 2013. Proceedings. ed. / Peter van Emde Boas; Frans C. A. Groen; Giuseppe F. Italiano; Jerzy Nawrocki; Harald Sack. Springer, 2013. p. 207-219 (Lecture Notes in Computer Science; Vol. 7741).

Research output: Chapter in Book/Report/Conference proceedingConference article in proceedingAcademicpeer-review

TY - GEN

T1 - Weak Arithmetic Completeness of Object-Oriented First-Order Assertion Networks

AU - Gouw, Stijn de

AU - Boer, Frank S. de

AU - Ahrendt, Wolfgang

AU - Bubel, Richard

PY - 2013

Y1 - 2013

N2 - We present a completeness proof of the inductive assertion method for object-oriented programs extended with auxiliary variables. The class of programs considered are assumed to compute over structures which include the standard interpretation of Presburger arithmetic. Further, the assertion language is first-order, i.e., quantification only ranges over basic types like that of the natural numbers, Boolean and Object.

AB - We present a completeness proof of the inductive assertion method for object-oriented programs extended with auxiliary variables. The class of programs considered are assumed to compute over structures which include the standard interpretation of Presburger arithmetic. Further, the assertion language is first-order, i.e., quantification only ranges over basic types like that of the natural numbers, Boolean and Object.

UR - https://link.springer.com/book/10.1007/978-3-642-35843-2

U2 - 10.1007/978-3-642-35843-2_19

DO - 10.1007/978-3-642-35843-2_19

M3 - Conference article in proceeding

SN - 978-3-642-35842-5

T3 - Lecture Notes in Computer Science

SP - 207

EP - 219

BT - SOFSEM 2013: Theory and Practice of Computer Science

A2 - , Peter van Emde Boas

A2 - , Frans C. A. Groen

A2 - , Giuseppe F. Italiano

A2 - , Jerzy Nawrocki

A2 - , Harald Sack

PB - Springer

ER -

Gouw SD, Boer FSD, Ahrendt W, Bubel R. Weak Arithmetic Completeness of Object-Oriented First-Order Assertion Networks. In PVEB, FCAG, GFI, JN, HS, editors, SOFSEM 2013: Theory and Practice of Computer Science: 39th International Conference on Current Trends in Theory and Practice of Computer Science, Spindleruv Mlýn, Czech Republic, January 26-31, 2013. Proceedings. Springer. 2013. p. 207-219. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-35843-2_19