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.
Additional Metadata
Keywords Inductive Assertion Method, Completeness, Expressiveness, Presburger Arithmetic, Auxiliary Variables, Object-Oriented
ACM Software/Program Verification (acm D.2.4), Specifying and Verifying and Reasoning about Programs (acm F.3.1)
THEME Software (theme 1)
Publisher Springer
Editor P. van Emde Boas , F.C.A. Groen , G.F. Italiano , J.R. Nawrocki , H. Sack
Series Lecture Notes in Computer Science
Project Highly Adaptable and Trustworthy Software using Forma Methods
Conference Conference on Current Trends in Theory and Practice of Computer Science
Citation
de Gouw, C.P.T, de Boer, F.S, Ahrendt, W, & Bubel, R. (2013). Weak Arithmetic Completeness of Object-Oriented First-Order Assertion Networks. In P van Emde Boas, F.C.A Groen, G.F Italiano, J.R Nawrocki, & H Sack (Eds.), SOFSEM 2013: Theory and Practice of Computer Science, 39th International Conference on Current Trends in Theory and Practice of Computer Science (pp. 207–219). Springer.