Re: C arithmetic, was Software proofs, was Are there different

[...]
> [The history of formal description of programming languages is not
> encouraging. Back in the 1970s the ANSI PL/I standard was defined in
> terms of formal operations on trees, but even so it had bugs/errors.
> Also, per your comment on addition, in a lot of cases the practical
> definition turns into whatever the underlying machine's instruction
> does. Until recently the C standard was deliberately unclear about
> whether arithmetic was ones- or twos-complement. -John]


The C standard still doesn't mandate two's-complement.


The 1990 edition of the C standard was vague about integer
representations, though it did impose some requirements. It required
a "pure binary" representation, and it required, for example,
a value that is within the range of both int and unsigned int to
have the same representation in both. That excluded some of the
more exotic possibilites. (It mentioned 2's complement a few times,
but only as an example.)


The 1999 standard explicitly required one of three representations:
sign and magnitude, two's complement, or one's complement. It also
explicitly permitted padding bits (bits that don't contribute
to the value, and that can either be ignored or create trap
representations).


The 2011 standard corrected the spelling of "ones' complement",
but otherwise didn't change anything significant. (The 2017 edition
was a minor update.)


The upcoming 2023 standard mandates two's complement. And it
requires INT_MIN to be exactly -INT_MAX-1; previously INT_MIN could
be equal to -INT_MAX, and -INT_MAX-1 could be a trap representation.
It still permits padding bits and trap representations.


Note that twos's complement *representation* doesn't imply two's
complement *behavior* on overflow. Signed integer overflow still
has undefined behavior.


--
Keith Thompson (The_Other_Keith) Keith.S.Thompson+u@gmail.com
Working, but not speaking, for XCOM Labs
void Void(void) { Void(); } /* The recursive call of the void */

Return to the comp.compilers page.
Search the comp.compilers archives again.