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

Re: [tlaplus] Re: What should I do next in the Hyperbook?

Hi Frederic,

I'm also curious to know what I'd put in a section on writing informal
specs.  My ideas are very vague.  The best I can do is point you to
the informal specs of my own code.  They vary from a couple of simple
lines of English to a few pages of what might be described as precise
text, sometimes containing formulas.  The code is in the TLA Toolbox
CodePlex repository.  Here are two examples of long specs:

- The comments at the beginning of the file


  Specifies the trickiest part of the pretty-printer.
  It is also interesting because it shows the original spec and how
  the spec was modified when the pretty-printer was enhanced to
  handle PlusCal.  This spec illustrates the fallacy of two arguments
  agains specification:

  1. You can't specify something as ill-defined as correctness
     of a pretty printer.

  2. A spec is useless because the program is going to me modified.
     (The spec was invaluable when I had to go back and modify
     the code, making the necessary change simple.  Without the
     spec I would have had to rewrite the entire method.)

- The class


  essentially implements an algorithm written in TLA+/PlusCal.  A
  copy of that spec is appears as a comment at the end of that
  file.  Documentation of various methods or pieces of code
  refer to that spec.  Looking at the comments in that Java
  file will give you a good idea of the kind of informal specs
  that I write.


On Wed, Sep 16, 2015 at 4:27 AM, fl <freder...@xxxxxxxxxxx> wrote:

8. Something about writing informal specs.

I'm curious to know what you would put in such a section.
I definitely find it difficult to write correct informal spec of a true routine. Either it is
imprecise as in this page:
or it is  rather difficult to know how to use it in practice. For instance as in:
But it is maybe due to the conciseness of the documentation. (And these ones are rather formal.)
Definitely I think that the use of what they now call "ghost variables" or "model variables"
is mandatory.
And there is still a lack of accurate and powerful tools. Notably to write easily true formal,
mathematical computer scince object in a language like TeX
(they have the property of being longer to write than the mathematical ones and it is a pain
to write them of change them).
But maybe you want to speak of the algorithm itself and the involved data structures.
Not its implementation.

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 http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.