A development calculus for specifications

被引：1

作者：

Wei Li

机构：

[1] Beihang University,State Key Laboratory of Software Development Environment

来源：

Science in China Series F: Information Sciences | 2003年 / 46卷

关键词：

specification; revision; necessary premise; R-calculus; R-condition;

D O I：

暂无

中图分类号：

学科分类号：

摘要：

A first order inference system, named R-calculus, is defined to develop the specifications. This system intends to eliminate the laws which are not consistent with users’ requirements. The R-calculus consists of the structural rules, an axiom, a cut rule, and the rules for logical connectives. Some examples are given to demonstrate the usage of the R-calculus. Furthermore, the properties regarding reachability and completeness of the R-calculus are formally defined and proved.

引用

页码：390 / 400

页数：10

共 8 条

[1]

Nordström B.(1984)Propositions and specifications of programs in Martin-Löf’s type theory BIT 24 288-301

[2]

Smith J.(1988)Toward formal development of programs from algebraic specifications: implementations revisited Acta Informatica 25 233-281

[3]

Sannella D.(1985)On the logic of theory change: partial meet contraction and revision functions The Journal of Symbolic Logic 50 510-530

[4]

Tarlecki A.(1993)An open logic system Science in China, Series A 36 362-375

[5]

Alchourrón C.E.(undefined)undefined undefined undefined undefined-undefined

[6]

Gärdenfors R.(undefined)undefined undefined undefined undefined-undefined

[7]

Makinson D.(undefined)undefined undefined undefined undefined-undefined

[8]

Li W.(undefined)undefined undefined undefined undefined-undefined

← 1 →