The Eiffel Compiler / Interpreter (tecomp)

engine

• Introduction
• Basic concepts
• The commands of the proof engine
• Propositional calculus
• Predicate calculus
• Verification of routines
• Appendix A: Proofs...