Advertisement

A generalization of Dijkstra’s calculus to typed program specifications

  • Klaus-Dieter Schewe
  • Bernhard Thalheim
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1684)

Abstract

Dijkstra’s predicate transformer calculus in its extended form gives an axiomatic semantics to program specifications including partiality and recursion. However, even the classical theory is based on infinitary first order logic which is needed to guarantee the existence of predicate transformers for weakest (liberal) preconditions. This theory can be generalized to higher-order intuitionistic logic.

Such logics can be interpreted in topoi. Then each topos E canonically corresponds to a definitionally complete theory T such that E is equivalent to the topos \( \mathbb{E}(T) \) (T) of definable types over T. Furthermore, each model of T in an arbitrary topos F canonically corresponds to a logical morphism \( \mathbb{E}(T) \to F \) (T) → F.

This correspondence enables the definition of a type specification discipline with a semantics based on topoi such that the predicate transformers in the associated logic give an axiomatic semantics for typed program specifications.

Keywords

Pairing Condition Intuitionistic Logic Full Proof Object Oriented Database Predicate Transformer 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    M. Barr, C. Wells: Category Theory for Computing Science, Prentice-Hall 1990Google Scholar
  2. 2.
    M. Barr, C. Wells: Toposes, Triples and Theories, Springer Grundlehren der mathematischen Wissenschaften 278, 1985Google Scholar
  3. 3.
    A. Boileau, A. Joyal: La Logique des Topos, Journal of Symbolic Logic, vol. 46(1), 1981, 6–16zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    K. B. Bruce, A. R. Meyer: The Semantics of Second Order Polymorphic Lambda Calculus, in G. Kahn, D. B. MacQueen, G. Plotkin (Eds.): Semantics of Data Types, Springer LNCS 173, 1984, pp. 131–144Google Scholar
  5. 5.
    P. Cousot: Methods and Logics for Proving Programs, in J. van Leeuwen (Ed.): The Handbookof Theoretical Computer Science, vol B: “Formal Models and Semantics”, Elsevier, 1990, pp. 841–993Google Scholar
  6. 6.
    E. W. Dijkstra, C. S. Scholten: Predicate Calculus and Program Semantics, Springer Texts and Monographs in Computer Science, 1989Google Scholar
  7. 7.
    H. Ehrig und B. Mahr: Fundamentals of Algebraic Specification 1, Springer EATCS Monographs, vol. 6, 1985Google Scholar
  8. 8.
    M. P. Fourman: The Logic of Topoi, in J. Barwise (Ed.): Handbookof Mathematical Logic, North-Holland Studies in Logic, vol. 90, 1977, pp. 1053–1090Google Scholar
  9. 9.
    J. A. Goguen: Types as Theories, Oxford University, 1990Google Scholar
  10. 10.
    R. Goldblatt: Topoi — The Categorial Analysis of Logic, North-Holland, Studies in Logic, vol. 98, 1984Google Scholar
  11. 11.
    P. Johnstone: Topos Theory, Academic Press, 1977Google Scholar
  12. 12.
    A. Kock, G. Reyes: Doctrines in Categorial Logic, in J. Barwise (Ed.): Handbook of Mathematical Logic, North-Holland Studies in Logic, vol. 90, 1977, pp. 283–313Google Scholar
  13. 13.
    S. Mac Lane: Categories for the Working Mathematician, Springer GTM, vol. 5, 1972Google Scholar
  14. 14.
    S. Mac Lane, I. Moerdijk: Sheaves in Geometry and Logic — A First Introduction to Topos Theory, Springer Universitext, 1992Google Scholar
  15. 15.
    J. C. Mitchell: Type Systems for Programming Languages, in J. van Leeuwen (Ed.): The Handbookof Theoretical Computer Science, vol B: “Formal Models and Semantics”, Elsevier, 1990, pp. 365–458Google Scholar
  16. 16.
    G. Nelson: A Generalization of Dijkstra’s Calculus, ACM TOPLAS, vol. 11(4), 1989, pp. 517–561CrossRefGoogle Scholar
  17. 17.
    J. C. Reynolds: Polymorphism is not Set-Theoretic, in G. Kahn, D. B. MacQueen, G. Plotkin (Eds.): Semantics of Data Types, Springer LNCS 173, 1984, pp. 145–156Google Scholar
  18. 18.
    K.-D. Schewe. Specification of Data-Intensive Application Systems. Habilitation Thesis. BTU Cottbus 1995. available from http://www.in.tu-clausthal.de/~schewe/public/habil.ps.gz
  19. 19.
    K.-D. Schewe, B. Thalheim. Fundamental Concepts of Object Oriented Databases. Acta Cybernetica vol. 11(4):49–84, 1993.zbMATHMathSciNetGoogle Scholar
  20. 20.
    K.-D. Schewe. Fundamentals of object oriented database modelling. ИНТеллеК-ТУалЪНЪΙ СИсТемЪΙ (Intelligent Systems). Moskau 1996.Google Scholar
  21. 21.
    K.-D. Schewe, B. Thalheim. Towards a Theory of Consistency Enforcement. Acta Informatica vol. 36(4): 97–141, 1999.zbMATHCrossRefMathSciNetGoogle Scholar
  22. 22.
    D. S. Scott: Identity and Existence in Intuitionistic Logic, in M. P. Fourman, C. J. Mulvey, D. S. Scott: Applications of Sheaves, Springer LNM, vol. 753, 1979, pp. 660–698Google Scholar
  23. 23.
    M. Wirsing: Algebraic Specification, in J. van Leeuwen (Ed.): The Handbookof Theoretical Computer Science, vol B: “Formal Models and Semantics”, Elsevier, 1990, pp. 675–788Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Klaus-Dieter Schewe
    • 1
  • Bernhard Thalheim
    • 2
  1. 1.Dept. of Computer ScienceTechnical University of ClausthalClausthal-ZellerfeldGermany
  2. 2.Dept. of Computer ScienceBrandenburgian Technical University at CottbusCottbusGermany

Personalised recommendations