Skip to main content
SpringerLink
Log in

Reasoning about Dynamic Features in Specification Languages

A Modal view on Creation and Modification

  • Conference paper
Semantics of Specification Languages (SoSL)

Part of the book series: Workshops in Computing ((WORKSHOPS COMP.))

Abstract

Using algebras over some signature to model the notion of state is quite common in specification languages. Some specification formalisms, e.g. COLD and Evolving Algebras, also allow for the dynamic change of states. Two kinds of elementary procedures are used: creation (of a new object) and modification (of a function or predicate at some point).

In this paper we present and investigate MLCM (Modal Logic of Creation and Modification), a multimodal predicate logic for reasoning over programs built up from such procedures. MLCM deviates from traditional dynamic predicate logic in two respects: creation is added as a primitive program construct and assignment (to variables) is replaced by assignment to constants and parametrized assignment to function and predicate symbols.

We present a definition of syntax, semantics and axiomatisation of MLCM and establish completeness for the repetition-free fragment via a traditional Henkin construction.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. E. Börger, A logical operational semantics for full prolog, In: Proceedings CSL ‘89, E. Börger, H. Kleine Büning and M.M. Richter (Eds.), LNCS 440, Springer Verlag, 1990, pp. 36–64.

    Google Scholar 

  2. E. Börger and D. Rosenzweig, The WAM — definition and Compiler Correctness, Technical Report TR - 14/92, Department of Computer Science, University of Pisa, 1992.

    Google Scholar 

  3. C.C. Chang and H.J. Keisler, Model Theory, North Holland, Second revised editon, 1990.

    MATH  Google Scholar 

  4. E.W. Dijkstra and C.S. Scholten, Predicate Calculus and Program Semantics, Springer Verlag, 1990.

    Google Scholar 

  5. L.M.G. Feijs and H.B.M. Jonkers, Formal Specification and Design, Cambridge Tracts in Theoretical Computer Science 35, 1992.

    Google Scholar 

  6. L.M.G. Feijs, H.B.M. Jonkers, C.P.J. Koymansar G.h. Renardel de Lavalette, Formal definition of the design language COLD-K (Preliminary version), ESPRIT document METEOR/t7/PRLE/7, April 1987 ( Final version: August 1989 ).

    Google Scholar 

  7. R. Goldblatt, Axiomatising the logic of computer science, LNCS 130, Springer Verlag, 1982.

    Google Scholar 

  8. Y. Gurevich, Logic and the challenge of computer science, In: Trends in Theoretical computer science, E. Börger (ed.), Computer Science Press, 1988, pp. 1–57.

    Google Scholar 

  9. Y. Gurevich, Evolving algebras; a tutorial introduction, Bulletin of the EATCS 43, Febr. 1991, pp. 264–284

    Google Scholar 

  10. Y. Gurevich and L. Moss, Algebraic operational semantics and Occam, In: Peoceedings CSL ‘89, E. Börger, H. Kleine Büning and M.M. Richter (Eds.), LNCS 440, Springer Verlag, 1990, pp. 176–192.

    Google Scholar 

  11. J.V. Guttag and J.J. Horning, The algebraic specification of abstract data types, Acta Informatica 10, 1978, pp. 27–52.

    Article  MathSciNet  MATH  Google Scholar 

  12. D. Harel, Dynamic Logic, In: Handbook of Philosophical Logic, Vol. II, D. Gabbay and F. Guenthner (eds.), D. Reidel Publishing Company, 1984, pp. 497–604.

    Google Scholar 

  13. M. Heisel, W. Reif and W. Stephan, A dynamic logic for program verfication, In: Logic at Botik 89,A. Meyer, M. Taitslin (eds), LNCS 363, Springer Verlag, pp. 134–145.

    Google Scholar 

  14. M. Heisel, W. Reif and W. Stephan, Tactical Theorem Proving in Program Verification, In: Conference on Automated Deduction, Siekmann (ed), LNAI, Spinger Verlag, 1990.

    Google Scholar 

  15. L. Henkin, The completeness of the first order functional calculus, The Journal of Symbolic Logic 14, 1949, pp. 159–166.

    Article  MathSciNet  MATH  Google Scholar 

  16. C.P.J. Koymans and G.R. Renardel de Lavalette, The logic MPLW, In: Algebraic Methods: Theory, tools and applications, M. Wirsing and J.A. Bergstra (eds.), LNCS 394, Springer Verlag, 1989, pp. 247–282.

    Google Scholar 

  17. V.R. Pratt, Semantical considerations on Floyd-Hoare logic, Proc. 17th annual IEEE symp. on foundations of computer science, 1976, pp. 109–121.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing Science, University of Groningen, P.O. Box 800, 9700 AV, Groningen, The Netherlands

    Rix Groenboom & Gerard R. Renardel de Lavalette

Authors
  1. Rix Groenboom
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gerard R. Renardel de Lavalette
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Mathematics and Computer Science, University of Leicester, University Road, LE1 7RH, Leicester, UK

    D. J. Andrews

  2. Department of Philosophy, Utrecht University, Heidelberglaan 8, 3584 CS, Utrecht, The Netherlands

    J. F. Groote (dr.ir) & C. A. Middelburg (prof.dr.ir) (dr.ir) &  (prof.dr.ir)

Rights and permissions

Reprints and permissions

Copyright information

© 1994 British Computer Society

About this paper

Cite this paper

Groenboom, R., Renardel de Lavalette, G.R. (1994). Reasoning about Dynamic Features in Specification Languages. In: Andrews, D.J., Groote, J.F., Middelburg, C.A. (eds) Semantics of Specification Languages (SoSL). Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3229-5_19

Download citation

  • DOI: https://doi.org/10.1007/978-1-4471-3229-5_19

  • Publisher Name: Springer, London

  • Print ISBN: 978-3-540-19854-3

  • Online ISBN: 978-1-4471-3229-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation