期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

A development calculus for specifications 被引量：3

A development calculus for specifications
原文传递
导出
摘要 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. 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.
作者 李未
机构地区 State Key Laboratory of Software Development Environment
出处 《Science in China(Series F)》 2003年第5期390-400,共11页 中国科学（F辑英文版）
关键词 SPECIFICATION REVISION necessary premise R-calculus R-condition. specification, revision, necessary premise, R-calculus, R-condition.
分类号 TP311.5 [自动化与计算机技术—计算机软件与理论]
  • 相关文献

参考文献12

  • 1[1]Burstall, R. M., Goguen, J. A., Putting theories together to make specifications, Proc. 5th. IJCAI, Cambridge, Mass, Los Altos: William Kaufmann, 1977, 1045-1058.
  • 2[2]Bjorner, D., Jones, C., Formal Specification and Software Development, New York: Prentice Hall International, 1983.
  • 3[3]Nordstrom, B., Smith, J., Propositions and specifications of programs in Martin-Lof's type theory, BIT,1984, 24: 288-301.
  • 4[4]Sannella, D., Tarlecki, A., Toward formal development of programs from algebraic specifications: implementations revisited, Acta Informatica, 1988, 25: 233-281.
  • 5[5]Gallier, J.H., Logic for Computer Science, Foundations of Automatic Theorem Proving, New York: John Wiley & Sons, 1987, 147-158, 162-163, 197-217.
  • 6[6]Paulson, L., Logic and Computations, Cambridge: Cambridge University Press, 1987, 38-50.
  • 7[7]Flew, A., A Dictionary of Philosophy, London: Pan Books Ltd, 1979.
  • 8[8]Burgess, F., Handbook of Mathematical Logic (ed. Barwise, J.), Amsterdam: North-Holland Publishing Company, 1977.
  • 9[9]Alchourrón, C.E., Gardenfors, R., Makinson, D., On the logic of theory change: partial meet contraction and revision functions, The Journal of Symbolic Logic, 1985, 50(2): 510-530.
  • 10[10]Li, W., An open logic system, Science in China, Series A, 1993, 36: 362-375.

同被引文献4

引证文献3

二级引证文献12

Science in China(Series F)
2003年 第5期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部