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

被引：0

作者：

de Gouw, Stijn ^{[2
,3
]}

de Boer, Frank ^{[2
,3
]}

Ahrendt, Wolfgang ^{[1
]}

Bubel, Richard ^{[4
]}

机构：

[1] Chalmers Univ, Gothenburg, Sweden

[2] CWI, Amsterdam, Netherlands

[3] Leiden Univ, NL-2300 RA Leiden, Netherlands

[4] Tech Univ Darmstadt, Darmstadt, Germany

来源：

SOFSEM 2013: THEORY AND PRACTICE OF COMPUTER SCIENCE | 2013年 / 7741卷

关键词：

VERIFICATION;

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页码：207 / 219

页数：13