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

Re: [tlaplus] TLA+ logic

I'm not sure what symbolic execution encompasses.  Complexity isn't the issue; it's expressiveness.  Complexity of an inexpressive language can be overcome with a lot of fairly easy work.  The partially developed symbolic model checker is BDD based.  BDD model checking essentially require static typing of the spec, which is in general impossible and which seems to be impossible in practice for a suitably general class of TLA+ specs.  However, a BDD model checker is possible because you don't have to statically type the spec--you just have to type a finite model of the spec.  That turns out to be possible in practice.  A BDD model checker for a fragment of TLA+ was built in one summer by an intern.  My understanding is that all the hard problems have been solved, and it just requires extending it to handle the full language.  But hard problems are usually hard to anticipate.


On Sunday, December 6, 2015 at 9:39:09 AM UTC-8, Ron Pressler wrote:
Thank you for the detailed response! 
There is no doubt that any proof system is probably too expensive for use in the industry, both because of the correctness requirements that are somewhat relaxed and because the systems tend to be more complicated than idealized algorithms. I was just interested in the more theoretical mathematical implications of the dependent-type vs set-theory approaches, just out of intellectual curiosity (now that I've started using TLA+, I'm interested in other approaches).

In any case, going on a tangent, I was surprised to read your mention of an incomplete symbolic model checker. After growing to enjoy TLA+ so much, that was the first thing that I thought would be a great addition, as it would allow checking of different kinds of specs, like sorting algorithms (a very interesting bug -- which only occurs on very large arrays -- was found in Java's sorting algorithm using the KeY project for symbolic execution) and order-dependent data structures like B-trees, where small models are ineffective. Any more information on this effort? It's the first time I hear of it. I would imagine that given TLA+'s simple and clear semantics, implementing symbolic execution would be easier than for something like Java.