direction, i.e., which arcs are linked by which vertices. Figure 
3 shows examples of channels that map onto the same directed 
graph. 
  
  
San. Norio 
—_>- -— ap — = ANT 
— —_— —— 
Figure 3: Channel patterns that map onto the same graph. 
The following algebraic specification describes formally the 
behavior of channels. It is based on the definition of a vertex, 
which is a simple type with operation to make a vertex from a 
unique id, to get the id from a vertex, and to test whether or 
not two vertices are equal (isEqual), i.e., whether they have 
the same id's. 
sort channel 
operations make vertex X vertex — channel 
initial Vertex: channel — vertex 
finalVertex: channel — vertex 
isEqual channel x channel — boolean 
upStream: channel x vertex | — boolean 
downStream: channelx vertex — boolean 
variables c1: channel; v1, v2, v3, v4: vertex; 
axioms initial Vertex (make (v1, v2)) == v1 
finalVertex (make (v1, v2)) == v2 
upStream (c1, v1) —— finalVertex (c1) = vl 
downStream (c1, v1) == initial Vertex (c1) = v1 
isEqual (make (v1, v2), make (v3, v4)) == 
vertex.isEqual (v1, v3) and vertex.isEqual (v2, v4) 
3.2 Channel Connections 
In a river network, channels can be connected in various ways. 
The constraint between two consecutive channels is that their 
flow direction is the same. In terms of the graph model, two 
arcs, e] and e2, may join if they have complementary vertices, 
i.e., either initial (e]) = final (e2) or final (e]) = initial (e2). 
In order to have connections between channels, channels must 
be part of a network. Such a network is built iteratively by 
adding channels. Channels are connected through common 
vertices. These vertices can then be classified according the 
number of its upstream and downstream channels. 
sort network 
operations create: — network 
addChannel: network x channel — network 
isIn: network x channel — boolean 
inDegree: — network x vertex — — integer 
outDegree: network x vertex — — integer 
variables nl: network; c1: channel; v1: vertex 
axioms isIn (create, c1) == false 
isIn (addChannel (nl, c1), c2) == 
if isEqual (cl, c2) then return true 
else isIn (n1, c2) 
inDegree (create, v1) == 0 
inDegree (addChannel (nl, cl), vl) == 
if upStream (c1, vl) then 1 + inDegree (nl, v1) 
else 0 + inDegree (nl, v1) 
320 
outDegree (create, vl) == 
outDegree (addChannel (n1, cl), vl) == 
if downStream (c1, v1) 
then 1+ outDegree (nl, v1) 
else 0 + outDegree (nl, v1) 
The specification will be extended throughout this paper as 
new features are introduced. 
3.2.1 Source and Destination 
The source is the origin of the water flow. Each river network 
has at least one source. In terms of the graph model, a source 
is a vertex of out-degree 1 and in-degree 0. 
A similarly distinct river landmark is the destination of a 
network. Rivers flow either into a lake or into the sea. Each 
river has one destination, though there are river networks with 
multiple destinations such as in river deltas. In terms of a 
graph, a destination is a vertex that has in-degree 1 and out- 
degree 0. 
sort network (cont.) 
operations source: network x vertex — boolean 
destination: network x vertex — boolean 
axioms source (nl, vl) == inDegree (nl, v1) = 0 and 
outDegree (nl, v1) 2 1 
destination (n1, v1) == inDegree (n1, v1) = 1 and 
outDegree (n1, v1) «0 
3.2.2 Auxiliary Nodes 
Auxiliary nodes are nodes whose in-degree and out-degree are 
1 (Figure 4). 
Figure 4: An auxiliary node and its graph representation. 
Unless such nodes are specific features, such as lakes, they 
contain no topologically significant information. 
sort network (cont.) 
operation auxNode: network x vertex — boolean 
axiom auxNode (nl, vl) == inDegree (nl, v1) = 1 and 
outDegree (nl, v1) = 1 
3.2.3 Junction 
Two or more channels may join at a junction and merge into a 
single channel. In the di-graph model, a junction corresponds 
to a vertex of out-degree 1 and in-degree 2 or higher. The in- 
degree represents the upstream channels, while the out-degree 
is a measure for the number of downstream channels. Figure 5 
shows an example of a junction and its mapping onto a di- 
SL N 
Figure 5: Junction pattern and its graph representation. 
sor 
Op 
axi 
3.2 
Re 
mo 
rive 
gra] 
of ] 
sor 
ope 
axi 
Fig 
a di 
3,3 
A la 
Carr 
have 
For 
may 
auxi 
coni 
char 
degr 
bran 
lake 
com 
lake 
wou 
of ar 
Figu