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

Re: [tlaplus] TLA+ logic

On Monday, December 7, 2015 at 2:19:25 PM UTC+2, Stephan Merz wrote:

Let's just try to be clear about terminology: KeY is an interactive theorem prover that includes an expansion strategy based on symbolic execution (typically, for unfolding a recursive call of a method). The user experience of writing proofs in KeY is closer to writing a TLA+ proof using TLAPS than calling a model checker or constraint solver, which are fully automatic. In particular, KeY requires inductive invariants, and can prove correctness for arbitrary instances.

You are absolutely right. I was under the false impression that KeY is an automatic tool.