Name
Abstract | ||
|---|---|---|
. Starting from the specification of a small imperative programminglanguage, and the description of two program transformationson this language, we formally prove the correctness of these transformations.The formal specifications are given in a single format, and canbe compiled into both executable tools and collections of definitions toreason about into a theorem prover. This work is a case study of an environmentintegrating executable tool generation and formal reasoningon these... |
Year | DOI | Venue |
|---|---|---|
1995 | 10.1007/3-540-59293-8_218 | TAPSOFT |
Keywords | Field | DocType |
executable specifications,programming language,theorem prover,formal specification | Specification language,Programming language,Programming language specification,Computer science,Correctness,Object language,Formal specification,Formal methods,Formal verification,Executable | Conference |
Volume | ISSN | ISBN |
915 | 0302-9743 | 3-540-59293-8 |
Citations | PageRank | References |
13 | 1.18 | 17 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yves Bertot | 1 | 442 | 40.82 |
| Ranan Fraer | 2 | 276 | 17.94 |