Skip to main content
SpringerLink
Log in

The expressive theory of stacks

  • Published:
Acta Informatica Aims and scope Submit manuscript

Summary

The usual theory of stacks is not expressive in the sense of Cook; that is, loop invariants needed to prove programs that use stacks cannot be stated in the logic. We first prove this assertion, then suggest ways of augmenting theories with new operators so as to achieve expressiveness. The main technique is to regard data types as function spaces. The technique is applied to stacks as well as to other data types.

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. Clarke, E.M.: Programming language constructs for which it is impossible to obtain good Hoare axiom systems. J. ACM 26, 129–147

  2. Clarke, E.M.: The characterization problem for Hoare logics. In: Mathematical Logic and Programming Languages (C.A.R. Hoare, J.C. Shepherdson, eds.), pp. 89–106. Englewood Cliffs, N.J.: Prentice-Hall 1985

    Google Scholar 

  3. Clarke, E.M., German, S., Halpern, J.: Effective Axiomatizations of Hoare Logics. J. ACM 30, 612–636 (1983)

    Google Scholar 

  4. Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7, 70–90 (1978)

    Google Scholar 

  5. Guttag, J., Horowitz, E., Musser, D.: Abstract Data Types and Software Validation. Commun. ACM 21, 1048–1064 (1978)

    Google Scholar 

  6. Hoare, C.A.R.: An Axiomatic Basis for Computer Programming. Commun. ACM 12, 576–581, 583 (1969)

    Google Scholar 

  7. Hoare, C.A.R.: Proof of Correctness of Data Representations. Acta Inf. 1, 271–281 (1972)

    Google Scholar 

  8. Kamin, S.: Final Data Type Specifications. Proc. Seventh Annual Conf. on Principles of Programming Languages, pp. 131–138. Las Vegas, 1980

  9. Kamin, S.: Final Data Types and their Specification. ACM Trans. Prog. Lang. Syst. 5, 97–123 (1983)

    Google Scholar 

  10. Kamin, S., Jefferson, S., Archer, M.: The Role of Executable Specifications: The FASE System, Proc. IEEE Symp. on Application and Assessment of Automated Tools for Software Development, San Francisco, November 1983

  11. Kamin, S.: A FASE Specification of FP, Logics of Programs '85. LNCS 193. Berlin, Heidelberg, New York: Springer 1985

    Google Scholar 

  12. Lipton, R.J.: A Necessary and Sufficient Condition for the Existence of Hoare Logics. Proc. Eighteenth Symp. on Found. Comp. Sci., pp. 1–6, October 1977

  13. Majster, M.: Limits of the Algebraic Specification of Data Types. SIGPLAN Notices 12, 37–42 (1977)

    Google Scholar 

  14. Monk, J.D.: Mathematical Logic. Berlin, Heidelberg, New York: Springer 1976

    Google Scholar 

  15. Nelson, G.: Verifying Reachability Invariants of Linked Structures. Proc. Tenth Annual Conf. on Principles of Programming Languages, pp. 38–47, January 1983

  16. Wulf, W., London, R., Shaw, M.: An Introduction to the Construction and Verification of ALPHARD Programs. IEEE Trans. Software Eng. 2, 253–265 (1976)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, University of Illinois, Urbana, Illinois, USA

    Samuel Kamin

Authors
  1. Samuel Kamin
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Kamin, S. The expressive theory of stacks. Acta Informatica 24, 695–709 (1987). https://doi.org/10.1007/BF00282622

Download citation

  • Received:

  • Issue Date:

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

Keywords

Search

Navigation