Hispanopedia Wiki
Articulo de referencia

Lógica temporal de las acciones

La lógica temporal de acciones ( TLA ) es una lógica desarrollada por Leslie Lamport que combina la lógica temporal con una lógica de acciones . Se utiliza para describir el com...

Hispanopedia WikiContenido en espanolLectura gratuita

La lógica temporal de acciones ( TLA ) es una lógica desarrollada por Leslie Lamport que combina la lógica temporal con una lógica de acciones . Se utiliza para describir el comportamiento de sistemas concurrentes y distribuidos . Es la lógica subyacente al lenguaje de especificación TLA+ .

Detalles

Las afirmaciones en la lógica temporal de las acciones son de la forma[A]t{\displaystyle [A]_{t}}, donde A es una acción y t contiene un subconjunto de las variables que aparecen en A. Una acción es una expresión que contiene variables con prima y sin prima, comoincógnita+incógnita′∗y=y′{\displaystyle x+x'*y=y'}El significado de las variables sin prima es el valor de la variable en este estado . El significado de las variables con prima es el valor de la variable en el siguiente estado . La expresión anterior significa que el valor de x hoy , más el valor de x mañana multiplicado por el valor de y hoy , es igual al valor de y mañana .

El significado de[A]t{\displaystyle [A]_{t}}Esto implica que o bien A es válida ahora, o bien las variables que aparecen en t no cambian. Esto permite pasos intermitentes, en los que ninguna de las variables del programa cambia de valor.

Lenguajes de especificación

Existen varios lenguajes de especificación que implementan la lógica temporal de acciones. Cada lenguaje tiene características y casos de uso únicos:

TLA+

TLA+ es el lenguaje de especificación predeterminado y más utilizado para TLA. Es un lenguaje matemático diseñado para describir el comportamiento de sistemas concurrentes y distribuidos. La especificación está escrita en estilo funcional.

----------------------------- MÓDULO Reloj ----------------------------- EXTENDS Naturals VARIABLES hora Inicialización == hora = 1 Siguiente == hora' = SI hora = 12 ENTONCES 1 SINO hora + 1 Especificación == Inicializar /\ [][Siguiente]_hora =============================================================================

PlusCal

PlusCal es un lenguaje de algoritmos de alto nivel que se traduce a TLA+. Permite a los usuarios escribir algoritmos con una sintaxis similar al pseudocódigo, que luego se convierte automáticamente en especificaciones TLA+. Esto hace que PlusCal sea ideal para quienes prefieren pensar en términos de algoritmos en lugar de máquinas de estados.

----------------------------- MÓDULO Reloj ---------------------- EXTENDS Naturals (*--algoritmo Reloj de hora { variable hora = 1; { mientras (VERDADERO) { hora := (hora % 12) + 1; } } } --*)

Quinta

Quint es otro lenguaje de especificación que se traduce a TLA+. Combina la sólida base teórica de la Lógica Temporal de Acciones (TLA) con herramientas de desarrollo y verificación de tipos de última generación. A diferencia de PlusCal, los operadores y palabras clave de Quint tienen una traducción uno a uno a TLA+. Quint ofrece un REPL, un simulador aleatorio e integración con los verificadores de modelos TLA+.

módulo reloj_de_hora { var hora: int acción inicial = hora' = 1 paso de acción = hora' = si (hora == 12) 1 sino hora + 1 }

FizzBee

FizzBee [ 1 ] es una alternativa a TLA+ con un lenguaje de especificación de alto nivel que utiliza una sintaxis similar a la de Python ( Starlark ), diseñado para brindar métodos formales a los ingenieros de software convencionales que trabajan en sistemas distribuidos. Si bien se basa en la Lógica Temporal de Acciones, no traduce ni utiliza TLA+ internamente, a diferencia de PlusCal o Quint.

Acción inicial : hora = 1acción atómica Tick : # El cuerpo de las acciones es Starlark (un dialecto de Python) hora = ( hora % 12 ) + 1

Véase también

Referencias

  1. ↑ "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 .
  • Lamport, Leslie (2002). Especificación de sistemas: El lenguaje TLA + y herramientas para ingenieros de hardware y software . Addison-Wesley. ISBN 0-321-14306-X.
  • Leslie Lamport (16 de diciembre de 1994), Introducción a TLA (PDF) , consultado el 17 de septiembre de 2010.
  • "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 .
  • Sitio web oficial
  • "Sistema de prueba TLA+" . INRIA .
  • Lamport, Leslie (2014). "Pensando para programadores" . Una introducción sencilla a TLA+ en Build.
  • "Sitio web de FizzBee" .
  • "Repositorio git de Quint" . GitHub .