A Sound and Complete Program Logic for Eiffel

被引：0

作者：

Nordio, Martin ^{[1
]}

Calcagno, Cristiano ^{[2
]}

Mueller, Peter ^{[1
]}

Meyer, Bertrand ^{[1
]}

机构：

[1] ETH, Zurich, Switzerland

[2] Imperial Coll, London, England

来源：

OBJECTS, COMPONENTS, MODELS AND PATTERNS, PROCEEDINGS | 2009年 / 33卷

关键词：

Software verification; program proofs; operational semantics; Eiffel; VERIFICATION; INVARIANTS; !text type='JAVA']JAVA[!/text;

D O I：

暂无

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

Object-oriented languages provide advantages such as reuse and modularity, but they also raise new challenges for program verification. Program logics have been developed for languages such as C# and Java. However, these logics do not cover the specifics of the Eiffel language. This paper presents a program logic for Eiffel that handles exceptions, once routines, and multiple inheritance. The logic is proven sound and complete w.r.t. an operational semantics. Lessons oil language design learned from the experience are discussed.

引用

页码：195 / +

页数：3

共 23 条

[1]

[Anonymous], 1997, Object-oriented software construction

[2]

[Anonymous], 2002, LICS

[3]

Banerjee A, 2008, LECT NOTES COMPUT SC, V5142, P387, DOI 10.1007/978-3-540-70592-5_17

[4] A Program Logic for Bytecode [J].

Bannwart, Fabian ;

Mueller, Peter .

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 141 (01) :255-273

[5]

Distefano D, 2008, OOPSLA 2008 NASHVILLE, CONFERENCE PROCEEDINGS, P213

[6]

Huisman M, 2000, LECT NOTES COMPUT SC, V1783, P284

[7]

Kassios IT, 2006, LECT NOTES COMPUT SC, V4085, P268

[8]

Leino KRM, 2005, LECT NOTES COMPUT SC, V3582, P26

[9]

MEYER B, 2006, ECMA367 ISO

[10]

*MOBIUS CONS, 2006, DEL 3 1 BYT COD LEV

← 1 2 3 →