Especificaciones Formales: Más Allá de las Instrucciones, Definiendo Comportamientos de Software
Esta publicación profundiza en la distinción entre especificaciones formales y programas tradicionales. Mientras que los programas son listas de instrucciones, las especificaciones formales son conjuntos de comportamientos. Usando un contador como ejemplo, el autor ilustra cómo las especificaciones definen todos los comportamientos correctos y utilizan la teoría de conjuntos, empleando generadores (Init y Next) para describir conjuntos infinitos de comportamientos. Esto contrasta con el concepto de no determinismo en la programación; en especificaciones formales, el no determinismo se refiere a las múltiples maneras en que un comportamiento puede extenderse, mientras que en los programas, se refiere a caminos de código inciertos. El artículo enfatiza la importancia de comprender las especificaciones formales como conjuntos de comportamientos, crucial para la depuración e interpretación de errores del verificador de modelos.