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

*From*: fl <freder...@xxxxxxxxxxx>*Date*: Wed, 23 Sep 2015 09:20:04 -0700 (PDT)*References*: <a475916a-37de-4c9c-8421-e17d35692019@googlegroups.com> <2074b94b-7bb7-4fe0-bcb9-25bffd7036a5@googlegroups.com>

Hi Leslie,

I didn't mean to propose what I wrote in those two classes as stellar

examples of what documentation should be like. I just wanted to show

the level of formality that I had in mind.

OK.

I have thought a bit about what I would say if myself, I had to speak about what one must put into

a specification of a routine written in a specific language.

I think there are three stages.

1) the theory. I'm just reading what Knuth is saying in the latest volume of his treatise about the

theory behind the algorithms that generate Grey code~: 30 pages! We can't do better.

2) The contract. I mean the couple preconditions/postconditions, requires/ensures. A first order logic +

set theory formula that combines what is expected in the variables when the algorithm begins with what is

expected in the variables when it finishes. Obviously we can replace this formula in whole or in part by words.

It may be ambiguous. But it is also easier to write. We can also add comments about the semantics as we

do with doxygen for instance. (We find that sort of contracts in your own work with tlatools under an informal

description.)

3) A simplified algorithm. A pseudo-code or a TLAPLUS code. (This is what you do in your own work with tlatools). Obviously it is not the implemented code. But since it is simpler, it is also easier to understand.

And we can also play it in isolation to understand it or make proofs about it. Here the relationship with the implemented

code is refinement.

--

FL

**Follow-Ups**:

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

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

- Prev by Date:
**Re: meaning of a tla predicate** - Next by Date:
**Re: What should I do next in the Hyperbook?** - Previous by thread:
**Re: What should I do next in the Hyperbook?** - Next by thread:
**Re: What should I do next in the Hyperbook?** - Index(es):