Name
Abstract | ||
|---|---|---|
The development of critical systems often places undue trust in the software tools used. This is especially true of compilers, which are a weak link between the source code produced and the object code which is executed. Stepney [23] advocates a method for the production of trusted compilers (i.e. those which are guaranteed to produce object code that is a correct refinement of the source code) by developing a proof of a small, but non trivial compiler by hand in the Z specification language. This approach is quick, but the type system of Z is too weak to ensure that partial functions are correctly applied. |
Year | DOI | Venue |
|---|---|---|
1997 | 10.1007/3-540-63533-5_30 | FME |
Keywords | Field | DocType |
case study,z refinement,specification language,type system,source code | Specification language,Object code,Programming language,Source code,Computer science,Formal specification,Theoretical computer science,Compiler,Software,High-level programming language,Partial function | Conference |
ISBN | Citations | PageRank |
3-540-63533-5 | 9 | 0.67 |
References | Authors | |
6 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| David W. J. Stringer-Calvert | 1 | 130 | 6.06 |
| Susan Stepney | 2 | 813 | 113.21 |
| Ian Wand | 3 | 9 | 0.67 |