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