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.
, , , , ,
,
Springer
P. van Emde Boas , F.C.A. Groen , G.F. Italiano , J.R. Nawrocki , H. Sack
Lecture Notes in Computer Science
Highly Adaptable and Trustworthy Software using Forma Methods
Conference on Current Trends in Theory and Practice of Computer Science
Computer Security

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.