[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Proofs of integer properties
One comment about the hyperbook in particular, the text
description building up proofs is good to follow along and
force you to think
but when there is a problem it's easy to get lost without reference to the
final working TLA+ text.
It might be helpful to have the actual TLA+ modules accompany the
hyperbook, rather than just the PDF versions (even the ASCII in PDF form).
In general, I have tried to present a complete module after developing it bit by bit. However, sometimes a module isn't developed bit by bit, but a first version is developed, then it is modified to form another version, then modified again and again. So, instead of having a single complete module, there are quite a few. In those cases, it seems impractical to provide a complete module for each of those versions. Perhaps someone has a suggestion on what to do in that case. However, it is possible that there are places where it would be reasonable to provide a complete module (or perhaps a complete proof) and I have failed to do so. I would appreciate having those exact places pointed out.