Please enable JavaScript.

Coggle requires JavaScript to display documents.

Verificación Formal de Programas, Módulo: Análisis y verificación de…

- - - - Consiste en aplicar métodos basados en la lógica y las matemáticas con el fin de analizar el diseño y el código de un programa
- - - - Tipos de variables
        
        Variables de entrada
        
        Variables de salida
        
        Estado
    - - Definición y ejemplos
        
        Combinar postcondiciones en una sola
      - Aplicación en verificación formal
        
        Permite verificar múltiples aspectos del resultado final
      - Ejemplo
        
        (P) S (Q) && (P) S (R) => (P) S (Q && R)
    - - Definición
        
        Combinar precondiciones en una sola
      - Aplicación en verificación formal
        
        Facilita la verificación cuando cualquiera de varias condiciones iniciales puede ser verdadera
      - Ejemplo
        
        (P || R) S (Q) SI (P)S (Q) Y (R) S (Q)
    - - Precondición vacía
        
        Definición y ejemplos
        
        Precondición que siempre es verdadera
        
        Implicaciones de una precondición vacía
        
        El programa puede comenzar desde cualquier estado
        
        Ejemplo
        
        (false) S (Q) siempre es verdadero, sin importar Q
  - - - Definicion
        
        Condicion que debe ser verdadera antes de la ejecución de un programa
      - Rol
        
        Establece las condiciones necesarias
      - Ejemplo
        
        Para una funcion de division, la precondicion es que el divisor no se acero.
    - - Definición
        
        Condiciones que debe ser verdadera despues de la ejecucion del programa
      - Rol
        
        Verifica que el resultado cumple con la espesificacion
      - Ejemplo
        
        Una funcion de suma debe retornar la suma de los 2 parametros
    - - Tipos
        
        Enteros, bool, punto flotante
      - Gestión de vairables en verificacion
        
        Seguimiento del estado y cambios de variables durante la ejecuión
    - - Definicion
        
        Conjunto de valores de toas las variables en un momento dado
      - Implicaciones de una precondicion vacia
        
        El programa puede comenzar desde cualquier estado
      - Ejemplo
        
        (true) S (Q) significa que S puede ejecutarse sin ninguna especificacion
- - - - Instrucción vacía
        
        R
      - Asignacion
        
        R(x=E)
      - Instruccion condicional
        
        ((C ? wp(S1, R)) ? (C ? WP(S1, R)))
      - Composicion secuencial
        
        wp(S1, wp(S2, R))
- - - - Asegura la correccion parcial del ciclo
    - - Condicion que se mantiene verdadera antes y despues de cada iteracion
    - - En un bucle que suma elementos de un array, el invariante podría ser que la suma parcial es correcta hasta el indice actual
    - - En un bucle que suma los elementos de un array, un invariante puede ser sum == suma parcial hasta el indice i.
  - - - Expresion que disminute con cada iteracion del ciclo y eventualmente alcanza un valor limite
    - - Ayuda a demostrar la terminacion del ciclo
    - - Garantiza que el bucle no se ejecutara indefinidamente
    - - En un bucle que cuenta hacia abajo, la cota puede ser el valor del contador.
  - - - Asegura que un invariante se mantiene durante la ejecución de un ciclo
    - - Combinacion de invariante y cota para demostrar correcion y terminacion
    - - Verificación de la corrección de un bucle de ordenamiento por burbuja
- - - - Estudio de los recursos necesario (tiempo y espacio) para ejecutar un algoritmo
    - - Tiempo de ejecución
        
        Medida del tiempo que toma un algoritmo para completarse
      - Espacio de memoria
        
        Cantidad de memoria utilizada por un algoritmo
    - - Definicion
        
        Como varia el tiempo o el espacio requeriedo a medida que crece la entrada
      - Comparación de tasas de crecimiento
        
        Constante, lineal, cuadratica
      - Ejemplo
        
        Un algoritmo de busqueda lineal tiene una tasa de crecimiento lineal o(N)
    - - Definicion
        
        Mejor caso es el tiempo minimo de ejecucion; peor caso es el tiempo máximo
      - Importancia en el diseño de algoritmos
        
        Ayuda a entender el comportamiento del algoritmo en diferentes escenarios
      - Ejemplo
        
        Busqueda en un array ordenado - Mejor caso O(1) (elemento en el primer nidice), peor caso O(n) (elemento no encontrado)
    - - Ω (grande)
        
        Uso en analisis de algoritmos
        
        Ayuda a entender el rendimiento mínimo esperado
        
        Ejemplo
        
        Ω(n) para un algoritmo de búsqueda lineal.
        
        Definicion
        
        Representa el mejor caso de un algoritmo.
      - Θ (grande)
        
        Representa el caso promedio de un algoritmo
        
        Uso en análisis de algoritmos
        
        Da una visión completa del rendimiento
        
        Ejemplo
        
        Θ(n log n) para el algoritmo de ordenamiento rápido
      - O (grande)
        
        Uso en analisis de algoritmos
        
        Simplifica el estudio de la complejidad
        
        Ejemplo
        
        O(n^2) para un algoritmo de ordenamiento por burbuja.
        
        Definición
        
        Representa el peor caso de un algoritmo
    - - Descripcion del algoritmo
        
        Da una visión completa del rendimiento
        
        O(log n)
      - Analisis de complejidad
        
        Representa el caso promedio de un algoritmo
        
        Divide repetidamente el array a la mitad para encontrar un elemento
      - Mejor y peor caso
        
        Θ(n log n) para el algoritmo de ordenamiento rápido.
        
        Mejor caso O(1) (elemento en el medio), peor caso O(log n) (elemento no encontrado).
- - - - El sistema se modela y sus propiedades como teoremas matemáticos y se hace uso de un demostrador de teoremas interactivo para probar su valide
    - - Permite verificar propiedades complejas así como su adaptabilidad