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

*From*: fl <freder...@xxxxxxxxxxx>*Date*: Wed, 16 Sep 2015 04:27:12 -0700 (PDT)*References*: <a475916a-37de-4c9c-8421-e17d35692019@googlegroups.com>

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.

--

FL

**Follow-Ups**:**Re: [tlaplus] Re: What should I do next in the Hyperbook?***From:*TLA Plus

**References**:**What should I do next in the Hyperbook?***From:*Leslie Lamport

- Prev by Date:
**Using TLA+ for teaching distributed systems (University at Buffalo)** - Next by Date:
**Re: [tlaplus] What should I do next in the Hyperbook?** - Previous by thread:
**What should I do next in the Hyperbook?** - Next by thread:
**Re: [tlaplus] Re: What should I do next in the Hyperbook?** - Index(es):