Skip to main content

Constructive specifications of abstract data types using temporal logic

  • Conference paper
  • First Online:
Logical Foundations of Computer Science — Tver '92 (LFCS 1992)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 620))

Included in the following conference series:

  • 154 Accesses

Abstract

We introduce an approach for the specification of abstract data types based on temporal logic. To this end we propose a constructive specification method. We present axiom schemes to get generally monomorphic and complete models. Nonconstructive operations are defined as abbrevations for algorithms using constructors. It is shown that our approach is at least as expressive as the classical method. Moreover it is possible to specify semicomputable and co-semicomputable algebras monomorphically.

The work of the author is supported by the Sonderforschungsbereich 342 of the TU München.

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

Access this chapter

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. H.Ehrig, B.Mahr: Fundamentals of Algebraic Specifications 1, Springer Verlag (1985)

    Google Scholar 

  2. D.Hilbert, P.Bernays: Grundlagen der Mathematik, Springer Verlag (1934)

    Google Scholar 

  3. H.A.Klaeren: A constructive method for abstract algebraic software specification, Theoretical Computer Science 30 (1984) 139–204

    Article  Google Scholar 

  4. F.Kröger: Temporal Logic of Programs, Springer Verlag (1987)

    Google Scholar 

  5. F.Kröger: Abstract Modules: Combining algebraic and temporal logic specification means, Techniques et Science Informatiques 6 (1987) 559–573

    Google Scholar 

  6. F.Kröger: On the interpretability of arithmetic in temporal logic, Theoretical Computer Science 73 (1990) 47–60

    Article  Google Scholar 

  7. F.Lesske: On constructive specifications of abstract data types using temporal logic, Report of the TU München, TUM-I9146 (1991)

    Google Scholar 

  8. J.Loeckx: Algorithmic Specifications: A Constructive Specification Method for Abstract Data Types, ACM Trans. on Progr. Languages and Systems 9 (1987) 646–685

    Article  Google Scholar 

  9. S.Merz: Characterizing Initial Models of Abstract Data Types Using Temporal Logic, Ludwig Maximilians Universität München, Institut für Informatik, Report 91/02 (1991)

    Google Scholar 

  10. Z.Ming-Hua: A Second Order Theory of Data Types, Acta Informatica 25 (1988) 283–303

    Article  Google Scholar 

  11. G.Mirkowska, A.Salwicki: Algorithmic Logic, D.Reindel Publishing Company (1987)

    Google Scholar 

  12. A.Szalas: Towards the temporal approach to abstract data types, Fundamenta Informaticae 11 (1988) 49–64

    Google Scholar 

  13. M.Wirsing: Algebraic Specification, in: Handbook of Theoretical Computer Science II, North Holland, Amsterdam (1990)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Anil Nerode Mikhail Taitslin

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lesske, F. (1992). Constructive specifications of abstract data types using temporal logic. In: Nerode, A., Taitslin, M. (eds) Logical Foundations of Computer Science — Tver '92. LFCS 1992. Lecture Notes in Computer Science, vol 620. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0023881

Download citation

  • DOI: https://doi.org/10.1007/BFb0023881

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-55707-4

  • Online ISBN: 978-3-540-47276-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics