Skip to main content
SpringerLink
Log in

Experiences with a specification environment

  • Development Systems and Logical Frameworks
  • Chapter
  • First Online:
KORSO: Methods, Languages, and Tools for the Construction of Correct Software

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

  • 150 Accesses

Abstract

The Obscure system is an environment intended to support the design and verification of specifications. After a short informal description of the system the paper sketches the case studies carried out in the framework of the Korso project. Based on the experience gained and on a comparison with other systems used within the Korso project, the paper critically discusses the use of specifications in the design of correct software in general and the features of the Obscure system in particular.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. A. Ayari, S. Friedrich, A. Heckler, and J. Loeckx. Das Fallbeispiel Lex. Technical Report WP 92/39, Univ. Saarbrücken, 1992.

    Google Scholar 

  2. S. Autexier. Hdms-A und Obscure — Die Funktionale Essenz von Hdms-A aus Sicht der algorithmischen Spezifikationsmethode — TEIL 2: Spezifikation des Datenmodells. Technical Report A/05/93, Univ. Saarbrücken, 1993.

    Google Scholar 

  3. S. Autexier, C. Benzmüller, and A. Heckler. Das Fallbeispiel Unix. Technical Report WP 92/36, Univ. Saarbrücken, 1992.

    Google Scholar 

  4. R. Betschko, S. Dick, K. Didrich, J. Faulhaber, and W. Grieskamp. Formal Development of an Efficient Implementation of a Lexical Scanner within the Korso Methodology Framework. Technical report 93-30, TU Berlin, 1993.

    Google Scholar 

  5. C. Benzmüller. Hdms-A und Obscure — Die Funktionale Essenz von HDMS-A aus Sicht der algorithmischen Spezifikationsmethode — TEIL 3: Spezifikation der atomaren Funktionen. Technical report A/06/93, Univ. Saarbrücken, 1993.

    Google Scholar 

  6. M. Bidoit. Pluss, a language for the development of modular algebraic specifications. Thèse d'Etat, Univ. Paris-Sud, 1989.

    Google Scholar 

  7. M. Bidoit, M.-C. Gaudel, and A. Mauboussin. How to make algebraic specifications more understandable: An experiment with the Pluss specification language. In: Science of Computer Programming 12, 1, 1–38, 1989.

    Article  Google Scholar 

  8. M. Broy, C. Facchi, R. Grosu, R. Hettler, H. Hußmann, D. Nazareth, F. Regensburger, and K. Stølen. The Requirement and Design Specification Language Spectrum — An Informal Introduction. Technical Report TUM-I9312, TU München, 1993.

    Google Scholar 

  9. J. Cai, S. Schlobach, and M. Wolf. The translation from Obscure into Ml: Documentation of the translation principles. Technical Report WP 93/43, Univ. Saarbrücken, 1993.

    Google Scholar 

  10. C. Choppy. Is my Specification “correct”? A Study with Pluss Specifications. Rapport de Recherche n∘ 817, Université de Paris Sud, 1993.

    Google Scholar 

  11. F. Cornelius, H. Hußmann, and M. Löwe. The Korso Case Study for Software Engineering with Formal Methods: A Medical Information System. In this volume.

    Google Scholar 

  12. E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.

    Google Scholar 

  13. A. Dold and M. Strecker. Program development with specification operators — illustrated by a specification of the LEX scanner. Korso working paper, Univ. Ulm, 1993.

    Google Scholar 

  14. Ch. Dollin, P. Arnold, D. Coleman, H. Gilchrist, and T. Rush. Axis Tutorial: a simple filing system. Technical Report HPL-ISC-TM-88-18, Hewlet-Packard Ltd., Bristol, 1988.

    Google Scholar 

  15. H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1 — Equations and Initial Semantics. Springer-Verlag, 1985.

    Google Scholar 

  16. J. Fuchs, A. Hoffmann, L. Meiss, J. Philippi, M. Stolz, M. Wolf, and J. Zeyer. The Obscure Manual. Part 1: Editing and Rapid Prototyping. Technical Report A/03/91, Univ. Saarbrücken, 1991.

    Google Scholar 

  17. A. Heckler. Hdms-A und Obscure — Die Funktionale Essenz von Hdms-A aus Sicht der algorithmischen Spezifikationsmethode — TEIL 1: Einführung und Anmerkungen. Technical Report A/04/93, Univ. Saarbrücken, 1993.

    Google Scholar 

  18. A. Heckler, R. Hettler, H. Hußmann, J. Loeckx, W. Reif, G. Schellhorn and K. Stenzel. Lex: A Case Study in Development and Validation of Formal Requirement Definitions. Submitted for publication.

    Google Scholar 

  19. R. Hettler. A Requirement Specification for a Lexical Analyzer. Technical Report TUM-I9409, TU München, 1994.

    Google Scholar 

  20. R. Hettler. Spezifikation des Unix-Datei-und Variablensystems. Eine Spectrum-Fallstudie. Technical Report (TUM-I9230), TU München, 1992.

    Google Scholar 

  21. T. Lehmann and J. Loeckx. Obscure, A Specification Language for Abstract Data Types. In: Acta Informatica 30, 303–350, 1993.

    Article  Google Scholar 

  22. J. Loeckx. Algorithmic specifications: a constructive specification method for abstract data types. In: ACM Trans. Prog. Lang. Syst. 9, 646–685, 1987.

    Article  Google Scholar 

  23. C. Morgan and B. Sufrin. Specification of the Unix Filing System. In: I. Hayes, editor, Specification Case Studies pp.90–140, Prentice Hall, 1987.

    Google Scholar 

  24. O. Slotosch, F. Nicki, S. Merz, H. Hußmann, and R. Hettler. Die funktionale Essenz von HDMSA. Technical Report TUM-I9335, TU München, 1993.

    Google Scholar 

  25. D. Sannella. A set-theoretic semantics of Clear. In: Acta Informatica 21, 443–472, 1984.

    Article  Google Scholar 

  26. D. Sannella and M. Wirsing. A kernel language for algebraic specification and implementation. LNCS 158, 413–427, 1983.

    Google Scholar 

  27. M. Wirsing. Algebraic specification. In: J. van Leeuwen, editor, Handbook of Theoretical Computer Science, North-Holland, 1990.

    Google Scholar 

  28. J. Zeyer. Kontextbedingungen für Obscure. Technical Report WP 89/11, Univ. Saarbrücken, 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Saarbrücken, Germany

    Jacques Loeckx & Jörg Zeyer

Authors
  1. Jacques Loeckx
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jörg Zeyer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Manfred Broy Stefan Jähnichen

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Loeckx, J., Zeyer, J. (1995). Experiences with a specification environment. In: Broy, M., Jähnichen, S. (eds) KORSO: Methods, Languages, and Tools for the Construction of Correct Software. Lecture Notes in Computer Science, vol 1009. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0015466

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60589-8

  • Online ISBN: 978-3-540-47802-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation