|
Last change
on this file since 3221 was
792,
checked in by amadio, 10 years ago
|
|
Deliverable D2.1 with addendum
|
|
File size:
872 bytes
|
| Line | |
|---|
| 1 | We discuss the problem of building a compiler which can {\em lift} in |
|---|
| 2 | a provably correct way pieces of information on the execution cost of |
|---|
| 3 | the object code to cost annotations on the source code. To this end, |
|---|
| 4 | we need a clear and flexible picture of: (i) the meaning of cost |
|---|
| 5 | annotations, (ii) the method to prove them sound and precise, and |
|---|
| 6 | (iii) the way such proofs can be composed. We propose a so-called |
|---|
| 7 | {\em labelling} approach to these three questions. As a first step, |
|---|
| 8 | we examine its application to a toy compiler. This formal study |
|---|
| 9 | suggests that the labelling approach has good compositionality and |
|---|
| 10 | scalability properties. In order to provide further evidence for this |
|---|
| 11 | claim, we report our successful experience in implementing and testing |
|---|
| 12 | the labelling approach on top of a prototype compiler written in |
|---|
| 13 | $\ocaml$ for (a large fragment of) the {\sc C} language. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
