% @(#)$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

[Index]

HTML generated using lcpp2html.