Las inicializaciones del mientras vienen dadas según la llamada inicial.
DERIVACIÓN ITERATIVA DIRECTA
El núcleo del invariante va a ser, en muchos casos, una versión debilitada de la postcondición. Una vez conseguido un invariante, se continúa diseñando instrucciones protegidas que lo mantengan, y a su vez avancen hacia la terminación. El avance ha de consistir en el decrecimiento de la correspondiente función de cota, con valor en los naturales. Se detecta que se han cubierto suficientes casos cuando se puede deducir la postcondición a partir del invariante y el cierre de todas las protecciones
Autor:
Pablo Turmero
| Página siguiente |