Science in China Series F: Information Sciences

, Volume 46, Issue 5, pp 390–400 | Cite as

A development calculus for specifications

  • Li Wei 


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.


specification revision necessary premise R-calculus R-condition 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  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.Google Scholar
  2. 2.
    Bjørner, D., Jones, C., Formal Specification and Software Development, New York: Prentice Hall International, 1983.Google Scholar
  3. 3.
    Nordström, B., Smith, J., Propositions and specifications of programs in Martin-Löf’s type theory, BIT, 1984, 24: 288–301.MATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Sannella, D., Tarlecki, A., Toward formal development of programs from algebraic specifications: implementations revisited, Acta Informatica, 1988, 25: 233–281.MATHCrossRefMathSciNetGoogle Scholar
  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.Google Scholar
  6. 6.
    Paulson, L., Logic and Computations, Cambridge: Cambridge University Press, 1987, 38–50.Google Scholar
  7. 7.
    Flew, A., A Dictionary of Philosophy, London: Pan Books Ltd, 1979.Google Scholar
  8. 8.
    Burgess, F., Handbook of Mathematical Logic (ed. Barwise, J.), Amsterdam: North-Holland Publishing Company, 1977.Google Scholar
  9. 9.
    Alchourrón, C.E., Gärdenfors, 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.MATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Li, W., An open logic system, Science in China, Series A, 1993, 36: 362–375.MATHGoogle Scholar
  11. 11.
    Li, W., A logical framework for the evolution of specifications, ESOP’94, LNCS 788, Berlin: Springer-Verlag, 1994, 394–408.Google Scholar
  12. 12.
    Gärdenfors, P., Knowledge in Flux, Cambridge: The MIT Press, 1988.Google Scholar

Copyright information

© Science in China Press 2003

Authors and Affiliations

  • Li Wei 
    • 1
  1. 1.State Key Laboratory of Software Development EnvironmentBeihang UniversityBeijingChina

Personalised recommendations