# Can TLAPS check any termination proofs?

• From: Lorin Hochstein <lor...@xxxxxxxxx>
• Date: Fri, 18 Jan 2019 19:04:02 -0800 (PST)

Is TLAPS capable (yet?) of checking a proof that an algorithm terminates?

In particular, consider the following simple algorithm:

----------------------------- MODULE CountDown -----------------------------

EXTENDS Naturals

CONSTANT N

ASSUME N \in Nat

(*

--fair algorithm CountDown {

variable i = N;

{

loop:

while (i>0) {

i := i-1

}

}}

*)

\* BEGIN TRANSLATION

VARIABLES i, pc

vars == << i, pc >>

Init == /\ i = N

/\ pc = "loop"

loop == /\ pc = "loop"

/\ IF i>0

THEN /\ i' = i-1

/\ pc' = "loop"

ELSE /\ pc' = "Done"

/\ i' = i

Next == loop \/ (pc = "Done" /\ UNCHANGED vars)

Spec == /\ Init /\ [][Next]_vars /\ WF_vars(Next)

Termination == <>(pc = "Done")

\* END TRANSLATION

THEOREM AlwaysTerminates == Spec => Termination

=============================================================================

Is it possible today to write a structured proof of the theorem AlwaysTerminates in a way that can be checked with TLAPS?

Lorin