[an error occurred while processing this directive]


Type of project:
Diploma Thesis January - May 2008

Hasan Karahan

Proof-Transforming Compilation of Eiffel Contracts

Supervising Assistant:
Martin Nordio


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:

  • A parser for the source proof.
  • A parser for the contract language.
  • A parser for a super set of the contract language.
  • A contract translator.
  • projectplan