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 para un sistema. [1]
Los lenguajes de especificación generalmente no se ejecutan directamente. Su objetivo es describir el qué , no el cómo . Se considera un error si una especificación de requisitos está llena 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 orientado a propiedades para la especificación (adoptado, por ejemplo, por CASL ), las especificaciones de los programas consisten principalmente en axiomas lógicos , normalmente en un sistema lógico en el que la igualdad tiene un papel destacado, que describen las propiedades que las funciones deben satisfacer, a menudo simplemente por su interrelación. Esto contrasta con la denominada 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 especializarse 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 demostrador de teoremas ).
Medios relacionados con Lenguajes de especificación en Wikimedia Commons