Please enable JavaScript.
Coggle requires JavaScript to display documents.
Verificacion Formal de Programas - Coggle Diagram
Verificacion Formal de Programas
Recordatorio propio
Conceptos e ideas sin modulos
Recuerdo sobre el manejo de Tripla de Hork
Verificacion por [S] vacio
Verificacion por asignacion de Q=> pmd (var:= <exp>,R) donde queda la formula final R(var:=<exp>)
Secuencia de intrucciones
donde
Se descompone [S] en x numero de triplas según aplique las etapas para alcanzar [R] así se daría la verificación por pasos.
Ciclos
donde
Se agrega una invariante [P]
Se agrega una inicializacion
Terminos
PMD: quiere decir Precondicion Mas Debil
{Q},{S},{R}: Tripla de Hork con Q es la precondicion, S es el proceso y R es el resultado
Conclusiones
Se hace dispendioso el reemplazo absoluto de las condiciones si el programa es largo
Se recomienda el manejo de leyes para la factorizacion u optimizacion en la resolucion de la comprobacion
Se pueden tener escenarios donde el tipo de instruccion sea por asignacion o vacio