Lambda the Ultimate

The following paper describes a proof engine for the Eiffel language.

The proof engine allows the verification of the assertions of Eiffel
code. Some language extensions are introduced to express proofs of
assertions. Within the proofs the user can enter proof commands and the proof
engine can verify the correct use of the proof commands.

Modularization techniques are introduced to the keep the proofs small and
expressive.

The proof engine has some improved features to do the burdensome work for the
user. It is expected that the developer enters the key assertions and proves
them and the proof engine can verify the routines using the key assertions.

- In the first chapter the basic concepts are explained.

- The second chapter introduces the commands of the proof engine.

- The third chapter shows how basic properties of boolean expression can be
proved with the proof engine.

- The forth chapter applies the proof engine to assertions within the class
INTEGER

- The fifth chapter shows how routines can be proved.

Find the detailed paper at http://tecomp.sourceforge.net (manual navigation: http://tecomp.sourceforge.net -> white papers -> verification -> proof engine)