Please enable JavaScript.
Coggle requires JavaScript to display documents.
VERIFICACIÓN FORMAL DE PROGRAMAS - Coggle Diagram
VERIFICACIÓN FORMAL DE PROGRAMAS
Conceptos Básicos
Estado de una Variable
Valor de una variable en un momento específico de la ejecución.
Estado de un Algoritmo
Valor de todas las variables en un momento determinado.
Aserción
Sentencias lógicas que representan un estado del sistema, mostrando relaciones entre valores de variables.
Especificación de un Programa
Precondición
Define el conjunto de estados iniciales válidos.
Postcondición
Define el conjunto de estados finales aceptados.
Programa y Estado del Programa
La información del programa es representada por variables (entrada/salida).
Conjunto de valores que toman las variables en un momento dado.
Matemáticas
Explicación
Se enfoca en el "por qué" de una afirmación.
Convicción
Basada en la demostración de enunciados y conjeturas.
Método de Sistematización
Simplificación de teorías organizando enunciados.
Verificación de Modelos
Confirma si el modelo matemático es finito o infinito.
Características
Teorema de Invarianza
Conjunto de reglas para decidir si un programa es correcto.
Ser "FINITO"
Debe ser preciso e indicar el orden de cada paso.
Propiedades
Estar Bien Definido
Entrada
Salida
Invariante
Es un predicado que se cumple en el estado del programa en cada iteración.
Cota de Ciclo
Función entera que disminuye en cada iteración del ciclo, indicando el fin del proceso.
Ordenamiento por mezcla
Algoritmo basado en divide y vencerás.
Pasos:
Dividir en mitades hasta que cada subarreglo tenga un solo elemento.
Ordenar y combinar las mitades.
Complejidad: O(n log n).
Aplicaciones:
Optimización con otros algoritmos.
Programación dinámica
Técnica para resolver problemas dividiéndolos en subproblemas más pequeños.
Características:
Subestructura óptima: soluciones construidas a partir de subproblemas.
Solapamiento de subproblemas: se resuelven varias veces.
Tipos:
Memorización (top-down).
Iterativo (bottom-up).
Ejemplos:
Mochila.
Floyd-Warshall.
LCS.
Teorema maestro
Forma general: T(n) = aT(n/b) + O(n^d).
a: Número de subproblemas.
b: Factor de reducción.
Ejemplo:
Ordenamiento por mezcla:
T(n) = 2T(n/2) + O(n).
Solución: O(n log n).