Es una especificación escrita en notación formal. Es una expresión que utiliza una síntaxis y semántica determinada que esta predefinida. Estos lenguajes están basados en conceptos matemáticos. La ventaja de esta metodología es que no tiene ambigüedad y reduce los costes de pruebas.

No se suele usar por que a partir de los 80 aparece la calidad y la agilidad, lo que resulta en una disminución de la documentación Estas técnicas formales no se adaptan bien a interfaces de usuario y no son escalables, están muy limitadas.

Al estar basadas en formalismos matemáticos son fáciles de corregir, pero difíciles de comprender y usar.

Con la especificación formal las fases de especificación y diseño reducen su coste.

Nos permite especificar componentes que vamos a utilizar y luego agrupar. Las interfaces se conocen como Tipos Abstractos de Datos u objetos en caso de Programación orientada a Objetos. Tiene una estructura predeterminada:

• Introducción
• Descripción: Define que hace la especificación (Funciones o Métodos)
• Signaturas: Define la Sintaxis de dichas operaciones (Atributos)
• Axiomas: Plan de pruebas, se especifica que pasa o como reaccionan las funciones y capturas de excepciones.

Introducción

• Especificación basada en modelos:
  • Permite especificar los comportamientos del sistema
  • Especifica las notaciones (VDM, B y Z)
• Especificaciones algebraicas

Notación Z Los sistemas se modelan usando conjuentos y relaciones entre conjuentos +Las epsecificaciones se presentan como texto informal