Journal of Computer Science and Technology

, Volume 8, Issue 1, pp 26–37 | Cite as

An introduction to INCAPS system

  • Li Renwei 
  • He Pei 
  • Zhang Wenhui 
Regular Papers


INCAPS, a subsystem of XYZ system, is an INteractive Computer-Assisted Proving System, The primary targets to develop it range from proving temporal logic formal theorem to verifying XYZ/SE program's correctness which are supported respectively by the mechanized logics—FOTL logic and Hoare-like proof system. This paper discusses five main topics concerning INCAPS system: the rules, implementation, tactics, forward proof and backward proof. It also gives several typical examples for demonstration of INCAPS' working principle. The achievement to data is that we have now accomplished successfully the verification of the hierarchical specification of AB protocol and the correctness of XYZ/SE program.


FOTL logic backward proof Hoare-like proof system XYZ/SE programs correctuess proof 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    McArthur, R. P., Tense Logic. D. Reidel Publishing Company, 1976.Google Scholar
  2. [2]
    Rescher, N. and Urquart, A., Temporal Logic. Springer-Verlag, 1971.Google Scholar
  3. [3]
    Li, R. W., N system: A natural temporal deduction systemChinese, Science Bulletin, 1989, 34 (5).Google Scholar
  4. [4]
    Li R. W., A natural deduction system of temporal logic.J. Computer Science and Technology, 1988, 3 (3), 173–185.CrossRefGoogle Scholar
  5. [5]
    Li, R. W., INCAPS: An interactive computer aided proving system.Chinese Journal of Computers, 1989, 12 (12).Google Scholar
  6. [6]
    Szalas, A., Concerning the semantic consequence relation in first-order temporal logic.Theoretical Computer Science, 1986, 47 (3).Google Scholar
  7. [7]
    Kroger, F., Temporal Logic of Programs Springer-Verlag, 1987.Google Scholar
  8. [8]
    Gordon, M., Milner al., A Metalanguage for Interactive Proof in LCF Conf Record of the Fifth Annual ACM Symp. Principles of Programming Language, 1978.Google Scholar
  9. [9]
    Schmidt, D. A., A programming notation for tactical reasoning. Seventh Conf. Automated Deduction Springer LNCS 170, 1984, 445–459.Google Scholar
  10. [10]
    He Pei, Proof strategies and validity.Journal of Software (in Chinese), 1991, 2 (4), 23–30.MathSciNetGoogle Scholar
  11. [11]
    Tang, C. S., XYZ: A Program Development Environment Based on Temporal Logic. Programming Languages and System Design (J. Bormann Ed.) 1983.Google Scholar
  12. [12]
    Tang, C. S., An Introduction to XYZ System. Techn. Rept. IS-CAS-XYZ-88-1, 1988.Google Scholar
  13. [13]
    Miao X and Tang, C. S., A methodology and an environment for stepwise refinement—according to design decisions.Journal of Software (in Chinese), 1990, 1 (3), 15–28.Google Scholar
  14. [14]
    Xie, H. H., A Structured Temporal Logic Language: XYZ/SE and Its Verification. Techn. Rept. IS-CAS-XYZ-88-3, 1988.Google Scholar
  15. [15]
    Gordon, M. J. C., Milner, R. and Wadsworth, C. P., Edinburgh LCF: A Mechanized Logic of Computation. LNCS 78, Springer-Verlag, 1979.Google Scholar
  16. [16]
    Paulson, L. C., Interactive Theorem Proving with Cambridge LCF, A user's Manual. Techn. Rept. No. 80, Computer Laboratory, Univ. of Cambridge, 1985.Google Scholar

Copyright information

© Science Press, Beijing China and Allerton Press Inc. 1993

Authors and Affiliations

  • Li Renwei 
    • 1
  • He Pei 
    • 1
  • Zhang Wenhui 
    • 1
  1. 1.Institute of SoftwareAcademia SinicaBeijing

Personalised recommendations