MÉTODOS FORMALES.  

UNA MIRADA PRACTICA

¿Qué es un Método Formal?

Método formal es cualquier técnica que trate la construcción y/o el análisis de modelos matemáticos

que contribuyen a la automatización del desarrollo de sistemas informáticos.

Uso del lenguaje Z

Las especificaciones en Z se estructuran como un conjunto de esquemas. Un esquema es, en esencia, una especificación formal análoga a la subrutina o el procedimiento de un lenguaje de programación.

La notación Z está basada en la teoría de conjuntos con tipos y en la lógica de primer orden. Z proporciona una estructura denominada esquema, para describir el estado y las operaciones de una especificación.

Operación - Reiniciar bloques

Pre-condicion: Que la cantidad de elementos de la cola de bloques sea mayor a 0

♯ColaBloques > 0

Post-condicion: Los todos elementos de la cola de bloques pasaran a libres, quedando la cola de bloques vacia para sus nuevas operaciones.

libres′= libres ⋃ ColabloquesA

ColaBloquesA′ = ∅

  Reiniciar Bloques                                                                                                

AGestorBloques

♯ ColaBloques > 0

libres′ = libres ⋃ ColaBloquesA

ColaBloquesA′ = ∅