On Using Conditional Definitions in Formal Theories

  • Jean-Raymond Abrial
  • Louis Mussat
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2272)


In this paper, our intention is to explore the notion of definition in formal theories and, in particular, that of conditional definitions. We are also interested in analyzingthe consequences of the latter on the structure of corresponding proof systems. Finally, we shall investigate the various ways such proof systems can be simplified.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    J.R. Abrial. The B-Book:Assigning Programs to Meanings. Cambridge University Press (1996).Google Scholar
  2. 2.
    H. Barringer, J.H. Cheng, C.B. Jones. A Logic Covering Undefinedness in Program Proofs. Acta Informatica 21: 251–269 (1984).zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    P. Behm, L. Burdy, J.M. Meynadier. Well defined B. Second B International Conference. (Bert editor) LNCS 1393 Springer (1998).Google Scholar
  4. 4.
    L. Burdy Traitement des expressions dépourvues de sens de la théorie des ensembles. Thèse de Doctorat (2000).Google Scholar
  5. 5.
    J.H. Cheng, C.B. Jones On the Usability of Logics which Handle Partial Functions. Proceedings of Third Refinement Workshop. (1990).Google Scholar
  6. 6.
    D. Gries. Foundations for Calculational Logic in Mathematical Methods in Program Development (M. Broy and B. Schieder Editors). Springer (1996).Google Scholar
  7. 7.
    C.B. Jones Partial Functions and Logics: a warning. Information Processing Letter 54 (1995).Google Scholar
  8. 8.
    B. Stoddart, S. Dunne, A. Galloway. Undefined Expressions and Logic in Z and B. Formal Methods in System Design, 15 (1999).Google Scholar
  9. 9.
    P. Suppes. Introduction to Logic. Wadsworth International Group (1957).Google Scholar
  10. 10.
    W.M. Farmer and J.D. Guttman. A Set Theory with Support for Partial Functions in Partiality and Modality. (E. Thijsse, F. Lepage, and H. Wansing Editors). Special issue of Logica Studia (2000).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Jean-Raymond Abrial
    • 1
  • Louis Mussat
    • 2
  1. 1.ConsultantMarseilleFrance
  2. 2.DCSSIParisFrance

Personalised recommendations