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

[Andrew Gwozdziewycz <apg...@xxxxxxxxx>]

Hi Stephan,

Thanks for the response!

On Wed, Apr 12, 2017 at 1:09 PM, Stephan Merz <stepha...@xxxxxxxxx> 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!




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



-- 
http://www.apgwoz.com