TLA+

Intentions are often incomplete and inconsistent. Specifying intentions using TLA+ (Temporal Logic Of Actions) can help. Also, verification of the completeness and consistency of TLA+ specifications can be automated!

TLA+ cannot verify specifications correspond to correct models. It also cannot verify or generate implementations. However, TLA+ specifications often suggest powerful proofs and theorems.

Here is an example TLA+ specification for account transfers:

---- MODULE account_transfers ----

EXTENDS Naturals, TLC

(* --algorithm account_transfers

\*******************************************************************************

variables send_bal    =    10,
          recv_bal    =    10,
          total_bal   =    20,
          trans_amt \in 1..20;

begin \*************************************************************************

a: if send_bal >= trans_amt then
b:         send_bal := send_bal - trans_amt;
           recv_bal := recv_bal + trans_amt;
   end if;

end algorithm *) \**************************************************************

SendBal == send_bal            >= 0
RecvBal == recv_bal            >= 0
SumBal  == send_bal + recv_bal  = total_bal

==== \**************************************************************************