[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

What is the purpose of THEOREM in AsynchInterface?

I'm reading the "Specifying Systems" book and was wondering what is the purpose of the theorem definition on the last line in the AsynchInterface module (page 27)?

When configuring the model with Spec as the Temporal formula and TypeInvariant as an invariant to check, running the TLC model checker finds no errors. Removing the THEOREM definition seems to have no impact on the outcome of the checks. Is it for readability purposes only?

What am I missing?

Thank you for helping,
- Nikola