Differences between TLA+ Specification and Property Based Testing

[Andrew Gwozdziewycz]

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.

[Stephan Merz]

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

--
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...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Andrew Gwozdziewycz]

Hi Stephan,

Thanks for the response!

On Wed, Apr 12, 2017 at 1:09 PM, Stephan Merz <stepha...@gmail.com> wrote:
> Hi Andrew,
>
> welcome to the list, and it looks like you did a great job using PBT, and
> Hypothesis in particular.

I definitely didn't write that blog post. :)

> 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.

I think, maybe, the thing to consider is:

- Design your system in TLA+/PlusCal.
- Verify the implementation meets the design with Property Based
Testing, by reusing the properties and invariants you uncovered in
TLA+/PlusCal.

This seems like a very very powerful combination!

> 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.)

Hmm. Ok, thanks for the clarification!

--
http://www.apgwoz.com

[Hillel Wayne]

Hi Andrew,

I like to think I'm both reasonably familiar with both Hypothesis and TLA+, although TLA+ moreso, so hopefully I can speak to some of your questions. I think the main thing to understand here is that the diehard problem is (in my opinion) not quite the problem domain for Hypothesis.

Hypothesis is a kind of one level above standard unit testing. Instead of testing that an input matches an output, you test that for a range of inputs, all of the outputs have a property. For example, given imagine we had a function badsort that sorts a list.

def badsort(array):

    if not array:

     return []

    lesser = badsort([x for x in array if x < array[0]])

    greater = badsort([x for x in array if x > array[0]])

    return lesser + [array[0]] + greater

We could write some unit tests that happily pass:

assert badsort([]) == []

assert badsort([1,3,2]) == [1,2,3]

When we use property-based testing, though, we ask "what are properties of the outputs that are true for all inputs?" One of them, for example, is that sorting a sorted list returns the original list. Another is that a sorted list has the same size as the original list. Here's how we'd write them in Hypothesis:

from hypothesis import given, assume

import hypothesis.strategies as st

int_list = st.lists(st.integers())

@given(int_list)

def test_idempotent(numbers):

    assert badsort(badsort(numbers)) == badsort(numbers)

    

@given(int_list)

def test_preserves_length(numbers):

    assert len(badsort(numbers)) == len(numbers)

The first property test passes, but the second test finds a counterexample: our invariant fails for [0, 0]! So the property found a bug in our code which corresponded to an edge case we didn't realize we should check.

On the other hand, TLA+ is a specification language. It's designed for building a model of your system outside of any particular code. You can't directly test your function with it, but you can test the algorithm your function implements. It's a little harder to give a toy example that clearly demonstrates why TLA+ is so powerful, but if you're interested I wrote an essay on how I've used it in production. And even that example is just at the PlusCal level; you can do much cooler stuff than I've done.

Hope that helps! I'd personally recommend using both TLA+ and PBT, because they're both really good at what they do.

Hillel

[Andrew Gwozdziewycz]

On Thu, Apr 13, 2017 at 12:28 PM, Hillel Wayne <hwa...@gmail.com> wrote:
> Hi Andrew,
>
> I like to think I'm both reasonably familiar with both Hypothesis and TLA+,
> although TLA+ moreso, so hopefully I can speak to some of your questions. I
> think the main thing to understand here is that the diehard problem is (in
> my opinion) not quite the problem domain for Hypothesis.

Yes! It obviously seemed like a hack! But, then again, it's pretty
much the equivalent of your Hanoi example on learntla.com!

Sure.

> On the other hand, TLA+ is a specification language. It's designed for
> building a model of your system outside of any particular code. You can't
> directly test your function with it, but you can test the algorithm your
> function implements. It's a little harder to give a toy example that clearly
> demonstrates why TLA+ is so powerful, but if you're interested I wrote an
> essay on how I've used it in production. And even that example is just at
> the PlusCal level; you can do much cooler stuff than I've done.

Yeah! Finding real world examples, and how to apply TLA+ to them is
difficult. The AWS paper talks about the benefits, but not the *what*
or *how*. I'll take a look at your essay, it's been in my queue for a
while to go back to now that I have a bit more understanding.

I think (hope?) that exposing myself to more examples of TLA+ will
help guide an intuition of *how* to use it for my day job. As Leslie
suggested (in his ongoing lecture series, I think?) TLA+ is a
different way of thinking, and I don't yet think that way.

> Hope that helps! I'd personally recommend using both TLA+ and PBT, because
> they're both really good at what they do.

Yes! I definitely am seeing this more and more to be the case, and
figuring out how to leverage both of them effectively... and then
convince others to do the same at work, will be an interesting
adventure!

Cheers (and thanks for learntla.com, it's great!)

Andrew