CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Weak Arithmetic Completeness of Object-Oriented First-Order Assertion Networks

Stijn de Gouw ; Frank de Boer ; Wolfgang Ahrendt (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Richard Bubel
39th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2013) (0302-9743). 7741, p. 207-219. (2013)
[Konferensbidrag, refereegranskat]

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.


Lecture Notes in Computer Science, Springer-Verlag



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2013-12-21. Senast ändrad 2017-11-29.
CPL Pubid: 190349