Specifying Imperative ML-Like Programs Using Dynamic Logic

被引：0

作者：

Maingaud, Severine ^{[1
,2
]}

Balat, Vincent ^{[1
,2
]}

Bubel, Richard ^{[3
]}

Haehnle, Reiner ^{[3
]}

Miquel, Alexandre ^{[4
]}

机构：

[1] CNRS, Lab Preuves Programmes & Syst, F-75700 Paris, France

[2] Univ Paris Diderot, Paris, France

[3] Chalmers Univ, Dept Comp Sci & Engn, Gothenburg, Sweden

[4] Univ Lyon, UCBL, CNRS, INRIA,LIP,UMR 5668,ENS Lyon, Lyon, France

来源：

FORMAL VERIFICATION OF OBJECT-ORIENTED SOFTWARE | 2011年 / 6528卷

关键词：

ML; dynamic logic; program specification; program verification; KeY; AF2;

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We present a logical system suited for specification and verification of imperative ML programs. The specification language combines dynamic logic (DL), explicit state updates and second-order functional arithmetic. Its proof system is based on a Gentzen-style sequent calculus (adapted to modal logic) with facilities for symbolic evaluation. We illustrate the system with some example, and give a full Kripke-style semantics in order to prove its correctness.

引用

页码：122 / +

页数：2

共 11 条

[1]

[Anonymous], LNCS LNAI

[2]

Balser M, 2000, LECT NOTES COMPUT SC, V1783, P363

[3]

Baro S, 2004, ANN NY ACAD SCI, V3085, P51

[4]

Chlipala A., 2009, ICFP 2009

[5]

Filliatre JC, 2003, 1366 LRI U PAR SUD

[6]

Harel D., 2000, Foundations of computing

[7] AN AXIOMATIC BASIS FOR COMPUTER PROGRAMMING [J].

HOARE, CAR .

COMMUNICATIONS OF THE ACM, 1969, 12 (10) :576-&

[8]

KANIG J, 2009, ACM SIGPLAN WORKSH M

[9]

Krivine J.L., 1993, LAMBDA CALCULUS TYPE

[10]

Régis-Gianas Y, 2008, LECT NOTES COMPUT SC, V5133, P305

← 1 2 →