The trait signed specifies four signed integer types and
several conversion functions between them; the actual specifications
come from the included traits char, short, int, and
long.
It also put some constraints on the size of integer types;
that is, char is a subrange of short, and
short is a subrange of int, which in turn is a subrange of
long.
% @(#)$Id: signed.lsl,v 1.5 1995/07/26 21:16:23 leavens Exp $
signed: trait
includes char, short, int, long
introduces
to_short: char -> short
to_int: short -> int
to_long: int -> long
asserts
\forall c: char, s: short, i:int
to_short(0) == 0;
to_short(succ(c)) == succ(to_short(c));
to_short(pred(c)) == pred(to_short(c));
to_int(0) == 0;
to_int(succ(s)) == succ(to_int(s));
to_int(pred(s)) == pred(to_int(s));
to_long(0) == 0;
to_long(succ(i)) == succ(to_long(i));
to_long(pred(i)) == pred(to_long(i));
LONG_MIN <= to_long(INT_MIN);
INT_MIN <= to_int(SHRT_MIN);
SHRT_MIN <= to_short(CHAR_MIN);
to_short(CHAR_MAX) <= SHRT_MAX;
to_int(SHRT_MAX) <= INT_MAX;
to_long(INT_MAX) <= LONG_MAX
Go to the first, previous, next, last section, table of contents.