Меня преследует TLA+
Подписан я на
Пару дней назад «Утренняя работа» предложила обсудить некую
работу. Статья обсуждает,
безусловно, интересные и актуальные вещи, но мое внимание привлекло то, что исследователи из Amazon
опять упоминают TLA+ — язык формальной спецификации систем
и идущая комплектом
Словом, прочитал несколько вводных статей и попробовал написать пару простеньких спецификацию.
Выяснилось, что TLA+ и компилируемый в него PlusCal позволяют описать систему и проверить ее на
предмет соответствия
Но почему все так ужасно с точки зрения эргономики программиста?!
Да что это я распинаюсь? Судите сами! Пример (простой):
---- MODULE transfer ---- EXTENDS Naturals, TLC (* --algorithm transfer variables alice_account = 10, bob_account = 10, account_total = alice_account + bob_account; process Transfer \in 1..2 variable money \in 1..20; begin Transfer: if alice_account >= money then A: alice_account := alice_account - money; bob_account := bob_account + money; end if; C: assert alice_account >= 0; end process end algorithm *) \* BEGIN TRANSLATION \* Label Transfer of process Transfer at line 12 col 3 changed to Transfer_ VARIABLES alice_account, bob_account, account_total, pc, money vars == << alice_account, bob_account, account_total, pc, money >> ProcSet == (1..2) Init == (* Global variables *) /\ alice_account = 10 /\ bob_account = 10 /\ account_total = alice_account + bob_account (* Process Transfer *) /\ money \in [1..2 -> 1..20] /\ pc = [self \in ProcSet |-> "Transfer_"] Transfer_(self) == /\ pc[self] = "Transfer_" /\ IF alice_account >= money[self] THEN /\ pc' = [pc EXCEPT ![self] = "A"] ELSE /\ pc' = [pc EXCEPT ![self] = "C"] /\ UNCHANGED << alice_account, bob_account, account_total, money >> A(self) == /\ pc[self] = "A" /\ alice_account' = alice_account - money[self] /\ bob_account' = bob_account + money[self] /\ pc' = [pc EXCEPT ![self] = "C"] /\ UNCHANGED << account_total, money >> C(self) == /\ pc[self] = "C" /\ Assert(alice_account >= 0, "Failure of assertion at line 16, column 4.") /\ pc' = [pc EXCEPT ![self] = "Done"] /\ UNCHANGED << alice_account, bob_account, account_total, money >> Transfer(self) == Transfer_(self) \/ A(self) \/ C(self) (* Allow infinite stuttering to prevent deadlock on termination. *) Terminating == /\ \A self \in ProcSet: pc[self] = "Done" /\ UNCHANGED vars Next == (\E self \in 1..2: Transfer(self)) \/ Terminating Spec == Init /\ [][Next]_vars Termination == <>(\A self \in ProcSet: pc[self] = "Done") \* END TRANSLATION MoneyNotNegative == money >= 0 MoneyInvariant == alice_account + bob_account = account_total ====
Уф… А книжку по языку все равно придется почитать.
Комментарии
Comments powered by Disqus