THE DATE REFINEMENT CALCULATOR FOR Z-SPECIFICATIONS

被引：7

作者：

JOSEPHS, MB

机构：

[1] IBM, Yorktown Heights, NY, USA, IBM, Yorktown Heights, NY, USA

来源：

INFORMATION PROCESSING LETTERS | 1988年 / 27卷 / 01期

关键词：

COMPUTER PROGRAMMING - Theory;

D O I：

10.1016/0020-0190(88)90078-6

中图分类号：

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

学科分类号：

0812 ;

摘要：

Data refinement is applied to specifications of programs rather than programs themselves. In particular, the weakest (most general) specification of a concrete operation is calculated from the specification of the abstract operation and a posited relation between abstract and concrete values. The method presented is designed for specifications expressed in the Z language. Use is made of the weakest precondition of a specification. An example of data refinement calculation is presented. 11 refs.

引用

页码：29 / 33

页数：5

共 12 条

[1]

GRIES D, 1985, SIGPLAN NOTICES, V20, P131, DOI 10.1145/17919.806834

[2]

Hayes I. J, 1987, SPECIFICATION CASE S

[3]

Hoare C. A. R., 1986, Fundamenta Informaticae, V9, P217

[4]

Hoare C. A. R., 1972, Acta Informatica, V1, P271, DOI 10.1007/BF00289507

[5]

Hoare C. A. R., 1986, Fundamenta Informaticae, V9, P51

[6] PRESPECIFICATION IN DATA REFINEMENT [J].

HOARE, CAR ;

HE, J ;

SANDERS, JW .

INFORMATION PROCESSING LETTERS, 1987, 25 (02) :71-76

[7]

Jones C. B, 1980, SOFTWARE DEV RIGOROU

[8]

JONES CB, 1987, LECT NOTES COMPUT SC, V252, P260

[9]

JOSEPHS MB, 1986, FORMAL METHODS STEPW

[10] DATA REFINEMENT BY MIRACLES [J].

MORGAN, CC .

INFORMATION PROCESSING LETTERS, 1988, 26 (05) :243-246

← 1 2 →