PlusCal

PlusCal (wcześniej nazywany +CAL ) to formalny język specyfikacji stworzony przez Lesliego Lamporta , który przekłada się na TLA ⁺ . W przeciwieństwie do zorientowanego na działanie TLA +, skupiającego ^się na systemach rozproszonych , PlusCal najbardziej przypomina imperatywny język programowania i lepiej nadaje się do określania algorytmów sekwencyjnych . PlusCal został zaprojektowany w celu zastąpienia pseudokodu , zachowując swoją prostotę, zapewniając jednocześnie formalnie zdefiniowany i weryfikowalny język. Zegar jednobitowy jest zapisywany w PlusCal w następujący sposób:

-- uczciwy algorytm OneBitClock { zmienny zegar \in {0, 1}; { while (PRAWDA) { if (zegar = 0) zegar := 1 else zegar := 0 } } }

Zobacz też

Linki zewnętrzne

Narzędzia i dokumentacja PlusCal znajdują się na stronie języka algorytmów PlusCal .