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