A Verification Environment for Imperative and Functional Programs in the Theorema system
Tudor Jebelean · 2005
We present a verification environment for imperative pro- grams (using Hoare logic) and for functional programs (using fixpoint theory) in the frame of the Theorema system (www.theorema.org). In particular, we discuss some methods for finding the invariants of loops and of specifications of auxiliary tail recursive functions. These meth- ods use algorithms from (polynomial) algebra and combinatorics, namely Groebner bases, variable elimination and symbolic summation (the Gosper algorithm, the technique of generating functions). The techniques are demonstrated on several examples which have been treated automati- cally by our implementation. AMS Subject Classification: 33F10, 65G20, 68N30, 68Q60, 68W30