Proofs for Eiffel SW
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 -> white papers -> verification -> proof engine
I'm confused about the goal you're trying to achieve. Is it to prove that assertions correctly describe how features manipulate data, or is it to introduce additional assertions about features that regular Eiffel code cannot describe?
Or did I just completely missed the point?
The goal is to prove that assertions are true, i.e. statically check the assertions instead of checking them at runtime. This applies to all kinds of assertions: class invariants, postconditions of functions, postconditions of routines, preconditions, ....
Unfortunately the standard assertions of Eiffel have not enough descriptive power. Therefore I have introduced some additional elements within the assertions (basically the equivalent of the mathematical `for all') which allow to write more powerful assertions.
With that the above goal seems to be achievable.