### 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;

```