Please enable JavaScript.
Coggle requires JavaScript to display documents.
Verificación Formal de Programas - Coggle Diagram
Verificación Formal de Programas
Recordatorio propio
Conceptos e ideas sinmódulos
Recuerdo sobre el
manejo de la tripla de
Hoare {Q} S {R}
Verificación por [S] vacío
Basta con que Q ya implique
R: la instrucción no modifica
el estado
Verificación por asignación
(de Q a la PMD): var :=
<exp>, queda la fórmula
final R(var := <exp>)
Axioma de asignación: se
sustituye la variable por la
expresión en la postcondición
R
Verificación por condicional
(if / then / else)
Se comprueba por separado
cada rama de la decisión
Secuencia de instrucciones
donde
Se descompone [S] en n
triplas según las etapas para
alcanzar [R]: la verificación
se da por pasos
Regla de la composición: {Q}
S1 {P} y {P} S2 {R}
Ciclos
donde
Se agrega una invariante [P]
Se agrega una inicialización
Se agrega una variante que
decrece y garantiza la
terminación
Se distingue la corrección
parcial de la corrección
total
Términos
PMD: Precondición Más
Débil; predicado más
general que garantiza R
antes de ejecutar S
{Q} S {R}: tripla de
Hoare — Q es la
precondición, S el
proceso y R el resultado
(base axiomática, Hoare
1969)
Invariante [P]: propiedad
que se mantiene en cada
iteración del ciclo
Variante: expresión
acotada que decrece para
asegurar la terminación
Corrección parcial vs.
corrección total (esta
última incluye la
terminación)
Recorrer comparando e
intercambiando pares
vecinos
Se comparan elementos
consecutivos de izquierda
a derecha
Si la pareja está
desordenada, se
intercambia
En cada pasada el mayor
«burbujea» hasta su
posición final
Se repite hasta que ya no
hay intercambios (bastan
n-1 pasadas)
Pensar en el costo de
un algoritmo
El tiempo de ejecución se
expresa como T(n), según
el tamaño n de la entrada
(modelo RAM)
Lo decisivo es la tasa de
crecimiento, no las
constantes ni los
coeficientes
Se acota con O (cota
superior, peor caso), Ω
(cota inferior, mejor
caso) y Θ (cota ajustada)
El tiempo varía entre el
mejor caso (optimista) y
el peor caso (pesimista)
Resolver de abajo hacia
arriba reutilizando lo
ya calculado
Se evalúan ecuaciones de
recurrencia sin
recalcular subproblemas
Los resultados
intermedios se guardan en
memoria
Transforma soluciones
exponenciales en
polinómicas
Así, calcular Fibonacci
pasa de O(2^n) a Θ(n)
Conclusiones
Se hace dispendioso el
reemplazo absoluto de las
condiciones si el
programa es largo
Se recomienda el manejo
de leyes para la
factorización u
optimización en la
comprobación
Se pueden tener
escenarios donde el tipo
de instrucción sea por
asignación o vacío
Garantiza la corrección
sobre todos los estados
posibles, a diferencia de
las pruebas
Dividir el trabajo en dos
momentos afianzó el
aprendizaje del tema
Lecturas y material de apoyo
Medir y comparar la eficiencia de un algoritmo
Modelo RAM: cada operación básica cuesta 1; se cuenta cuántas se hacen → T(n)
Lo relevante es la tasa de crecimiento, no coeficientes ni términos menores
Mejor caso (optimista) vs peor caso (pesimista)
O (cota superior / peor caso), Ω (cota inferior / mejor caso), Θ (cota ajustada)
Descomponer en subproblemas, resolver recursivamente y combinar
Tres fases: división, conquista (casos base) y combinación
ordenamiento por mezcla → parte el arreglo en mitades, ordena cada una, las fusiona en orden
Recurrencia general: T(n) = a·T(n/b) + f(n)
Teorema maestro: compara c contra log_b(a) en tres casos para obtener la complejidad
Clasificar los problemas según su dificultad inherente
Problema de decisión: salida booleana (verdadero/falso)
Clase P: existe algoritmo O(nᵏ) → tratable
Clase NP: verificable en tiempo polinómico (certificado + verificador); máquina no determinista
Reducción de Karp: transformar en tiempo polinómico una instancia de un problema en otra
Tomar decisiones óptimas locales en cada etapa, sin reconsiderar
Resuelve por etapas; cada decisión es definitiva e independiente de las futuras
Cambio de monedas: con sistema canónico da el óptimo global; con uno no canónico puede quedar subóptimo
Codificación de Huffman: árbol por frecuencias, símbolos frecuentes → códigos más cortos, ningún código es prefijo de otro