Objetivos
  • Especificar problemas por medio de precondiciones y postcondiciones usando un lenguaje formal (en nuestro caso, lógica de primer orden con números enteros, secuencias, reales, booleanos, strings, sumatorias, productorias y “cuentatorias”).
  • Razonar sobre la corrección de programas imperativos, incluyendo transformaciones de estados y usos informales del teorema de alternativas y del teorema del invariante.

  • Conocer la teoría de demostraciones formales usando precondición más débil, incluyendo las versiones formales del teorema de alternativas y del teorema del invariante.

  • Conocer y desarrollar algoritmos sobre secuencias, incluyendo búsqueda binaria, algoritmos cuadráticos de ordenamiento de arreglos y otros algoritmos interesantes sobre arreglos y matrices.