LEX : a case study in development and validation of formal specifications
Andreas Ramses Heckler, Rudolf Hettler, Heinrich Hußmann, Jacques Loeckx, Wolfgang Reif, Gerhard Schellhorn, Stenzel, Kurt · 1996
The paper describes an experiment in the combined use of various tools for the development and validation of formal specifications. The first tool consists of a very abstract, (non-executable) axiomatic specification language. The second tool consists of an (executable) constructive specification language together with a specification environment. Finally, the third tool is a verifiation system. The first two tools were used to develop two specifications for the same case study, viz. a generic scanner similar to the tool Lex present inUnix. Reflecting the nature of the tools the first specification is abstract and non-executable, whereas the second specification is less abstract but executable. Thereupon the verification system was used to formally prove that the second specification is consistent with the first one in that it describes the same problem. During this proof it appeared that both specifications contained conceptual errors ("adequacy errors"). It is argued that the combined use of tools similar to those employed in the experiment may substantially increase the quality of software.