PlusCal

PlusCal (anteriormente llamado +CAL ) es un lenguaje de especificación formal creado por Leslie Lamport , que se transpila a TLA ⁺ . A diferencia del enfoque orientado a la acción de TLA ⁺ en sistemas distribuidos , PlusCal se asemeja más a un lenguaje de programación imperativo y es más adecuado para especificar algoritmos secuenciales . ^[¹^] PlusCal fue diseñado para reemplazar el pseudocódigo , conservando su simplicidad a la vez que proporciona un lenguaje formalmente definido y verificable. ^[²^] Un reloj de un bit se escribe en PlusCal de la siguiente manera:

-- algoritmo justo OneBitClock { reloj variable \in {0, 1}; { mientras (VERDADERO) { si (reloj = 0) reloj := 1 demás reloj := 0 } } }

Véase también

↑ Lamport, Leslie (28 de febrero de 2015). Principios y especificaciones de sistemas concurrentes . pág. 7. Consultado el 10 de mayo de 2015. PlusCal es más conveniente que TLA ⁺ para describir el flujo de control en un algoritmo . Esto generalmente lo hace mejor para especificar algoritmos secuenciales y algoritmos multiproceso de memoria compartida.
↑ Lamport, Leslie (2 de enero de 2009). "El lenguaje de algoritmos PlusCal" (PDF) . Aspectos teóricos de la computación - ICTAC 2009. Notas de clase en ciencias de la computación. Vol. 5684. Springer Berlin Heidelberg. págs. 36–60 . doi : 10.1007/978-3-642-03466-4_2 . ISBN 978-3-642-03465-7Consultado el 10 de mayo de 2015 .

Las herramientas y la documentación de PlusCal se encuentran en la página del lenguaje de algoritmos de PlusCal .