How to make algebraic specifications more understandable?

An experiment with the PLUSS specification language
  • M. Bidoit
  • M.-C. Gaudel
  • A. Mauboussin
Part I Algebraic Specification
Part of the Lecture Notes in Computer Science book series (LNCS, volume 394)


This paper relates an experiment in writing an algebraic specification of a rather complex example, namely a subset of the UNIX file system. The PLUSS specification language, which is used for this experiment, provides a set of linguistic features which allow the modularization of such specifications and the definition of a flexible and convenient syntax for expressions and axioms (such as mixfix operators, overloading, coercions, ...). This experiment was a way for evaluating the adequacy of these features to several criteria: mainly legibility and understandability, but also reusability of specifications. The paper presents the specification and discusses it with respect to these important points.


Concrete Syntax Abstract Data Type File Specification Home Directory Algebraic Specification 
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. [ADJ 78]
    J. Goguen, J. Thatcher and E. Wagner, "An Initial Algebra Approach to the Specification, Correctness and Implementation of Abstract Data Types", Current Trends in Programming Methodology, Vol.4, Yeh Ed., Prentice Hall, 1978.Google Scholar
  2. [AW 86]
    E. Astesiano and M. Wirsing, "An Introduction to ASL", Proceedings of the IFIP WG 2.1 Working Conference on Program Specifications and Transformations, Bad Toelz, FRG, 1986.Google Scholar
  3. [BBC 86]
    G. Bernot, M. Bidoit and C. Choppy, "Abstract Dat Types with Exception Handling: An Initial Approach Based on a Distinction between Exceptions and Errors" Theoretical Computer Science, Vol. 46, No. 1, pp.13–45, 1986.CrossRefGoogle Scholar
  4. [B2G3 84]
    M. Bidoit, B. Biebow, M-C. Gaudel, C. Gresse and G. Guiho, "Exception Handling: Formal Specification and Systematic Program Construction", Proceedings of the 7th International Conference on Software Engineering, Orlando, March 1984.Google Scholar
  5. [BC 86]
    M. Bidoit and C. Choppy, "The ALEX-PLUSS Specification Language", ESPRIT Project "FOR-ME-TOO" Report, January 1986.Google Scholar
  6. [BCM 84]
    B. Biebow, N. Choquet and A. Mauboussin, "Specification par Types Abstraits Algebriques de Fonctions Caracteristiques d'une Unite de Raccordement d'Abonnes Telephoniques", Rapport de Contrat DAII 84.35.087, Sept. 1985.Google Scholar
  7. [BG 85]
    M. Bidoit and M.-C. Gaudel, "PLUSS: Proposition pour un Langage de Specifications Structurees", Actes des Journees AFCET "Nouveaux Langages pour le Genie Logiciel", Evry, France, October 28–29, 1985, BIGRE+GLOBULE No.45.Google Scholar
  8. [BH 85]
    B. Biebow and J. Hagelstein, "Algebraic Specification of Synchronisation and Errors: A Telephonic Example", Proceedings of TAPSOFT, Berlin, March 1985, Vol. 2, pp.294–308, LNCS 186, Springer-Verlag.Google Scholar
  9. [Bid 84]
    M. Bidoit, "Algebraic Specification of Exception Handling and Error Recovery by Means of Equations and Declarations", ICALP Proceedings, LNCS, Springer Verlag, 1984.Google Scholar
  10. [Bie 84]
    B. Biebow, "Application d'un Langage de Specification Algebrique a des Exemples Telephoniques", These de 3e Cycle, Universite Paris 6, Feb.1984.Google Scholar
  11. [BW 82]
    M. Broy and M. Wirsing, "Partial Abstract Types", Acta Informatica 18, pp.47–64, 1982.Google Scholar
  12. [CGHM 86]
    M-A. Choquer, M-C. Gaudel, Y. Holvoet and A. Mauboussin, "A Concrete Syntax for PLUSS", METEOR Report, Task 10 and 11, March 1986.Google Scholar
  13. [Cho 86]
    M.-A. Choquer, "Specification of the Evaluation Tool: Leftmost Outermost Reduction Strategy in the Equational Case", METEOR Report, November 86.Google Scholar
  14. [CLP 86]
    CGE-LRI-Passau Teams, "A Proposed List of Components for a Specification Development Environment", METEOR Working Document, September 1986.Google Scholar
  15. [Des 83]
    J. Despeyroux-Savonitto, "An Algebraic Specification of a Pascal Compiler", SIGPLAN 18(12), pp34–48, 1983.CrossRefGoogle Scholar
  16. [Fei 87]
    L.M.G. Feijs, "Systematic Design with COLD-K-an annoted example-", METEOR Report, METEOR/t8/PRLE/3, Philips Research Laboratories Eindhoven, December 1987.Google Scholar
  17. [FGJM 85]
    K. Futatsugi, J. A. Goguen, J-P. Jouannaud and J. Meseguer, "Principles of OBJ2", Proceedings of 12th ACM Symposium on Principles of Programming Languages, New-Orleans, Louisiana, Jan.14–16, 1985, pp.52–66.Google Scholar
  18. [FJKR 87]
    L.M.G. Feijs, H.B.M. Jonkers, C.P.J. Koymans and G.R. Renardel de Lavalette, "Formal Definition of the Design Language COLD-K", METEOR Report, METEOR/t7/PRLE/7, Philips Research Laboratories Eindhoven, Preliminary Edition, April 1987.Google Scholar
  19. [Gau 84]
    M.-C. Gaudel, "A First Introduction to PLUSS", METEOR Report, December 1984.Google Scholar
  20. [Gau 85]
    M.-C. Gaudel, "Toward Structured Algebraic Specifications", Conference Preprints of Esprit Technical Week '85, Brussels, September 23–25, 1985, also in ESPRIT'85 Status Report of Continuing Work, Edited by The Commission of the European Communities, Brussels.Google Scholar
  21. [GH 85]
    A. Geser and H. Hussmann, "Rapid Prototyping for Algebraic Specifications, Examples for the Use of the RAP System", MIP-8517, Universitaet Passau, Dec. 1985.Google Scholar
  22. [Hus 85]
    H. Hussmann, "Rapid Prototyping for Algebraic Specifications — RAP-System User's Manual", MIP-8504, Universitaet Passau, Mar. 1985.Google Scholar
  23. [Jon 84]
    H.B.M. Jonkers, "Specification of a UNIX like File System in COLD-S", FAST Working Document, Philips Research Laboratories Eindhoven, 1984.Google Scholar
  24. [LG 86]
    B. Liskov and J. Guttag, "Abstraction and Specification in Program Development", MIT Press, 1986.Google Scholar
  25. [Mos 86]
    P. Mosses, "Action Semantics", 4th Workshop on Abstract Data Types, Burg Warberg, G.R.D., 1986.Google Scholar
  26. [MS 84]
    C. Morgan and B. Sufrin, "Specification of the UNIX Filing System", IEEE Transactions on Software Engineering, Vol.SE-10, No.2, pp.128–142, Feb. 1984.Google Scholar
  27. [Pro 82]
    K. Proch, "ORSEC: Un Outil de Recherche de Specifications Equivalentes par Comparaison d'Exemples", These de 3e Cycle, CRIN, Nancy, France, Dec. 1982.Google Scholar
  28. [Wis 83]
    M. Wirsing, "Structured Algebraic Specifications: A Kernel Language", Habilitation Thesis, Techn. Univ. Munchen, 1983, to appear in TCS, also Univ. Passau, MIP-8511.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1989

Authors and Affiliations

  • M. Bidoit
    • 1
    • 2
  • M.-C. Gaudel
    • 1
  • A. Mauboussin
    • 2
  1. 1.LRI, Bat. 490, Universite de Paris-SudOrsay CedexFrance
  2. 2.Laboratoires de Marcoussis, CR-CGEMarcoussisFrance

Personalised recommendations