Generation of Invariants in Theorema
Laura Ildik, KovTudor Jebelean · 2003
Explicitly stated program invariants can help programmers by identifying program prop- erties that must be preserved when modifying code. In practice, in most of the cases, however, these invariants are usually implicit. In this paper we present an alternative to expecting programmers to fully annotate code with invariants, namely a method for automatically generation of invariants from the program itself, using an implementation of a prototype verification condition generator for impera- tive programs. The generator is part of the Theorema system, a computer aided mathematical assistant which offers automated reasoning and computer algebra facilities. We use Hoare Logic and the weakest precondition strategy, and we propose a novel method for analyzing loop constructs by aid of algebraic computations: combinatorial summation and equational elimination. The verification conditions for pro- grams containing loops are generated fully automatically, in a form which can be immediately used by the automatic provers of Theorema in order to check whether they hold.