Lenguaje de especificación

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.

Resumen

Los lenguajes de especificación generalmente no se ejecutan directamente. Su objetivo es describir el qué, no el cómo. De hecho, se considera un error si una especificación de requisitos está repleta de detalles de implementación innecesarios.

Una suposición 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 otras propiedades.

En el enfoque de especificación orientado a la propiedad (tomado, 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, que describe 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 de 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 un contenido de aplicación específico y debe ser 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).

Idiomas