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 en 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]
Descripción general
Los lenguajes de especificación generalmente no se ejecutan directamente. Están destinados a describir el qué , no el cómo . De hecho, se considera un error si la especificación de un requisito está abarrotada 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 teóricas 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 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 prominente, describiendo las propiedades que las funciones deben satisfacer, a menudo solo 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 realmente puedan implementarse. 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 tuberías de Hartmann , cuando se aplican correctamente, pueden considerarse una especificación de flujo de datos que se puede ejecutar directamente. 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 la corrección del programa ( ver demostrador de teoremas ).
Idiomas
Ver también
Referencias
- ^ Joseph Goguen "Uno, ninguno, cien mil lenguajes de especificación" Documento invitado,Congreso IFIP 1986 págs. 995-1004
- ^ Fuchs, Norbert E .; Schwertel, Uta; Schwitter, Rolf (1998). "Intento de inglés controlado, no solo otro lenguaje de especificación lógica" (PDF) . Taller Internacional de Síntesis y Transformación de la Programación Lógica . Apuntes de conferencias en Ciencias de la Computación. 1559 . Saltador. págs. 1–20. doi : 10.1007 / 3-540-48958-4_1 . ISBN 978-3-540-65765-1.
- ^ Linden, Theodore; Lawrence Markosian (1989). "Síntesis transformacional usando refinar" . En Richer, Mark (ed.). Herramientas y técnicas de IA . Ablex. págs. 261-286. ISBN 0-89391-494-0. Consultado el 6 de julio de 2014 .