Please enable JavaScript.
Coggle requires JavaScript to display documents.
Entrega 1 Verificación de algoritmos, Entrega Final Verificación de…
Entrega 1 Verificación de algoritmos
Entrega Final Verificación de algortimos
Trabajo realizado por
Harold Senider Alvarez Carrillo
Andres Felipe Chacon Cifuentes
Referencias
Material del Politécnico Grancolombiano
Dasgupta et al. (2006) – Algorithms
Cormen et al. (2009) – Introduction to Algorithms
Kaldewaij (1990) – Derivación de algoritmos
Hoare (1969) – Lógica de Hoare
Conclusiones
Elige el diseño algorítmico adecuado según el problema
Garantiza corrección, eficiencia y finitud
La verificación formal supera las pruebas empíricas
Complejidad Computacional
Reducción de Karp
Si A ≤ B y B ∈ P ⇒ A ∈ P
Transformación en tiempo polinomial
Clases:
NP-Completo: no se sabe si son tratables
NP: verificables en tiempo polinomial
P: resolubles en tiempo polinomial
Problemas de Decisión - Salida booleana: sí/no
Algoritmos Voraces
Ejemplo 2: Codificación de Huffman - Asocia códigos binarios más cortos a símbolos frecuentes
Ejemplo 1: Cambio de monedas - Minimiza número de monedas
Decisiones óptimas locales en cada paso
Técnicas de Diseño de Algoritmos
Programación Dinámica
Ejemplo: fib(n)
F[1] := 1
F[0] := 0
Usa memoria para evitar cálculos repetidos
Dividir y Conquistar
Usa Teorema Maestro para T(n)
Ejemplo: Merge Sort
Divide en subproblemas, resuelve y combina
Análisis de Algoritmos
Tasa de crecimiento - 2ⁿ > n² > n
Notación asintótica - O(n), Θ(n), Ω(n)
Casos:
Peor caso
Mejor caso
Tiempo de ejecución T(n) - Cuántas operaciones básicas realiza
Programas Iterativos
Ejemplo:
Cota: t = (n + 1) - i
Invariante: suma = suma(1..i-1), i ∈ [1, n+1]
Teorema de Invarianza
El ciclo termina (cota alcanza mínimo)
P ∧ ¬condición ⇒ poscondición
P se mantiene por iteración
P se cumple al inicio
Cota del ciclo - Función que decrece hasta terminar
Invariante de ciclo - Se mantiene antes y después de cada iteración
Precondición más Débil - Deriva el estado mínimo necesario para que se cumpla la poscondición
Aplicaciones:
Secuencia: wp(S1; S2, R) ≡ wp(S1, wp(S2, R))
Condicional: wp(if C then A else B, R) ≡ (C ⇒ wp(A, R)) ∧ (¬C ⇒ wp(B, R))
Asignación: wp(x:=E, R) ≡ R[x := E]
Vacía: wp(⌀, R) ≡ R
Fundamentos de la Verificación
Triplas de Hoare
Demuestran formalmente la corrección del programa
Sintaxis: {Q} S {R}
Especificación de programas
Ejemplo: {Pre: a ≥ 0 ∧ b ≥ 0} mcd(a,b) {Pos: a = MCD(A,B)}
Uso de variables semánticas
Precondición y poscondición