Precondición Más Débil de Algoritmos de Punto Fijo

Resumo

Dijkstra definió el transformador de predicados wp (weakest precondition), y en dicha definición establece para la instrucción de iteración Do un predicado Hk(Post) que describe los estados iniciales que hacen que el ciclo itere a lo sumo k veces, satisfaciendo la postcondición Post. En trabajos recientes se han determinado técnicas para calcular explícitamente Hk(Post), lo cual representa una alternativa a la regla de Hoare del invariante y una forma de calcular precondiciones más débiles de Do. No existen muchas técnicas prácticas, que permitan calcular explícitamentela precondición más débil wp, por lo tanto historicamente ha sido más versatil usar las reglas de Hoare para obtener precondiciones, con lo cual se sacrifica la generalidad de las aserciones. En este trabajo se muestra como hacer este cálculo explícito de wp para una familia de algoritmos de punto fijo. Esta familia de algoritmos, junto con sus precondiciones más débiles, representan un framework para construir algoritmos de punto fijo correctos.