Hispanopedia Wiki
Articulo de referencia

Lenguaje de especificación

Un lenguaje de especificación es un lenguaje formal en ciencias de la computación que se utiliza durante el análisis de sistemas , el análisis de requisitos y el diseño de siste...

Hispanopedia WikiContenido en espanolLectura gratuita

Un lenguaje de especificación es un lenguaje formal en ciencias de la computación 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 ]

Descripción general

Los lenguajes de especificación generalmente no se ejecutan directamente. Están diseñados para describir el qué , no el cómo . [ 2 ] Se considera un error si una especificación de requisitos está sobrecargada de detalles de implementación innecesarios.

Una suposición fundamental común en muchos enfoques de especificación es que los programas se modelan como estructuras algebraicas o basadas en la teoría de modelos , que incluyen una colección de conjuntos de valores de datos junto con funciones sobre dichos conjuntos. Este nivel de abstracción coincide con la idea 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 especificación orientado a propiedades (como el adoptado por CASL , por ejemplo ), las especificaciones de los programas consisten principalmente en axiomas lógicos , generalmente en un sistema lógico donde la igualdad desempeña un papel fundamental, que describen las propiedades que deben satisfacer las funciones, a menudo simplemente por su interrelación. Esto contrasta con la denominada especificación orientada a modelos en marcos como VDM y la notación Z , que consiste en una simple realización del comportamiento requerido.

Las especificaciones deben someterse a un proceso de refinamiento (la incorporación de detalles de implementación) antes de poder implementarse. El resultado de dicho proceso es un algoritmo ejecutable, formulado 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 directamente ejecutable . Otro ejemplo es el modelo de actores , que carece de 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 de programas ( véase demostrador de teoremas ).

Idiomas

Véase también

Referencias

  1. ↑ Joseph Goguen , "Uno, ninguno, cien mil lenguajes de especificación", artículo invitado, Congreso IFIP 1986, págs. 995–1004.
  2. ↑ Hayes, IJ; Jones, CB (noviembre de 1989). "Las especificaciones no son (necesariamente) ejecutables" . Software Engineering Journal . 4 (6). doi : 10.1049/sej.1989.0045 .
  3. ↑ Fuchs, Norbert E.; Schwertel, Uta; Schwitter, Rolf (1998). «Attempto Controlled English—not just another logic specification language» (PDF) . Taller internacional sobre síntesis y transformación de programación lógica . Lecture Notes in Computer Science. Vol. 1559. Springer. pp. 1–20 . doi : 10.1007/3-540-48958-4_1 . ISBN   978-3-540-65765-1.
  4. ↑ "El lenguaje de métodos formales más sencillo jamás creado para desarrolladores que diseñan sistemas distribuidos, microservicios y aplicaciones en la nube" . Consultado el 28 de mayo de 2024 .
  5. ↑ Linden, Theodore; Lawrence Markosian (1989). «Síntesis transformacional mediante Refine» . En Richer, Mark (ed.). Herramientas y técnicas de IA . Ablex. págs. 261–286 . ISBN  0-89391-494-0Consultado el 6 de julio de 2014 .
  • Logotipo de Wikimedia CommonsContenido multimedia relacionado con lenguajes de especificación en Wikimedia Commons.