Weak Arithmetic Completeness of Object-Oriented First-Order Assertion Networks
Presented at the Conference on Current Trends in Theory and Practice of Computer Science, Špindlerův Mlýn
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.
|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)|
|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|
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.