Angelic nondeterminism in the unifying theories of programming

被引：17

作者：

Cavalcanti, Ana ^{[1
]}

Woodcock, Jim

Dunne, Steve

机构：

[1] Univ York, Dept Comp Sci, York YO10 5DD, N Yorkshire, England

[2] Univ Teesside, Sch Comp, Middlesbrough TS1 3BA, Cleveland, England

来源：

FORMAL ASPECTS OF COMPUTING | 2006年 / 18卷 / 03期

基金：

英国工程与自然科学研究理事会;

关键词：

semantics; refinement; relations; predicate transformers;

D O I：

10.1007/s00165-006-0001-8

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Hoare and He's unifying theories of programming (UTP) is a model of alphabetised relations expressed as predicates; it supports development in several programming paradigms. The aim of Hoare and He's work is the unification of languages and techniques, so that we can benefit from results in different contexts. In this paper, we investigate the integration of angelic nondeterminism in the UTP; we propose the unification of a model of binary multirelations, which is isomorphic to the monotonic predicate transformers model and can express angelic and demonic nondeterminism.

引用

页码：288 / 307

页数：20

共 24 条

[1]

Back R.-J., 1998, Refinement Calculus-A Systematic Introduction

[2]

BACK RJR, 1989, LECT NOTES COMPUT SC, V375, P139

[3] DUALITY IN SPECIFICATION LANGUAGES - A LATTICE-THEORETICAL APPROACH [J].

BACK, RJR ;

VONWRIGHT, J .

ACTA INFORMATICA, 1990, 27 (07) :583-625

[4] COMBINING ANGELS, DEMONS AND MIRACLES IN PROGRAM SPECIFICATIONS [J].

BACK, RJR ;

VONWRIGHT, J .

THEORETICAL COMPUTER SCIENCE, 1992, 100 (02) :365-383

[5]

Cavalcanti A., 2003, Formal Aspects of Computing, V15, P146, DOI 10.1007/s00165-003-0006-5

[6] A weakest precondition semantics for Z [J].

Cavalcanti, A ;

Woodcock, J .

COMPUTER JOURNAL, 1998, 41 (01) :1-15

[7]

CAVALCANTI ALC, 1999, FORM ASP COMPUT, V10, P267

[8]

CAVALCANTI ALC, 2005, ELECT NOTES THEORET, V137

[9]

CAVALCANTI ALC, 2002, LNCS, V2391, P471

[10]

CAVALCANTI ALC, 2004, ANGELIC NONDETERMINI

← 1 2 3 →