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. © 2013 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
De Gouw, S., De Boer, F., Ahrendt, W., & Bubel, R. (2013). Weak arithmetic completeness of object-oriented first-order assertion networks. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7741 LNCS, pp. 207–219). https://doi.org/10.1007/978-3-642-35843-2_19
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
