User loginNavigation 
archivesIntroduction to the proof engine for static verification of softwareMy latest blog entry talks about the proof engine of Modern Eiffel. The blog entry is a basic introduction to the proof engine. It shows the basic inference rules, the basic commands, it introduces some axioms to reason in the propositional calculus. A lot of proofs are demonstrated using the boolean operators "and" "or" and "=>". The introduction should be easy to follow, even for SW developers without training in proof techniques and formal mathematics. The proof engine is intended to be easy to use and understand. The introduction to the proof engine demonstrates that writing proofs is just another form of programming (manipulating the state of the proof engine with proof commands). Those not familiar with Modern Eiffel can read be previous blog entry to understand its basic concepts. By hbrandl at 20120220 17:46  LtU Forum  login or register to post comments  other blogs  2055 reads

Browse archivesActive forum topics
New forum topics 
Recent comments
8 hours 30 min ago
12 hours 37 min ago
13 hours 28 min ago
13 hours 53 min ago
1 day 22 hours ago
1 day 23 hours ago
1 day 23 hours ago
1 day 23 hours ago
2 days 2 hours ago
2 days 10 hours ago