A type model for VDM

  • B. Q. Monahan
Foundations I
Part of the Lecture Notes in Computer Science book series (LNCS, volume 252)


A model of types for use in VDM specifications is presented. Standard VDM types consisting of finitary values are given set-theoretic denotations, restricting the use of Scott domain theory to the provision of types for the continuous functions and Bekic mappings. An objective of this work was to give a simple account of recursively defined data types not involving the full apparatus surrounding the use of Scott domain theory. To do this, various “type universes” are introduced axiomatically for use as semantic denotation spaces for type expressions. Basic constructions of these universes are given to show that these axiomatic requirements can be satisfied. As these type universes indirectly specify the “values” that each type consists of, it also gives a framework for building a full semantic model of VDM.


Proof Obligation Type Expression Type Definition Denotational Semantic Smash Product 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Bjorner,Jones]
    D.Bjorner, C.B.Jones, Formal Specification and Software Development, Prentice Hall, 1982Google Scholar
  2. [Blikle]
    A.Blikle, A metalanguage for Naive Denotational Semantics, Progetto Finalizzato Informatica, C.N.R. Progetto Pl CNET 104, Pisa, 1984.Google Scholar
  3. [Cohn]
    P.M.Cohn, Universal Algebra, D.Reidel Pub. Co., 1980.Google Scholar
  4. [Devlin]
    K.J.Devlin, Fundamentals of Contemporary Set Theory, Universitext, Springer-Verlag, 1979.Google Scholar
  5. [Enderton]
    H.Enderton, Elements of Set Theory Academic Press, 1975Google Scholar
  6. [Goldblatt]
    R. Goldblatt, Topoi: The Categorical Analysis of Logic, Studies in Logic, Vol 98, North Holland Pub. Co., Amsterdam, 1979Google Scholar
  7. [Halmos]
    P.Halmos, Naive Set Theory, Springer-Verlag, 1979Google Scholar
  8. [Jones]
    C.B.Jones, Systematic Software Development using VDM, Prentice Hall, 1986Google Scholar
  9. [Monahan]
    B.Q.Monahan, A type model for VDM, Internal technical report, STL Ltd/University of Manchester, July 1984Google Scholar
  10. [Milner]
    R. Milner, A theory of type polymorphism in programming, J.Computer and System Sciences, Vol 17, p348–375, 1978.Google Scholar
  11. [Schmidt]
    D.A.Schmidt, Denotational Semantics: A methodology for language development, Allyn and Bacon, 1986Google Scholar
  12. [Scott]
    D.S.Scott, Domains for Denotational Semantics, ICALP' 82, Aarhus, Denmark, July, 1982Google Scholar
  13. [Stoy]
    J.E.Stoy, Denotational Semantics, The MIT Press, 1977Google Scholar
  14. [Winskel,Larsen]
    G.Winskel, K.G.Larsen, Using Information Systems to solve Recursive Domain Equations effectively Technical report 51, University of Cambridge Computer Laboratory, 1985.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1987

Authors and Affiliations

  • B. Q. Monahan
    • 1
  1. 1.Imperial Software Technology Ltd.London

Personalised recommendations