A simple proof

The invariant

Intuitively, the theorem Correctness holds because the implementation guarantees the following invariant

That is, InductiveInvariant holds for the initial state (i.e., the state specified by Init) and is preserved by the next-state relation [Next]_<<x,y>>.

Checking proofs

First we need to assume that constants M and N are not equal to zero.

Let us then prove that InductiveInvariant holds for the initial state.

To check wether TLAPS can prove that theorem by itself, we declare its proof obvious.

We can now ask TLAPS to prove that theorem, by right-clicking on the line of the theorem (or use the ctrl+G,ctrl+G / cmd-G,cmd-G shortcut), as shown in the following screenshot:

But TLAPS does not know how to prove the proof obligation corresponding to that proof. As you can see in the following screenshot, it prints that obligation and reports failures of three backends, Zenon, Isabelle, and SMT. The default behavior of TLAPS is to send obligations first to an SMT solver (by default Z3), then if that fails to the automatic prover Zenon, then if Zenon fails to Isabelle (with the tactic "auto"). See the tactics section to learn more about this process.

Using facts and definitions

As you can see, the obligation cannot be proved because TLAPS treats the symbols Init and InductiveInvariant as opaque identifiers unless it is explicitly instructed to expand their definitions using the directive DEF. The main purpose of this treatment of definitions is to make proof-checking tractable, because expanding definitions can arbitrarily increase the size of expressions. Explicit use of definitions is also a good hint to the (human) reader to look only at the listed definitions to understand a proof step. In that precise case, we can ask TLAPS to expand definitions of Init and InductiveInvariant, by replacing the proof OBVIOUS by the proof BY DEF Init, InductiveInvariant. You can see that, in the obligation sent to the backends, the definitions of Init and InductiveInvariant have been expanded:

Unfortunately, the theorem is still colored red, meaning that none of the back-ends could prove that obligation. As with definitions, we have to specify which facts are usable. In this case, we have to make the fact NumberAssumption usable by changing the proof to:

The general form of a BY proof is:

BY e₁, …, e_m DEF d₁, …, d_n

which claims that the assertion follows by assuming e₁, …, e_m and expanding the definitions d₁, …, d_n. It is the job of TLAPS to then check this claim, and also to check that the cited facts e₁, …, e_m are indeed true.

Finally, SMT succeeds in proving that obligation and the theorem gets colored green:

Summary