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

Standards and TLAPLUS

Like the Bible, the C standard deserves to be thoroughly commented by generations of scholars.


Page 4 it is said that "a byte is composed of a contiguous sequence of bits, the number of which is


Page 27 it is said that "number of bits for [the] smallest object that is not a bit-field ([a] byte)" is >= 8.

So far so good. But:

Page 4 it is said that a byte is an "addressable unit of data storage large enough to hold any member of the basic character

set of the execution environment".

And page 22, you can see that this set has 100 elements.

But since it is clear that a byte that is at least 8 bit long is large enough to accommodate 100 elements, I don't

really understand what this information is good for.

Or this is information about the characters (the objects that represent them must be 1 byte long) but in that case

the sentence must be restated.

(It is an example: there are other curiosities in the standard.)

All that to say that if they were using a formal language like TLAPLUS to formulate their propositions

they would gain in clarity and they would avoid redundancy. (But they must keep the literate commentary too obvioulsy.)