Skip to main content
SpringerLink
Log in

Predicative programming — A survey

  • Conference paper
  • First Online:
Formal Methods in Programming and Their Applications

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

Abstract

The idea of using a predicate to specify behaviour is a compelling one, and leads to a desire to refine specifications into implementations in languages whose semantics have also been specified with predicates.

Many of us believe we share a common intuition about what a specification phrased as a predicate means. It may be surprising to learn that there are several ways to interpret a predicate as a specification. Under these interpretations, the same predicate can specify different behaviour. This paper examines three simple styles of specification using predicates.

The author is supported by DSTO Australia.

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. Bear, S., Rush, T.: Rigorous software engineering: A method for preventing software defects. HP J. 42 (1991) 24–31

    Google Scholar 

  2. Gordon, M.: Why higher-order logic is a good formalism for specifying and verifying hardware. In Milne, G., Subrahmanyam, P. (eds), Proceedings of the 1985 Edinburgh Workshop on VLSI Design: Formal Aspects of VLSI Design, Edinburgh, Scotland (1985). North Holland, Amsterdam, The Netherlands 153–177

    Google Scholar 

  3. Gordon, M.: Mechanizing programming logics in higher-order logic. In Birtwistle, G., Subrahmanyam, P. (eds), Current Trends in Hardware Verification and Automated Theorem Proving (Proceedings of the 1988 Banff Workshop on Hardware Verification), Banff, Canada (1988). Springer-Verlag, Berlin, Germany 387–439

    Google Scholar 

  4. Gravell, A.: Constructive refinement of first-order specifications. In Jones et al. [11] 181–210

    Google Scholar 

  5. Grundy, J.: A window inference tool for refinement. In Jones et al. [11] 230–254

    Google Scholar 

  6. Grundy, J.: A three-valued logic for refinement. In Sabelfeld, V. (ed.), Proceedings of the International Conference on Formal Methods in Programming and Their Applications, Lecture Notes in Computer Science, Novosibirsk, Russia (1993). Springer-Verlag, Berlin, Germany

    Google Scholar 

  7. Hayes, I.: Specification Case Studies. Prentice Hall International Series in Computer Science. Prentice Hall International, London, England (1987)

    Google Scholar 

  8. Hehner, E.: Predicative programming — part 1. Commun. ACM 27 (1984) 134–143

    Google Scholar 

  9. Hehner, E.: Termination conventions and comparative semantics. Acta Inf. 25 (1988) 1–14

    Google Scholar 

  10. Hoare, C.: Programs are predicates. Trans. Royal Society — A 312 (1984) 475–490

    Google Scholar 

  11. Jones, C., et al. (eds). Proceedings of the 5th Refinement Workshop, Workshops in Computer Science, Lloyd's Register, London, England (1992). BCS-FACS, Springer-Verlag, London, England

    Google Scholar 

  12. Mili, A.: A relational approach to the design of deterministic programs. Acta Inf. 20 (1983) 315–328

    Google Scholar 

  13. Morgan, C.: Data refinement by miracles. Inf. Process. Lett. 26 (1988) 243–246

    Google Scholar 

  14. Neilson, D.: From Z to C.: Illustration of a rigorous development method. Technical Monograph PRG-101, Oxford University Computing Laboratory, Programming Research Group, 8–11 Keble Road, Oxford OX1 3QD, England (1990)

    Google Scholar 

  15. Nelson, G.: A generalization of Dijkstra's calculus. ACM Trans. Programming Languages & Syst. 11 (1989) 517–561

    Google Scholar 

  16. Nguyen, T.: A relational model of demonic nondeterministic programs. J. Foundations Comput. Sci. 2 (1991) 101–131

    Google Scholar 

  17. Parnas, D.: Technical correspondence: Predicative programming. Commun. ACM 28 (1985) 354–356

    Google Scholar 

  18. Sekerinski, E.: A calculus for predicative programming. In Woodcock, J., et al. (eds), Proceedings of the 2nd Mathematics of Program Construction Conference, Lecture Notes in Computer Science, Oxford University, Oxford, England (1992). Springer-Verlag, Berlin, Germany

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Laboratory, University of Cambridge, New Museums Site, Pembroke Street, CB2 3QG, Cambridge, England

    Jim Grundy

Authors
  1. Jim Grundy
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Dines Bjørner Manfred Broy Igor V. Pottosin

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Grundy, J. (1993). Predicative programming — A survey. In: Bjørner, D., Broy, M., Pottosin, I.V. (eds) Formal Methods in Programming and Their Applications. Lecture Notes in Computer Science, vol 735. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0039697

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-57316-6

  • Online ISBN: 978-3-540-48056-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation