11.1.2 Short Integer Trait

The trait short is paradigmatic for the other integer traits. It is defined as follows.

% @(#)$Id: short.lsl,v 1.8 1995/11/09 21:22:39 leavens Exp $

short(short): trait

  includes Integer(short), % from LSL handbook
           Between(short), NoContainedObjects(short)

  introduces
    SHRT_MIN, SHRT_MAX: -> short
    inRange: short -> Bool

  asserts 
    \forall s: short
      SHRT_MIN == (- SHRT_MAX) - 1;
      SHRT_MIN <= 0 /\ 1 <= SHRT_MAX;
      inRange(s) == (SHRT_MIN <= s /\ s <= SHRT_MAX);

  implies
    \forall s: short
      inRange(s) == between(SHRT_MIN, s, SHRT_MAX);

The trait functions SHRT_MIN and SHRT_MAX are supposed to denote the minimum and maximum values of type short on a particular machine; these are typically implemented by C++ macros in standard header files.

The trait Between defines some useful shorthands. It is shown below.

% @(#)$Id: Between.lsl,v 1.3 1995/11/09 21:21:36 leavens Exp $
Between(T): trait
  assumes PartialOrder
  introduces
    between, strictly_between: T, T, T -> Bool
    between, strictly_between: T, T, T, T -> Bool
  asserts
    \forall w, x, y, z: T
      between(x,y,z) == x <= y /\ y <= z;
      between(w,x,y,z) == w <= x /\ x <= y /\ y <= z;
      strictly_between(x,y,z) == x < y /\ y < z;
      strictly_between(w,x,y,z) == w < x /\ x < y /\ y < z;
      strictly_between(w,x,y,z) == w < x /\ x < y /\ y < z;

Go to the first, previous, next, last section, table of contents.