Меня преследует 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

====

Уф… А книжку по языку все равно придется почитать.