 |
|
Application name:
CAT Compiler System
Organisation:
Norsk Data GmbH, Muelheim, Germany
Method:
VDM
Tools:
A simple VDM compiler which takes code generator specifications written in (a subset of) VDM as input and generates a Pascal module from it. Integrated part of the system. VDM Class Library Generator
Domain:
Software engineering
Period:
The project started in 1983. Until 1991, new components were developed and maintenance was done.
Size:
team size: seven (during initial development) to two (during maintenance) persons; about 30.000 lines of VDM specification.
Description:
The CAT compiler system provides compilers for several source languages (C, Pascal, Basic,...) for different platforms. The source language program is compiled into an intermediate language (CAT) representation from which then code generators produce code for the different target processors/operating systems.
Application of VDM:
- specification of the critical front end parts (static semantic check, compile algorithm);
- manual translation to Pascal using a precoded implementation library for the abstract syntax representation;
- code generator specification in VDM;
- automatic translation to Pascal using the VDM subset compiler;
- later developments (peephole optimizer, ...) were specified in VDM and implemented using the VDM Class Library Generator;
- initial work done on correctness proofs for the code generator specifications.
Conclusions:
- All important aspects of the application domain were covered during the specification phase. Coding was straightforward and resulted in nearly error-free code from the beginning.
- Automatic translation of code generator specifications moved programming effort to a `higher level'.
- The application of VDM was successful but during the early years the following problems were encountered: + Specifying - due to missing tool support - was a more or less paper and pencil work. Therefore, no hard milestones could be demonstrated for a long period of time (e.g. the specification of the Basic front end took five months, no single line of code was produced during this time and management got nervous at the end. After another month of coding the front end was running right from the start). + Acceptance of the method increased once better tool support became available (VDM Class Library Generator).
Publications:
"Programming with VDM Domains". Hans-Martin Hoercher and Uwe Schmidt. In: VDM'90; VDM and Z -- Formal Methods in Software Development. D. Bjoerner, H. Langmaack and C.A.R. Hoare (editors). Springer-Verlag, LNCS 428. Pages 122-134. 1990.
"Correctness Proofs for META-IV written Code Generator Specifications using Term Rewriting". Karl Heinz Buth and Bettina Wenzel. In: VDM'88; VDM -- The Way Ahead. R. Bloomfield, L. Marshall, R. Jones (editors). Springer-Verlag, LNCS 328. Pages 406-433. 1988.
"Experiences with VDM in Norsk Data". Uwe Schmidt and Reinhard Voeller. In: VDM'87; VDM -- A Formal Method at Work. D. Bjoerner, C.B. Jones (editors). Springer-Verlag, LNCS 252. Pages 49-62. 1987.
Contact:
| Name: | Hans-Martin Hoercher |
| Organisation: | DST Deutsche System-Technik GmbH |
| Address: | Edisonstrasse 3
D-24145 Kiel |
| Country: | Germany |
| Phone number: | +49 (431) 710 |
| Fax: | +49 (431) 7109503 |
| E-mail: | hoercher@dst.de |
Contact:
| Name: | Uwe Schmidt |
| Organisation: | Fachhochschule Wedel |
| Address: | Feldstrasse 143
D-22880 Wedel |
| Country: | Germany |
| Phone number: | +49 (4103) 804845 |
| E-mail: | uwe@fh-wedel.de |
|
