% @(#)$Id: unsigned.lsl,v 1.5 1995/07/26 21:16:23 leavens Exp $

unsigned: trait

  includes unsignedChar, unsignedShort, unsignedInt, unsignedLong

  introduces 
    to_unsignedShort: unsignedChar -> unsignedShort
    to_unsignedInt: unsignedShort -> unsignedInt
    to_unsignedLong: unsignedInt -> unsignedLong

  asserts
    \forall c: unsignedChar, s: unsignedShort, i: unsignedInt
      to_unsignedShort(0) == 0;
      to_unsignedShort(succ(c)) == succ(to_unsignedShort(c));
      to_unsignedInt(0) == 0;
      to_unsignedInt(succ(s)) == succ(to_unsignedInt(s));
      to_unsignedLong(0) == 0;
      to_unsignedLong(succ(i)) == succ(to_unsignedLong(i));
      to_unsignedShort(UCHAR_MAX) <= USHRT_MAX;
      to_unsignedInt(USHRT_MAX) <= UINT_MAX;
      to_unsignedLong(UINT_MAX) <= ULONG_MAX

[Index]

HTML generated using lcpp2html.