Skip to main content
SpringerLink
Log in

Remarks on the impact of program verification on language design

  • Section V - Workshop Position Papers
  • Conference paper
  • First Online:
Design and Implementation of Programming Languages

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 54))

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ambler, A. L., D. I. Good, J. C. Browne, W. F. Burger, R. M. Cohen, C. G. Hoch, and R. E. Wells, "Gypsy: A Language for Specification and Implementation of Verifiable Programs," Proceedings of Language Design for Reliable Software, 1977 (to appear).

    Google Scholar 

  2. Brinch Hansen, P., "The Programming Language Concurrent Pascal," IEEE Transactions on Software Engineering, Vol. SE-1, No. 2, June 1975, pp. 199–207.

    Google Scholar 

  3. Conway, R., "PL/CS—A Highly Disciplined Subset of PL/C," SIGPLAN Notices, Vol. 11, No. 12, December 1976, pp. 21–24. Also Cornell University Technical Report TR76-273, March 1976.

    Google Scholar 

  4. Dijkstra, E. W., "Correctness Concerns and, Among Other Reasons, Why They Are Resented," Proceedings of the International Conference on Reliable Software, 1975, pp. 546–550. Also SIGPLAN Notices, Vol. 10, No. 6, June 1975.

    Google Scholar 

  5. Dijkstra, E. W., "Guarded Commands, Nondeterminacy and Formal Derivation of Programs," Communications of ACM, Vol. 18, No. 8, August 1975, pp. 453–457.

    Google Scholar 

  6. Guttag, J. V., J. J. Horning, and R. L. London, A Proof Rule for Euclid Procedures, 1977 (submitted for publication).

    Google Scholar 

  7. Hoare, C.A.R., "Proof of Correctness of Data Representations," Acta Information, Vol. 1, No. 4, 1972, pp. 271–281.

    Google Scholar 

  8. Jensen, K., and N. Wirth, PASCAL User Manual and Report, Lecture Notes in Computer Science, Vol. 18, G. Goos and J. Hartmanis, (eds.), Springer-Verlag, 1974.

    Google Scholar 

  9. Lampson, B. W., J. J. Horning, R. L. London, J. G. Mitchell, and G. J. Popek, "Report on the Programming Language Euclid," SIGPLAN Notices, 1977 (to appear).

    Google Scholar 

  10. Liskov, B., A. Snyder, R. Atkinson, and C. Shaffert, "Abstraction Mechanisms in Clu," Proceedings of Language Design for Reliable Software, 1977 (to appear). Also MIT Computation Structures Group Memo 144, October 1976.

    Google Scholar 

  11. London, R. L., M. Shaw, and W. A. Wulf, Abstraction and Verification in Alphard: A Symbol Table Example, Carnegie-Mellon University and USC Information Sciences Institute Technical Reports, 1976.

    Google Scholar 

  12. London, R. L., J. V. Guttag, J. J. Horning, B. W. Lampson, J. G. Mitchell, and G. J. Popek, Proof Rules for the Programming Language Euclid, 1977.

    Google Scholar 

  13. Popek, G. J., J. J. Horning, B. W. Lampson, R. L. London, and J. G. Mitchell, "Some Design Issues in Euclid" (working title), Proceedings of Language Design for Reliable Software, 1977 (to appear).

    Google Scholar 

  14. Shaw, M., "Abstraction and Verification in Alphard: Design and Verification of a Tree Handler," Proceedings of Fifth Texas Conference on Computing Systems, 1976, pp. 86–94. Also Carnegie-Mellon University Technical Report, 1976.

    Google Scholar 

  15. Shaw, M., W. A. Wulf, and R. L. London, Abstraction and Verification in Alphard: Iteration and Generators, Carnegie-Mellon University and USC Information Sciences Institute Technical Reports, 1976. Also Communications of ACM (to appear).

    Google Scholar 

  16. Wulf, W. A., R. L. London, and M. Shaw, Abstraction and Verification in Alphard: Introduction to Language and Methodology, Carnegie-Mellon University and USC Information Sciences Institute Technical Reports, 1976.

    Google Scholar 

  17. Wulf, W. A., R. L. London, and M. Shaw, "An Introduction to the Construction and Verification of Alphard Programs," IEEE Transactions on Software Engineering, Vol. SE-2, No. 4, December 1976, pp. 253–265.

    Google Scholar 

  18. Wulf, W. A., M. Shaw, and R. L. London, "Achieving Quality Software: Reflections on the Aims and Objectives of Alphard," Computer Science Research Review 1975–76, Carnegie-Mellon University, pp. 7–15.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. USC Information Sciences Institute, USA

    Raiph L. London

Authors
  1. Raiph L. London
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

John H. Williams David A. Fisher

Rights and permissions

Reprints and permissions

Copyright information

© 1977 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

London, R.L. (1977). Remarks on the impact of program verification on language design. In: Williams, J.H., Fisher, D.A. (eds) Design and Implementation of Programming Languages. Lecture Notes in Computer Science, vol 54. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0021429

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-08360-3

  • Online ISBN: 978-3-540-37260-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation