Quickcheck'ing a protocol

classic Classic list List threaded Threaded
11 messages Options
Reply | Threaded
Open this post in threaded view
|

Quickcheck'ing a protocol

Josh Adams-2
So I've been frustrated lately by the fact that Slack's IRC gateway isn't RFC 2812 compliant (https://github.com/bitwalker/exirc/issues/51)

In dealing with this I wondered why the crap they needed an engineer to go through the spec as a result of their server's response to figure out that this was an issue (they've added it to their bug tracker, so I have some amount of faith it might get fixed eventually - for now I'll paper over the issue in the client which reduces the stress on them to actually fix it though).

Should RFCs / protocols of this nature just come with something like a quickcheck model for their spec?  Is anyone aware of prior art around this sort of thing aside from Quvic/Volvo that I could draw from if I wanted to fiddle in this arena?

I'd think that the ideal situation involves an open source quickcheck implementation to test a given protocol implementation against at least some of the RFC, and a means to run the tests against potential servers/clients, with badges potentially showing the percentage of the test that passes.  This would allow economics to drive spec implementers towards correctness, which would save countless engineer-hours spent figuring out why the damn clients can't talk to the damn servers for a given spec.

Thoughts?  Pipe dream?  "Silly child, see A, B, and C for the many people who are already doing this?"

--
Josh Adams

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Quickcheck'ing a protocol

Pierre Fenoll-2
Have you tried using PropEr / Quickcheck statem? http://proper.softlab.ntua.gr/Tutorials/PropEr_testing_of_finite_state_machines.html
PropEr is free & open source & I use it to quickcheck RESTfull APIs.



Cheers,
-- 
Pierre Fenoll


On 22 September 2016 at 05:45, Josh Adams <[hidden email]> wrote:
So I've been frustrated lately by the fact that Slack's IRC gateway isn't RFC 2812 compliant (https://github.com/bitwalker/exirc/issues/51)

In dealing with this I wondered why the crap they needed an engineer to go through the spec as a result of their server's response to figure out that this was an issue (they've added it to their bug tracker, so I have some amount of faith it might get fixed eventually - for now I'll paper over the issue in the client which reduces the stress on them to actually fix it though).

Should RFCs / protocols of this nature just come with something like a quickcheck model for their spec?  Is anyone aware of prior art around this sort of thing aside from Quvic/Volvo that I could draw from if I wanted to fiddle in this arena?

I'd think that the ideal situation involves an open source quickcheck implementation to test a given protocol implementation against at least some of the RFC, and a means to run the tests against potential servers/clients, with badges potentially showing the percentage of the test that passes.  This would allow economics to drive spec implementers towards correctness, which would save countless engineer-hours spent figuring out why the damn clients can't talk to the damn servers for a given spec.

Thoughts?  Pipe dream?  "Silly child, see A, B, and C for the many people who are already doing this?"

--
Josh Adams

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions



_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Quickcheck'ing a protocol

Andrew Berman
Hey Pierre,

How do you QuickCheck RESTful APIs?  I'm a noobie with QuickCheck and using it with RESTful APIs would be really useful to me.  Do you have any sample code or is there a tutorial anywhere?

Thanks!

On Wed, Sep 21, 2016 at 10:58 PM Pierre Fenoll <[hidden email]> wrote:
Have you tried using PropEr / Quickcheck statem? http://proper.softlab.ntua.gr/Tutorials/PropEr_testing_of_finite_state_machines.html
PropEr is free & open source & I use it to quickcheck RESTfull APIs.



Cheers,
-- 
Pierre Fenoll

On 22 September 2016 at 05:45, Josh Adams <[hidden email]> wrote:
So I've been frustrated lately by the fact that Slack's IRC gateway isn't RFC 2812 compliant (https://github.com/bitwalker/exirc/issues/51)

In dealing with this I wondered why the crap they needed an engineer to go through the spec as a result of their server's response to figure out that this was an issue (they've added it to their bug tracker, so I have some amount of faith it might get fixed eventually - for now I'll paper over the issue in the client which reduces the stress on them to actually fix it though).

Should RFCs / protocols of this nature just come with something like a quickcheck model for their spec?  Is anyone aware of prior art around this sort of thing aside from Quvic/Volvo that I could draw from if I wanted to fiddle in this arena?

I'd think that the ideal situation involves an open source quickcheck implementation to test a given protocol implementation against at least some of the RFC, and a means to run the tests against potential servers/clients, with badges potentially showing the percentage of the test that passes.  This would allow economics to drive spec implementers towards correctness, which would save countless engineer-hours spent figuring out why the damn clients can't talk to the damn servers for a given spec.

Thoughts?  Pipe dream?  "Silly child, see A, B, and C for the many people who are already doing this?"

--
Josh Adams

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions


_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Quickcheck'ing a protocol

Mark Allen-3
In reply to this post by Josh Adams-2
Josh,

Have you looked at Scribble? http://scribble.org/






On Wednesday, September 21, 2016 10:45 PM, Josh Adams <[hidden email]> wrote:


So I've been frustrated lately by the fact that Slack's IRC gateway isn't RFC 2812 compliant (https://github.com/bitwalker/exirc/issues/51)

In dealing with this I wondered why the crap they needed an engineer to go through the spec as a result of their server's response to figure out that this was an issue (they've added it to their bug tracker, so I have some amount of faith it might get fixed eventually - for now I'll paper over the issue in the client which reduces the stress on them to actually fix it though).

Should RFCs / protocols of this nature just come with something like a quickcheck model for their spec?  Is anyone aware of prior art around this sort of thing aside from Quvic/Volvo that I could draw from if I wanted to fiddle in this arena?

I'd think that the ideal situation involves an open source quickcheck implementation to test a given protocol implementation against at least some of the RFC, and a means to run the tests against potential servers/clients, with badges potentially showing the percentage of the test that passes.  This would allow economics to drive spec implementers towards correctness, which would save countless engineer-hours spent figuring out why the damn clients can't talk to the damn servers for a given spec.

Thoughts?  Pipe dream?  "Silly child, see A, B, and C for the many people who are already doing this?"

--
Josh Adams

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions



_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Quickcheck'ing a protocol

James Aimonetti-2
In reply to this post by Andrew Berman
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256


You should check out Thomas Arts' talk from this past Erlang Factory:

https://www.youtube.com/watch?v=iW2J7Of8jsE

The ideas should be generally applicable.

Andrew Berman writes:

> Hey Pierre,
>
> How do you QuickCheck RESTful APIs?  I'm a noobie with QuickCheck and using
> it with RESTful APIs would be really useful to me.  Do you have any sample
> code or is there a tutorial anywhere?
>
> Thanks!
>
> On Wed, Sep 21, 2016 at 10:58 PM Pierre Fenoll <[hidden email]>
> wrote:
>
>> Have you tried using PropEr / Quickcheck statem?
>> http://proper.softlab.ntua.gr/Tutorials/PropEr_testing_of_finite_state_machines.html
>> PropEr is free & open source & I use it to quickcheck RESTfull APIs.
>>
>>
>>
>> Cheers,
>> --
>> Pierre Fenoll
>>
>> On 22 September 2016 at 05:45, Josh Adams <[hidden email]> wrote:
>>
>>> So I've been frustrated lately by the fact that Slack's IRC gateway isn't
>>> RFC 2812 compliant (https://github.com/bitwalker/exirc/issues/51)
>>>
>>> In dealing with this I wondered why the crap they needed an engineer to
>>> go through the spec as a result of their server's response to figure out
>>> that this was an issue (they've added it to their bug tracker, so I have
>>> some amount of faith it might get fixed eventually - for now I'll paper
>>> over the issue in the client which reduces the stress on them to actually
>>> fix it though).
>>>
>>> Should RFCs / protocols of this nature just come with something like a
>>> quickcheck model for their spec?  Is anyone aware of prior art around this
>>> sort of thing aside from Quvic/Volvo that I could draw from if I wanted to
>>> fiddle in this arena?
>>>
>>> I'd think that the ideal situation involves an open source quickcheck
>>> implementation to test a given protocol implementation against at least
>>> some of the RFC, and a means to run the tests against potential
>>> servers/clients, with badges potentially showing the percentage of the test
>>> that passes.  This would allow economics to drive spec implementers towards
>>> correctness, which would save countless engineer-hours spent figuring out
>>> why the damn clients can't talk to the damn servers for a given spec.
>>>
>>> Thoughts?  Pipe dream?  "Silly child, see A, B, and C for the many people
>>> who are already doing this?"
>>>
>>> --
>>> Josh Adams
>>>
>>> _______________________________________________
>>> erlang-questions mailing list
>>> [hidden email]
>>> http://erlang.org/mailman/listinfo/erlang-questions
>>>
>>>
>> _______________________________________________
>> erlang-questions mailing list
>> [hidden email]
>> http://erlang.org/mailman/listinfo/erlang-questions
>>
> _______________________________________________
> erlang-questions mailing list
> [hidden email]
> http://erlang.org/mailman/listinfo/erlang-questions


- --
James Aimonetti

Lead Systems Architect
"If Dialyzer don't care, I don't care"
2600HzPDX | http://2600hz.com
sip:[hidden email]
tel:415.886.7905
irc:mc_ @ freenode
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2

iQEcBAEBCAAGBQJX5D73AAoJENTKa+JPXCVg8SwH/jTe/EhqLBQc1b82rptahsuy
SL2dwQjzq6kxfzJquVE05t4yjjhI3GKaHoaeGkPMNF4Wq4Y9ZdWVOrIfyE1fHuxg
EltLgUq6OAjQeCYkQXNOTtcWzt6AJ8ZpKK9z9U7hydJL9NAs1IF6v2D/NjbvJ02H
OAlRLZzhqcN1nm+/yOPPqs9zBac5SR3YHK3bo8A5vlx5M+8jrI3SV6fe5cBXTbIF
CzVKmrlD3EZlGEYaDN1ssFDShv42CZJk4+2bvQnsJDJ4YRe7WqoDOJIhgcg92Tuo
ntiYR8nlMY+qzDWYjOZnpVNNUN5oudLUjmhCuLU5vGwkLB74Y+2YBwxbC7gabec=
=KvP6
-----END PGP SIGNATURE-----
_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Quickcheck'ing a protocol

Josh Adams-2
In reply to this post by Mark Allen-3
I have not seen it.  The user forum appears to have zero posts and the developer forum a handful ending in 2014.  This is not immediately encouraging :)  Thanks though, will try to dig further :)

On Thu, Sep 22, 2016 at 2:30 PM, Mark Allen <[hidden email]> wrote:
Josh,

Have you looked at Scribble? http://scribble.org/






On Wednesday, September 21, 2016 10:45 PM, Josh Adams <[hidden email]> wrote:


So I've been frustrated lately by the fact that Slack's IRC gateway isn't RFC 2812 compliant (https://github.com/bitwalker/exirc/issues/51)

In dealing with this I wondered why the crap they needed an engineer to go through the spec as a result of their server's response to figure out that this was an issue (they've added it to their bug tracker, so I have some amount of faith it might get fixed eventually - for now I'll paper over the issue in the client which reduces the stress on them to actually fix it though).

Should RFCs / protocols of this nature just come with something like a quickcheck model for their spec?  Is anyone aware of prior art around this sort of thing aside from Quvic/Volvo that I could draw from if I wanted to fiddle in this arena?

I'd think that the ideal situation involves an open source quickcheck implementation to test a given protocol implementation against at least some of the RFC, and a means to run the tests against potential servers/clients, with badges potentially showing the percentage of the test that passes.  This would allow economics to drive spec implementers towards correctness, which would save countless engineer-hours spent figuring out why the damn clients can't talk to the damn servers for a given spec.

Thoughts?  Pipe dream?  "Silly child, see A, B, and C for the many people who are already doing this?"

--
Josh Adams

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions





--
Josh Adams

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Quickcheck'ing a protocol

Jesper Louis Andersen-2
In reply to this post by Josh Adams-2

On Thu, Sep 22, 2016 at 5:45 AM, Josh Adams <[hidden email]> wrote:
Should RFCs / protocols of this nature just come with something like a quickcheck model for their spec?

In principle, protocols should come with two things:

* A set of parser combinators which fit into a framework such as Meredith Patterson's Hammer. This would make it next to impossible to accidentally parse the protocol wrong and establish syntactically valid input. In an Erlang world, it would produce proper Erlang terms.

* A QuickCheck specification. This would allow implementors to verify their protocol against a quasi-formal model which would greatly improve quality of software. Every implementation would be at least as precise as the QC model. A more ambitious solution would include a model closer to e.g. TLA+. Then one writes a compiler from TLA+ to a QC system and you can check real-world programs.

I think the reason it is not done has to do with effort. Doing the right thing(tm) often takes an order of magnitude more time compared to the quick and dirty hack. Since software is built primarily on the basis of speed (time), people don't do the necessary work up front. Rather, it is baked on later, when the damage has been done. Up front modeling often changes the spec in ways which removes ambiguity and room for error.

If we should start, *the* place to start is TLS 1.3 :P



--
J.

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Quickcheck'ing a protocol

Josh Adams-2
In principle, protocols should come with two things:

* A set of parser combinators which fit into a framework such as Meredith Patterson's Hammer. This would make it next to impossible to accidentally parse the protocol wrong and establish syntactically valid input. In an Erlang world, it would produce proper Erlang terms.

* A QuickCheck specification. This would allow implementors to verify their protocol against a quasi-formal model which would greatly improve quality of software. Every implementation would be at least as precise as the QC model. A more ambitious solution would include a model closer to e.g. TLA+. Then one writes a compiler from TLA+ to a QC system and you can check real-world programs.

I think the reason it is not done has to do with effort. Doing the right thing(tm) often takes an order of magnitude more time compared to the quick and dirty hack. Since software is built primarily on the basis of speed (time), people don't do the necessary work up front. Rather, it is baked on later, when the damage has been done. Up front modeling often changes the spec in ways which removes ambiguity and room for error.

If we should start, *the* place to start is TLS 1.3 :P

This all sounds amazing and like a thing I'd like to encourage the world to adopt.  Any thoughts on a very simple protocol one could get started in?  If we could get a few similarly-written examples in place and popularized perhaps it could encourage adoption?  Bonus if we can define a service that checks an implementation, provide 'badges' that link to the service, and convince some implementations of the initial test protocols to link to them in their READMEs/sites :)

I just started doing math on this sort of thing recently and when I consider the amount of time wasted (at least 4 hours of my time just to prove that slack failed to adhere to the IRC RFC) times the number of engineers that have inevitably run into the same thing, it really sickens me.  As software continues to eat the world, I expect there to be a short asymptote to how much we can feasibly do unless we start handling things more correctly as a society.  There's...just no acceptable reason to have the situation we presently have, at this stage in our field :(

I'd be glad to do a few episodes of my screencast on this sort of thing, which (a) would justify my spending the time on such a project, and (b) might help me popularize the idea / get other people up in arms about it.  I'd need some help though because I'm a bit out of my depth here :) 
 
--
Josh Adams

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Quickcheck'ing a protocol

Andrew Berman
In reply to this post by James Aimonetti-2
Cool, thanks!

On Thu, Sep 22, 2016 at 1:28 PM James Aimonetti <[hidden email]> wrote:
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256


You should check out Thomas Arts' talk from this past Erlang Factory:

https://www.youtube.com/watch?v=iW2J7Of8jsE

The ideas should be generally applicable.

Andrew Berman writes:

> Hey Pierre,
>
> How do you QuickCheck RESTful APIs?  I'm a noobie with QuickCheck and using
> it with RESTful APIs would be really useful to me.  Do you have any sample
> code or is there a tutorial anywhere?
>
> Thanks!
>
> On Wed, Sep 21, 2016 at 10:58 PM Pierre Fenoll <[hidden email]>
> wrote:
>
>> Have you tried using PropEr / Quickcheck statem?
>> http://proper.softlab.ntua.gr/Tutorials/PropEr_testing_of_finite_state_machines.html
>> PropEr is free & open source & I use it to quickcheck RESTfull APIs.
>>
>>
>>
>> Cheers,
>> --
>> Pierre Fenoll
>>
>> On 22 September 2016 at 05:45, Josh Adams <[hidden email]> wrote:
>>
>>> So I've been frustrated lately by the fact that Slack's IRC gateway isn't
>>> RFC 2812 compliant (https://github.com/bitwalker/exirc/issues/51)
>>>
>>> In dealing with this I wondered why the crap they needed an engineer to
>>> go through the spec as a result of their server's response to figure out
>>> that this was an issue (they've added it to their bug tracker, so I have
>>> some amount of faith it might get fixed eventually - for now I'll paper
>>> over the issue in the client which reduces the stress on them to actually
>>> fix it though).
>>>
>>> Should RFCs / protocols of this nature just come with something like a
>>> quickcheck model for their spec?  Is anyone aware of prior art around this
>>> sort of thing aside from Quvic/Volvo that I could draw from if I wanted to
>>> fiddle in this arena?
>>>
>>> I'd think that the ideal situation involves an open source quickcheck
>>> implementation to test a given protocol implementation against at least
>>> some of the RFC, and a means to run the tests against potential
>>> servers/clients, with badges potentially showing the percentage of the test
>>> that passes.  This would allow economics to drive spec implementers towards
>>> correctness, which would save countless engineer-hours spent figuring out
>>> why the damn clients can't talk to the damn servers for a given spec.
>>>
>>> Thoughts?  Pipe dream?  "Silly child, see A, B, and C for the many people
>>> who are already doing this?"
>>>
>>> --
>>> Josh Adams
>>>
>>> _______________________________________________
>>> erlang-questions mailing list
>>> [hidden email]
>>> http://erlang.org/mailman/listinfo/erlang-questions
>>>
>>>
>> _______________________________________________
>> erlang-questions mailing list
>> [hidden email]
>> http://erlang.org/mailman/listinfo/erlang-questions
>>
> _______________________________________________
> erlang-questions mailing list
> [hidden email]
> http://erlang.org/mailman/listinfo/erlang-questions


- --
James Aimonetti

Lead Systems Architect
"If Dialyzer don't care, I don't care"
2600HzPDX | http://2600hz.com
[hidden email]
tel:415.886.7905
irc:mc_ @ freenode
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2

iQEcBAEBCAAGBQJX5D73AAoJENTKa+JPXCVg8SwH/jTe/EhqLBQc1b82rptahsuy
SL2dwQjzq6kxfzJquVE05t4yjjhI3GKaHoaeGkPMNF4Wq4Y9ZdWVOrIfyE1fHuxg
EltLgUq6OAjQeCYkQXNOTtcWzt6AJ8ZpKK9z9U7hydJL9NAs1IF6v2D/NjbvJ02H
OAlRLZzhqcN1nm+/yOPPqs9zBac5SR3YHK3bo8A5vlx5M+8jrI3SV6fe5cBXTbIF
CzVKmrlD3EZlGEYaDN1ssFDShv42CZJk4+2bvQnsJDJ4YRe7WqoDOJIhgcg92Tuo
ntiYR8nlMY+qzDWYjOZnpVNNUN5oudLUjmhCuLU5vGwkLB74Y+2YBwxbC7gabec=
=KvP6
-----END PGP SIGNATURE-----

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Quickcheck'ing a protocol

Pierre Fenoll-2
In reply to this post by Andrew Berman
There are a bunch of papers / thesis on this topic. 
I recommend the statem doc link I posted earlier. 
There's a talk from Quviq at latest SF Erlang Factory: https://m.youtube.com/watch?v=iW2J7Of8jsE
Note that Quviq provides a paid CI service. My bet is a service that quickchecks a project's APIs would be worth good money. 

Please share your troubles / findings :)

On 22 Sep 2016, at 19:53, Andrew Berman <[hidden email]> wrote:

Hey Pierre,

How do you QuickCheck RESTful APIs?  I'm a noobie with QuickCheck and using it with RESTful APIs would be really useful to me.  Do you have any sample code or is there a tutorial anywhere?

Thanks!

On Wed, Sep 21, 2016 at 10:58 PM Pierre Fenoll <[hidden email]> wrote:
Have you tried using PropEr / Quickcheck statem? http://proper.softlab.ntua.gr/Tutorials/PropEr_testing_of_finite_state_machines.html
PropEr is free & open source & I use it to quickcheck RESTfull APIs.



Cheers,
-- 
Pierre Fenoll

On 22 September 2016 at 05:45, Josh Adams <[hidden email]> wrote:
So I've been frustrated lately by the fact that Slack's IRC gateway isn't RFC 2812 compliant (https://github.com/bitwalker/exirc/issues/51)

In dealing with this I wondered why the crap they needed an engineer to go through the spec as a result of their server's response to figure out that this was an issue (they've added it to their bug tracker, so I have some amount of faith it might get fixed eventually - for now I'll paper over the issue in the client which reduces the stress on them to actually fix it though).

Should RFCs / protocols of this nature just come with something like a quickcheck model for their spec?  Is anyone aware of prior art around this sort of thing aside from Quvic/Volvo that I could draw from if I wanted to fiddle in this arena?

I'd think that the ideal situation involves an open source quickcheck implementation to test a given protocol implementation against at least some of the RFC, and a means to run the tests against potential servers/clients, with badges potentially showing the percentage of the test that passes.  This would allow economics to drive spec implementers towards correctness, which would save countless engineer-hours spent figuring out why the damn clients can't talk to the damn servers for a given spec.

Thoughts?  Pipe dream?  "Silly child, see A, B, and C for the many people who are already doing this?"

--
Josh Adams

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions


_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Quickcheck'ing a protocol

Jesper Louis Andersen-2
In reply to this post by Josh Adams-2

On Thu, Sep 22, 2016 at 10:43 PM, Josh Adams <[hidden email]> wrote:
This all sounds amazing and like a thing I'd like to encourage the world to adopt.

The world seems to agree. A recent news article touches on the subject[0], where Jeanette Wing (and probably her research group) are working on building a formal model of TLS.

There are a couple of viable avenues you can adopt. One of the more promising is to write down a formal specification from which you can derive test cases. But if constructed correctly, they can also be executed at the same time. Erlang isn't a nice vehicle for this since you are lack (Standard) ML style functors, but the ideas are certainly transferable.

Because you can also execute the model, you can use it as a driver in a QuickCheck test case and make sure that some other implementation is correct w.r.t to the executable specification.

The way to approach this kind of thing is to crawl before walking. Start out with a small ping-pong protocol which base64 encodes its queries and responses. Then show this correct and use that to build gradually more complex stuff. Most of the full quickcheck developments starts in a corner of the full system and then gradually extend themselves. Trying to attack a full system from day 1 is usually hard.

Also, you have to learn some tricks in order to handle standard protocol problems. By targeting toys with those problems it is often easier to figure out how to handle them, before trying to do it on the full system. Model building is fun, but it takes the same thought process as when you are trying to solve an abstract math problem: the answer will come to you why you are doing other stuff, muddling on the question.


--
J.

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions