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

Re: [tlaplus] Re: Reusing Specs



Hi,

thank you very much, Leslie! I got a little confused about our approach when I read your first post because
our system uses Paxos as a sub-system and we decided to not write a Paxos specification ourselves since
one already exists and we would like to use it, but now it's clear, and indeed doesn't make sense to write a
specification to serve for general purpose.

Rodrigo

Em qua, 19 de jun de 2019 às 10:58, Leslie Lamport <tlaplus.ll@xxxxxxxxx> escreveu:
Hi Rodrigo,

It sounds like you are doing exactly what I advised.  I never said not
to reuse specs that have already been written.  It's rare that one can
reuse an existing spec without modifying it; I'm delighted that you
were able to do that with my Voting spec.  Perhaps that will become
more common when more algorithm designers write precise specifications
of their algorithms.

A spec is written for a purpose, and a good spec is one that serves
its purpose well.  It appears that the purpose of your spec required
certain modules to be reused for describing a particular class of
algorithms.  And you understood that, as I wrote, copy/paste/modify is
a fine way of reusing a module.

What I tried to say in my note is that, when writing a spec, one
shouldn't worry about whether the spec might be used again for some
unknown purpose.

Leslie


--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1fb4f1e4-372a-4e14-afdc-2e1844d20690%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.


--
Rodrigo Q. Saramago

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAAjYtgUf9-g1%2B1X-HjP6hCB%2BBTydBY%2BcVZ1rwsKCLhF-iqAdhQ%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.