Una especificación formal usa notación matemática para describir de manera precisa las propiedades que un sistema de información debe tener, sin preocuparse por la forma de obtener dichas propiedades. Describe lo que el sistema debe hacer sin decir cómo se va a hacer.^[1]​

Esta abstracción hace que las especificaciones formales sean útiles en el proceso de desarrollar un sistema, porque permiten responder preguntas acerca de lo que el sistema hace con confianza, sin la necesidad de tratar con una gran cantidad de información no relevante que se encuentra en el código de programa del sistema en un lenguaje de programación cualquiera, o especular sobre el significado de frases en un impreciso pseudocódigo.^[1]​

Una especificación formal pueden servir como un punto de referencia fiable para quienes se dedican a investigar sobre los requerimientos del cliente que solicita el sistema, o para que los desarrolladores de este sepan satisfacer esos requerimientos, y también para los que redactan manuales de instrucciones para el sistema. Debido a que es independiente del código del programa, las especificaciones formales de un sistema pueden ser elaboradas a principios de su desarrollo; y puede ser un medio valioso para promover un entendimiento común entre todos los interesados en el sistema.^[1]​

Ventajas de una Especificación formal

A continuación se detallan algunas de las ventajas de realizar una especificación formal para el desarrollo de un sistema:^[2]​

• Se proporciona información detallada sobre los requisitos del software y del diseño.
• Las especificaciones formales pueden ser analizadas matemáticamente y puede demostrarse la consistencia y completitud de la especificación; luego es posible demostrar que la implementación corresponde a la especificación.
• Las especificaciones formales pueden ser usadas como guía para el testing en la identificación de casos de prueba apropiados.
• Las especificaciones formales pueden ser procesadas usando herramientas de software, esto hace posible efectuar animaciones de la especificación, proveyendo de esta forma un prototipo del software.

Véase también

• Métodos formales
• Lenguajes formales
• Lenguajes de especificación
• Implementación de referencia