
Semesterarbeit

Prooftransforming compilers (PTC) are similar to certifying compilers in proofcarrying code, but take a source proof as input and produce the bytecode proof. An important property of prooftransforming compilers is that they do not have to be trusted. If the compiler produces a wrong specification or a wrong proof for a component, the proof checker of the component platform will reject the component. Goal of the semester project is to implement a prooftransforming compiler from Eiffel to .Net CIL. The source languge is a subset of Eiffel, the logic for the subset of Eiffel is a Hoare style logic. The bytecode language is .Net CIL. 