Un lenguaje de especificación es un lenguaje formal en informática que se utiliza durante el análisis de sistemas , el análisis de requisitos y el diseño de sistemas para describir un sistema a un nivel mucho más alto que un lenguaje de programación , que se utiliza para producir el código ejecutable de un sistema. [1]
Los lenguajes de especificación generalmente no se ejecutan directamente. Están destinados a describir el qué , no el cómo . Se considera un error si una especificación de requisitos está repleta de detalles de implementación innecesarios.
Un supuesto fundamental común de muchos enfoques de especificación es que los programas se modelan como estructuras algebraicas o de teoría de modelos que incluyen una colección de conjuntos de valores de datos junto con funciones sobre esos conjuntos. Este nivel de abstracción coincide con la opinión de que la corrección del comportamiento de entrada/salida de un programa tiene prioridad sobre todas sus demás propiedades.
En el enfoque de la especificación orientado a las propiedades (adoptado, por ejemplo, por CASL ), las especificaciones de los programas consisten principalmente en axiomas lógicos , generalmente en un sistema lógico en el que la igualdad tiene un papel destacado, describiendo las propiedades que las funciones deben satisfacer, a menudo simplemente por su interrelación. Esto contrasta con la llamada especificación orientada a modelos en marcos como VDM y Z , que consisten en una simple realización del comportamiento requerido.
Las especificaciones deben estar sujetas a un proceso de refinamiento (el llenado de los detalles de implementación) antes de que puedan implementarse realmente. El resultado de dicho proceso de refinamiento es un algoritmo ejecutable, que se formula en un lenguaje de programación o en un subconjunto ejecutable del lenguaje de especificación en cuestión. Por ejemplo, las canalizaciones Hartmann , cuando se aplican correctamente, pueden considerarse una especificación de flujo de datos que es directamente ejecutable. Otro ejemplo es el modelo de actor que no tiene contenido de aplicación específico y debe estar especializado para ser ejecutable.
Un uso importante de los lenguajes de especificación es permitir la creación de pruebas de corrección del programa ( ver probador de teoremas ).
Medios relacionados con los lenguajes de especificación en Wikimedia Commons