Re: [tlaplus] TLA+ logic

On 07 Dec 2015, at 11:23, Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx> wrote:

On Sunday, December 6, 2015 at 11:43:02 PM UTC+2, leuschel wrote:
Do you have a TLA+ spec of the flawed sorting algorithm ?

No, but the algorithm, as well as a formal specification of the broken assumed invariants and an account of the bug and its discovery, can all be found here.

I am also not sure what kind of symbolic execution you are after.
The answer of Leslie Lamport refers to BDD-based symbolic model checking.

I am not too sure either (as I am not well-versed in the taxonomy of formal methods), but the kind of symbolic execution used in KeY :) I believe it is not the same as BDD model-checking.
A tool that is able to automatically check sorting algorithms is a very powerful one to have in your toolbelt, as sorting algorithms -- like state machines -- are exemplars of a very large class of algorithms and data structures (heaps, B-trees and many other kinds of trees, other indexes in general), and if you can check them, you can probably check many interesting programs.

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.

Regards,

Stephan