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.
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 < relation. Here are some of the basic order definitions as an example of how to proceed. The first is a definition of
, and the following two
define notation for chains of inequalities.
<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 int;
it may be defined as follows.
{ <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.
