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

SeriesLecture Notes in Computer Science
Volume7741
ISSN0302-9743

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

Cite this