This section presents a collection of definitions which are of general use. Most libraries will include these objects or ones similar to them.

It is convenient to have a singleton type
available. We call it ` one`.

one == { x:int | x=0 in int }Most programming languages contain a two--element type of ``booleans'' ; we use the two--element type

two == { x:int | (x=0 in int | x=1 in int) }Associated with the ``boolean'' type is the usual conditional operator, the ``if--then--else'' construct.

if <x:two> then <t1:exp> else <t2:exp> fi == int_eq( <x>; 0; <t1>; <t2> )To make selections from pairs we define the basic selectors as follows.

1of( <P:pair> ) == spread( <P>; u,v.u )

2of( <P:pair> ) == spread( <P>; u,v.v )To define some of the most basic types the usual order relations on integers are very useful. These must be defined from the simple

<m:int> <= <n:int> == <n> < <m> -> void

<m:int> < <n:int> < <k:int> == <m> < <n> & <n> < <k>

<m:int> <= <n:int> <= <k:int> == <m> <= <n> & <n> <= <k>Another useful concept is the idea of a finite interval in

{ <lb:int>, ..., <hb:int> } == { i:int | <lb> <= i <= <hb> }

The basic logic definitions were discussed in chapter 3, but they are repeated in figure for reference in the subsequent sections. To illustrate the kind of parenthesizing which it is wise to do in practice only white space has been added to the text of the actual library object.

Thu Sep 14 08:45:18 EDT 1995