The Static Part of the Design Language COLD-K

  • Gerard R. Renardel de Lavalette
Conference paper
Part of the Workshops in Computing book series (WORKSHOPS COMP.)


This paper is about the static fragment of the design language COLD-K, obtained by dropping all dynamic features (procedures and expressions). It contains definitions of syntax and semantics, together with a presentation of the notions used in the definition of the semantics, such as MPL W (many-sorted partial infinitary logic), inductive definitions, the algebra of theories (with the operations renaming, import and export) and the type structure defined over this algebra.


Predicate Symbol Explicit Definition Module Algebra Semantic Domain Strong Normalisation 
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. [1]
    J.C.M. Baeten, J.A. Bergstra, S. Mauw, G.J. Veltink, A process specification formalism based on static COLD, in: J.A. Bergstra, L.M.G. Feijs (eds.) Algebraic methods: Theory, Tools and Applications (Part II), LNCS, Springer-Verlag, 1991.Google Scholar
  2. [2]
    H.P. Barendregt, The lambda calculus, its syntax and semantics (Revised edition), North-Holland, 1984.MATHGoogle Scholar
  3. [3]
    H. Barringer, J.H. Cheng, C.B. Jones, A logic covering undefinedness in program proofs, Acta Informatica 21 (1984) 251–269.MathSciNetMATHCrossRefGoogle Scholar
  4. [4]
    J.A. Bergstra, J. Heering, P. Klint, Module algebra, Journal of the ACM 37 (1990) 335–372.MathSciNetMATHCrossRefGoogle Scholar
  5. [5]
    J.H. Cheng, A Logic for Partial Functions, Ph.D. thesis, University of Manchester, Department of Computer Science, 1986 Technical Report UMCS–86–7–1.Google Scholar
  6. [6]
    M.E.A. Corthout, H.B.M. Jonkers, The transformational development of a new point containment algorithm, Philips Journal of Research 41 (1986), 83–174.MATHGoogle Scholar
  7. [7]
    M.E.A. Corthout, H.B.M. Jonkers, A new point containment algorithm for B-regions in the discrete plane, Proceedings of the Conference on Theoretical Foundations of Computer Graphics and CAD, Italy (1987).Google Scholar
  8. [8]
    L.M.G. Feijs, A formalisation of design methods, Ph.D. thesis, Technical University Eindhoven, 1990.Google Scholar
  9. [9]
    L.M.G. Feijs, H.B.M. Jonkers, Transformational design: an annotated example, Proceedings of the IFIP TC 2 Working Conference on Program Specification and Transformation, North-Holland (1986).Google Scholar
  10. [10]
    L.M.G. Feijs, H.B.M. Jonkers, Formal Specification and Design, Cambridge Tracts in Theoretical Computer Science 35, Cambridge University Press, 1992.MATHCrossRefGoogle Scholar
  11. [11]
    L.M.G. Feijs, H.B.M. Jonkers, C.P.J. Koymans, G.R. Renardel de Lavalette, Formal definition of the design language COLD-K, Technical Report, ESPRIT project 432, Doc.Nr. METEOR/t7/PRLE/7 (1987).Google Scholar
  12. [12]
    R. Groenboom, G.R. Renardel de Lavalette, Reasoning over dynamic features in specification languages,this volume.Google Scholar
  13. [13]
    D. Harel, Dynamic Logic, in: Handbook of Philosophical Logic, vol. II (D. Gabbay, F. Guenthner, eds.) Reidel (1984) 497–604.CrossRefGoogle Scholar
  14. [14]
    H.B.M. Jonkers, Inheritance in COLD, in: J.A. Bergstra, L.M.G. Feijs (eds.) Algebraic methods: Theory, Tools and Applications (Part II), LNCS, Springer-Verlag, 1991.Google Scholar
  15. [15]
    H.B.M. Jonkers, J.H. Obbink, COLD: a common object-oriented language for design, Working document, Philips Research Laboratories Eindhoven, 1983.Google Scholar
  16. [16]
    C.P.J. Koymans, G.R. Renardel de Lavalette, The logic MPL„, in: Algebraic methods: Theory, Tools and Applications (M. Wirsing, J.A. Bergstra, eds.) Lecture Notes in Computer Science 394, Springer-Verlag, 1989.Google Scholar
  17. [17]
    C.A. Middelburg, The VIP VDM specification language,in: VDM’88, VDM — the WAY AHEAD (r. Bloomfield, L. Marshall, R. Jones, eds.), Lecture Notes in Computer Science 328, Springer-Verlag (1989) 187–201.Google Scholar
  18. [18]
    C.A. Middelburg, VVSL: a language for structured VDM specifications, Formal aspects of Computing 1 (1989) 115–135.CrossRefGoogle Scholar
  19. [19]
    C.A. Middelburg, G.R. Renardel de Lavalette, LPF and MPLW - a logical comparison of VDM SL and COLD-K, in: S. Prehn, W.J. Toetenel (eds.) VDM’91: Formal Software Development Methods, LNCS551, Springer-Verlag, 279–308.Google Scholar
  20. [20]
    G.R. Renardel de Lavalette, COLD-K2, the static kernel of COLD-K, Report RP/mod-89/8, Software Engineering Research Centre, Utrecht, the Netherlands, November 1989.Google Scholar
  21. [21]
    G.R. Renardel de Lavalette, Logical semantics of modularisation,in: Computer Science Logic’91 (E. Börger, G. Jäger, H. Kleine Büning, M.M. Richter, eds.), LNCS626, 306–315.Google Scholar
  22. [22]
    G.R. Renardel de Lavalette, Formal development of a serial copy management system,in: Vdm’91: Formal Software Development Methods (S. Prehn, W.J. Toetenel, eds.), LNCS551, Springer-Verlag, 477–495.Google Scholar
  23. [23]
    G.R. Renardel de Lavalette, From implicit via inductive to explicit definitions,this volume.Google Scholar
  24. [24]
    D.S Scott, Existance and description in Formal Logic, in: R. Schoenman (Ed.), Bertrand Russell, Philosopher of the Century, Allen and Unwin, London, (1967), 181–200.Google Scholar

Copyright information

© British Computer Society 1994

Authors and Affiliations

  • Gerard R. Renardel de Lavalette
    • 1
  1. 1.Department of Computing ScienceUniversity of GroningenGroningenThe Netherlands

Personalised recommendations