data specification using int-basic1 intinf = ⌜ . ⌝(. .i : int) | -∞ | ∞ ; variables i∞ : intinf; end data specification