Revisita a la Técnica de Derivación de Invariantes “Reemplazo de Constante por Variable”

Revisit the Invariant Derivation Technique “Replacement of Constant by Variable”

Resumen

Dijkstra definió el transformador de predicados  (weakest precondition), y en dicha definición establece para la instrucción de iteración Do un predicado  que describe los estados iniciales que hacen que el ciclo itere a lo sumo  veces, satisfaciendo la postcondición . En trabajos recientes se han determinado técnicas para calcular explícitamente , lo cual representa una alternativa a la regla de Hoare del invariante. En este trabajo se demuestra que la técnica de derivación de algoritmos de Dijkstra denominada “reemplazo de constante por variable”, genera invariantes que son equivalentes a   para algún , cuando  satisface ciertas condiciones.