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
tlatools/src/tla2tex/FindAlignments.java
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
tlatools/src/pcal/TLAtoPCalMapping.java
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.
Leslie
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 isimprecise 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 painto write them of change them).But maybe you want to speak of the algorithm itself and the involved data structures.Not its implementation.--FL--
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.