Re: [tlaplus] Differences between TLA+ Specification and Property Based Testing

Hi Andrew,

welcome to the list, and it looks like you did a great job using PBT, and Hypothesis in particular. As to comparing Hypothesis (about which I know next to nothing) and TLA+, I believe that the comment [1] sums it up pretty well. TLA+ is intended for modeling and analyzing designs at a high level of abstraction, and the Die Hard puzzle just scratches the surface because there is not a lot to abstract from. TLA+ encourages you to abstract from real-world data structures (lists, heaps, priority queues, balanced trees or whatever) and replace them by mathematical concepts, in particular sets and functions. The most convincing use case for TLA+ is for modeling designs before you write any code.

The encouraging observation is that there is a convergence with high-level programming languages and their APIs that encourage you to think in terms of high-level concepts as well, before you commit to any specific implementation for efficiency's sake. I have no idea to what extent the Hypothesis system supports those APIs directly, but if it doesn't, I am confident that it or similar systems will go there at some point.

Personally, I don't think the "concurrency" aspect plays a big role here: note that TLA+ (unless other formalisms such as process algebras) does not have explicit constructs for concurrency but uses non-determinism, just like you state several "rules" in Hypothesis. (You cannot state fairness assumptions in PBT, but that's an advanced subject that is not as immediately relevant as safety properties are.)

My 2 cents,

Stephan

[1] link

On 12 Apr 2017, at 11:04, Andrew Gwozdziewycz <apg...@xxxxxxxxx> wrote:

Hi Folks,

First time poster, and newbie^1 to both TLA+ and property based testing (PBT from here on out), generally. Recently, a blog post was published (http://nchammas.com/writing/how-not-to-die-hard-with-hypothesis) about solving the Die Hard 3 Jug problem in Hypothesis (http://hypothesis.works)--a PBT library for Python. The fact that this was so straightforward was rather shocking to me, I have to admit!

It seems to me that the main advantage TLA+ / Pluscal has over PBT is the high-level mathematical pseudocode... But a few questions about this assumption:

1. The Jug implementation in Hypothesis shows that for *some* specifications, TLA+ and PBT are equivalent in what can be expressed / specified / assured. Is this *generally* true?

2. I'm thinking that the concurrency support in TLA+ might also be a huge advantage, but I think it's likely possible to simulate this in PBT, as well. Is there anything special about TLA+'s concurrency modeling that couldn't be replicated via PBT?

3. Generally, why should someone choose TLA+ over PBT? What other advantages does TLA+ have over PBT?

4. I think it's the case that intuition on creating invariants and properties for specifications / PBT tests, comes with experience. But, what tips do y'all have for recognizing (learning to intuit) that these types of specifications can have meaningful impact on code that I'm writing every day (mostly around distributed systems monitoring, REST APIs)?

Thanks for your time!

Andrew "Overjoyed by the potential of this stuff to make everything I touch better" Gwozdziewycz

[^1]: Meaning, I've read the AWS paper, watched the Leslie Lamport lecture series (1-3), the DrTLA Paxos lecture, and read through some specifications in the tlaplus github repo. For both TLA+, and PBT, I have some clarity in how I'd use it for testing certain types of algorithms, but have no clue yet how to apply either to work I generally do.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.