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

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

doi:10.1007/978-3-642-35843-2_19

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 proceeding › Conference Article in proceeding › Academic › peer-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 language	English
Title of host publication	SOFSEM 2013: Theory and Practice of Computer Science
Subtitle of host publication	39th International Conference on Current Trends in Theory and Practice of Computer Science, Spindleruv Mlýn, Czech Republic, January 26-31, 2013. Proceedings
Editors	Peter van Emde Boas , Frans C. A. Groen , Giuseppe F. Italiano , Jerzy Nawrocki , Harald Sack
Publisher	Springer
Pages	207-219
Number of pages	13
ISBN (Electronic)	978-3-642-35843-2
ISBN (Print)	978-3-642-35842-5
DOIs	https://doi.org/10.1007/978-3-642-35843-2_19
Publication status	Published - 2013
Externally published	Yes
Event	39th International Conference on Current Trends in Theory and Practice of Computer Science - Špindlerův Mlýn, Czech Republic Duration: 26 Jan 2013 → 31 Jan 2013 http://www.sofsem.cz/sofsem13/

Publication series

Series	Lecture Notes in Computer Science
Volume	7741
ISSN	0302-9743

Conference

Conference	39th International Conference on Current Trends in Theory and Practice of Computer Science
Abbreviated title	SOFSEM 2013
Country/Territory	Czech Republic
City	Špindlerův Mlýn
Period	26/01/13 → 31/01/13
Internet address	http://www.sofsem.cz/sofsem13/

Access to Document

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

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). Springer. https://doi.org/10.1007/978-3-642-35843-2_19

Gouw, Stijn de ; Boer, Frank S. de ; Ahrendt, Wolfgang et al. / 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, Vol. 7741).

@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",

address = "United States",

note = "39th International Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM 2013 ; Conference date: 26-01-2013 Through 31-01-2013",

url = "http://www.sofsem.cz/sofsem13/",

}

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. Springer, Lecture Notes in Computer Science, vol. 7741, 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 et al.
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 proceeding › Conference Article in proceeding › Academic › peer-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

T2 - 39th International Conference on Current Trends in Theory and Practice of Computer Science

Y2 - 26 January 2013 through 31 January 2013

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, Vol. 7741). doi: 10.1007/978-3-642-35843-2_19

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

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this