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’s Hk(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 c...
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Objeto de conferencia |
| Lenguaje: | Inglés |
| Publicado: |
2017
|
| Materias: | |
| Acceso en línea: | http://sedici.unlp.edu.ar/handle/10915/65163 |
| Aporte de: |
| Sumario: | In this paper we present a series of theorems that allow to establish strategies for the calculation of invariant assertions, such as the Dijkstra’s Hk(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. |
|---|