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