Calculation of Invariants Assertions

摘要

In this paper we present a series of theorems that allow to establish strategies for the calculation of invariant assertions, such as the Dijkstra'sHk(Post), or the weakest precondition of the loop. A criterion is also shown for calculating the termination condition of a loop. As in the integrals calculus, the strategies proposed here to perform the calculation of an invariant, will depend on the shape of the loop with which it is working, particularly will work with for-type loops with or without early termination due to a sentry.http://www.elsevier.com/locate/entcs.