Skip to main content
SpringerLink
Log in

An introduction to INCAPS system

  • Regular Papers
  • Published:
Journal of Computer Science and Technology Aims and scope Submit manuscript

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. McArthur, R. P., Tense Logic. D. Reidel Publishing Company, 1976.

  2. Rescher, N. and Urquart, A., Temporal Logic. Springer-Verlag, 1971.

  3. Li, R. W., N system: A natural temporal deduction systemChinese, Science Bulletin, 1989, 34 (5).

  4. Li R. W., A natural deduction system of temporal logic.J. Computer Science and Technology, 1988, 3 (3), 173–185.

    Article  Google Scholar 

  5. Li, R. W., INCAPS: An interactive computer aided proving system.Chinese Journal of Computers, 1989, 12 (12).

  6. Szalas, A., Concerning the semantic consequence relation in first-order temporal logic.Theoretical Computer Science, 1986, 47 (3).

  7. Kroger, F., Temporal Logic of Programs Springer-Verlag, 1987.

  8. Gordon, M., Milner R.et al., A Metalanguage for Interactive Proof in LCF Conf Record of the Fifth Annual ACM Symp. Principles of Programming Language, 1978.

  9. Schmidt, D. A., A programming notation for tactical reasoning. Seventh Conf. Automated Deduction Springer LNCS 170, 1984, 445–459.

    Google Scholar 

  10. He Pei, Proof strategies and validity.Journal of Software (in Chinese), 1991, 2 (4), 23–30.

    MathSciNet  Google Scholar 

  11. Tang, C. S., XYZ: A Program Development Environment Based on Temporal Logic. Programming Languages and System Design (J. Bormann Ed.) 1983.

  12. Tang, C. S., An Introduction to XYZ System. Techn. Rept. IS-CAS-XYZ-88-1, 1988.

  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. Xie, H. H., A Structured Temporal Logic Language: XYZ/SE and Its Verification. Techn. Rept. IS-CAS-XYZ-88-3, 1988.

  15. Gordon, M. J. C., Milner, R. and Wadsworth, C. P., Edinburgh LCF: A Mechanized Logic of Computation. LNCS 78, Springer-Verlag, 1979.

  16. Paulson, L. C., Interactive Theorem Proving with Cambridge LCF, A user's Manual. Techn. Rept. No. 80, Computer Laboratory, Univ. of Cambridge, 1985.

Download references

Author information

Authors and Affiliations

  1. Institute of Software, Academia Sinica, 100080, Beijing

    Li Renwei, He Pei & Zhang Wenhui

Authors
  1. Li Renwei
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. He Pei
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Zhang Wenhui
    View author publications

    You can also search for this author in PubMed Google Scholar

Additional information

This project is supported by the National Natural Science Foundation of China.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Li, R., He, P. & Zhang, W. An introduction to INCAPS system. J. of Comput. Sci. & Technol. 8, 26–37 (1993). https://doi.org/10.1007/BF02946583

Download citation

  • Received:

  • Revised:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF02946583

Keywords

Search

Navigation