LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/internals/verify eiffel sw/01 introduction

01 introduction

This folder contains some rough ideas to pave the way towards a verifying eiffel compiler.

Goal: Check all assertions, output the verified and unverified assertions.

Theory: Weakest precondition calculus.

Some basic definitions:

 Local Variables: 
 mode: outline
 coding: iso-latin-1
 outline-regexp: "=\\(=\\)*"