Меня преследует TLA+
Подписан я на блог-рассылку The Morning Paper, автор которой разбирает интересные классические или новые научные публикации на околоайтишные темы: распределенные системы, языки программирования, базы данных и так далее.
Пару дней назад "Утренняя работа" предложила обсудить некую работу. Статья обсуждает, безусловно, интересные и актуальные вещи, но мое внимание привлекло то, что исследователи из Amazon опять упоминают TLA+ - язык формальной спецификации систем и идущая комплектом программа-верификатор.
Словом, прочитал несколько вводных статей и попробовал написать пару простеньких спецификацию.
Выяснилось, что TLA+ и компилируемый в него PlusCal позволяют описать систему и проверить ее на предмет соответствия каким-то требованиям или инвариантам. Тут все вкусно, питательно и полезно.
Но почему все так ужасно с точки зрения эргономики программиста?!
Во-первых, почему оно работает только через какую-то дубовую среду разработки (TLA Toolbox)?! Причем среда-то не особо помогает, но зато прячет обычные консольные программы.
Во-вторых, реализация дуализма TLA+/PlusCal. Ну ладно, что там два языка (читаемый PlusCal компилируется в нечитаемый TLA+). Но кому пришла в голову мысль о том, что PlusCal пишется прямо в комментариях TLA? И код этот ракрывается на лету интегрированной средой?! Прямо Java образца 2005 года, с ее адскими генераторами XML.
В-третьих, кому (тому самому Лэсли Лампорту, на секундочку) пришла в голову мысль о двух синтаксисах в PlusCal?! 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 ====
Уф... А книжку по языку все равно придется почитать.
