Specifications are (preferably) executable

Specifications are (preferably) executable

For access to this article, please select a purchase option:

Buy article PDF
(plus tax if applicable)
Buy Knowledge Pack
10 articles for £75.00
(plus taxes if applicable)

IET members benefit from discounts to all IET publications and free access to E&T Magazine. If you are an IET member, log in to your account and the discounts will automatically be applied.

Learn more about IET membership 

Recommend Title Publication to library

You must fill out fields marked with: *

Librarian details
Your details
Why are you recommending this title?
Select reason:
Software Engineering Journal — Recommend this title to your library

Thank you

Your recommendation has been sent to your librarian.

The validation of specifications with respect to user requirements is extremely difficult. To ease the validation task and to give users immediate feedback on the behaviour of the future software, it was suggested that specifications should be made executable. However, Hayes and Jones [1] argue that executable specifications should be avoided because executability can restrict the expressiveness of specification langugages, and can adversely affect implementations. We argue for executable specifications by showing that non-executable formal specifications can be made executable on almost the same level of abstraction, and without essentially changing their structure. No new algorithms have to be introduced to get executability. Furthermore, we show that declarative specification languages combine high expressiveness and executability.


    1. 1)
      • Specifications are not (necessarily) executable
    2. 2)
      • A specifier's introduction to formal methods
    3. 3)
      • , New paradigms in software development
    4. 4)
      • Specifications: formal and informal — a case study
    5. 5)
      • Fromherz, M.P.J.: `A survey of executable specification methodologies', 89.05, Technical Report,
    6. 6)
      • , The definition of standard ML
    7. 7)
      • , The art of Prolog'— advanced programming techniques
    8. 8)
      • The relation between logic programming and logic specification, Mathematical logic and programming languages
    9. 9)
      • One, none, a hundred thousand specification languages, Information processing 86 (IFIP)
    10. 10)
      • New research directions in logic specification languages, Information processing 86 (IFIP)
    11. 11)
      • Fromherz, M.P.J.: `A methodology for executable specifications — combining logic programming, object-orientation and visualisation', 1991, PhD Thesis, University of Zurich, Department of Computer Science, Switzerland
    12. 12)
      • TRIO: a language for executable specifications of real-time systems
    13. 13)
      • Stadler, R.: `Ausführbare Beschreibung von Directory-Systemen — Prolog-basierte Spezifikation der Architektur von Directory-Systemen', 1990, PhD Thesis, University of Zurich, Department of Computer Science, Switzerland
    14. 14)
      • PLEASE: executable specifications for incremental software development
    15. 15)
      • An overview and bibliography of ENCOMPASS, an environment for incremental software development using executable, logic-based specifications
    16. 16)
      • Specifications of distributed systems in Prolog
    17. 17)
      • Making Prolog more expressive
    18. 18)
      • Hill, P.M., Lloyd, J.W.: TR-91-02, The Gödel Report, March 1991
    19. 19)
      • Hoare logic, executable specifications, and logic programs
    20. 20)
      • An overview of some formal methods for program design
    21. 21)
      • , Essays in computing science
    22. 22)
      • , The craft of Prolog
    23. 23)
      • , A discipline of programming
    24. 24)
      • Functional programs as executable specifications, Mathematical logic and programming languages
    25. 25)
      • , Specification and transformation of programs — a formal approach to software development
    26. 26)
      • Gardner, P.A., Shepherdson, J.C.: `Unfold/fold transformations of logic programs', PM-89-01, 1989
    27. 27)
      • Stolze, M., Gutknecht, M., Pfeifer, R.: `Integrated knowledge acquisition: toward adaptive expert system design', 91.04, Technical Report, 1991
    28. 28)
      • , Philosophy of logic
    29. 29)
      • Bry, F.: `Logic programming as constructivism: a formalisation and its application to databases', Proc. 8th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS), 1989, Philadelphia, Pennsylvania, p. 34–50
    30. 30)
      • Bundy, A., Smaill, A., Wiggins, G.: `The synthesis of logic programs from inductive proofs', Computational Logic Symp. Proc., November 1990, Brussels, Belgium, Springer Verlag, 1990
    31. 31)
      • , Logic programming, systematic program development
    32. 32)
      • Flener, P.: `Towards stepwise, schema-guided synthesis of logic programs', Proc. LOPSTR '91, 1992, Manchester, UK, Springer Verlag
    33. 33)
      • Fribourg, L.: `Extracting logic programs from proofs that use extended Prolog execution and induction', Proc. 7th Int Conf. on Logic Programming, 1990, Jerusalem, Israel, MIT Press
    34. 34)
      • Lau, K.-K., Prestwich, S.D.: `Synthesis of a family of recursive sorting procedures', Proc. 1991 Int Symp. on Logic Programming, 1991, San Diego, USA, MIT Press
    35. 35)
      • Kemmerer, R.A., White, S., Mili, A., Davis, N.: `Problem set for the Fourth International Workshop on Software Specification and Design', Proc. IEEE ACM Fourth Int. Workshop on Software Specification and Design, April 1987, Monterey California, p. ix–x
    36. 36)
      • Declarative error diagnosis
    37. 37)
      • Zave, P., Yeh, R.T.: `Executable requirements specification for embedded systems', Proc. 5th Int Conf. on Software Engineering, 1981, San Diego, California, p. 295–304, (reprinted in [41])
    38. 38)
      • An operational approach to requirements specification for embedded systems
    39. 39)
      • A transformation system for developing recursive programs
    40. 40)
      • Tamaki, H., Sato, T.: `Unfold/fold transformation of logic programs', Proc. Second Int. Conf. on Logic Programming, 1984, Uppsala, Sweden, p. 127–138
    41. 41)
      • Fuchs, N.E., Fromherz, M.P.J.: `Schema-based transformations of logic programs', Proc. LOPSTR '91, 1992, Manchester, UK, Springer Verlag
    42. 42)
      • , Software specification techniques

Related content

This is a required field
Please enter a valid email address