Executing formal specifications need not be harmful
- 1 January 1996
- journal article
- Published by Institution of Engineering and Technology (IET) in Software Engineering Journal
- Vol. 11 (2) , 104-110
- https://doi.org/10.1049/sej.1996.0014
Abstract
The various arguments that have been advanced for and against the use of executable specifications are reviewed. Examples are provided of the problems that may arise in applying this technique and of the benefits which may accrue. A case study is reported in which execution is used to validate the published specification of a commercially available package. It is concluded that there are circumstances when executable specifications can be of high value but that execution must be used together with, and as a supplement to, other methods of validating specifications such as inspection and proof.Keywords
This publication has 10 references indexed in Scilit:
- Automating the generation and sequencing of test cases from model-based specificationsPublished by Springer Nature ,2005
- Towards Correct Executable Semantics for ZPublished by Springer Nature ,1994
- Model checking in practicePublished by Springer Nature ,1993
- The VDM-SL Reference GuidePublished by Taylor & Francis ,1991
- What is a Good Formal Specification?Published by Springer Nature ,1991
- From Z Specifications To Functional ImplementationsPublished by Springer Nature ,1990
- Computer Aided Transformation of Z into PrologPublished by Springer Nature ,1990
- Specifying and prototyping: Some thoughts on why they are successfulPublished by Springer Nature ,1985
- Miranda: A non-strict functional language with polymorphic typesLecture Notes in Computer Science, 1985
- Proofs and RefutationsPublished by Cambridge University Press (CUP) ,1976