Diplomarbeit
Type of project:
Diploma Thesis January - May 2008
Author:
Hasan Karahan
Title:
Proof-Transforming Compilation of Eiffel Contracts
Supervising Assistant:
Martin Nordio
Description
|
A proof-transforming compiler is a compiler that takes a source proof as input and produces a bytecode proof. This project consists of the development of a proof-transforming compiler for Eiffel contracts. The compiler takes a source proof with contracts and produces a bytecode proof and its CIL contract. The work consists of the implementation of a contract translation. The input of the compiler is a source proof and contracts written in the XML format. In a first step, a parser for the source proof will be implemented. The parser will produce an AST.
The result will be a proof-transforming compiler for a subset of Eiffel and it consists of:
|