A VDM CASE-STUDY IN MURAL

被引：4

作者：

FIELDS, B ^{[1
]}

ELVANGGORANSSON, M ^{[1
]}

机构：

[1] UNIV OSLO, DEPT INFORMAT, OSLO 3, NORWAY

来源：

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING | 1992年 / 18卷 / 04期

关键词：

FORMAL METHODS; STEPWISE REFINEMENT; SPECIFICATION SUPPORT; VERIFICATION SUPPORT; THEOREM PROVING;

D O I：

10.1109/32.129217

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

This paper describes the application of an interactive theorem-proving assistant and specification support tool called mural in the specification and verification of a small VDM development. The paper's intention is to give a feel for how mural works and of mural's applicability as a tool in specifying and verifying software.

引用

页码：279 / 295

页数：17

共 21 条

[1] A LOGIC COVERING UNDEFINEDNESS IN PROGRAM PROOFS [J].

BARRINGER, H ;

CHENG, JH ;

JONES, CB .

ACTA INFORMATICA, 1984, 21 (03) :251-269

[2] THE APPLICATION OF FORMAL METHODS TO THE ASSESSMENT OF HIGH INTEGRITY SOFTWARE [J].

BLOOMFIELD, RE ;

FROOME, PKD .

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1986, 12 (09) :988-993

[3]

CHENG JH, 1990, 3RD P REF WORKSH

[4]

DAHL OJ, 1986, 106 U OSL DEP INF RE

[5]

GARLAND SJ, 1990, P IFIP TC2 WORKING C

[6]

GORDON M, 1979, LECTURE NOTES COMPUT, V78

[7]

GORDON M, 1985, 68 U CAMBR COMP LAB

[8]

HARPER R, 1987, P S LOGIC COMPUTER S

[9]

Jones C. B., 1990, SYSTEMATIC SOFTWARE, V2

[10]

Jones C. B., 1991, FORMAL DEV SUPPORT S

← 1 2 3 →