Z Notation: Representation of a 2D array

Question

I'm a complete beginner at the Z notation. I need to represent a graph type in Z. The idea I have is to use an incidence matrix so that I can traverse freely between nodes and edges with ease.

The only problem is, I don't know how to specify the incidence matrix in Z. I would think that I need a 2D array, but looking through the reference material available for the Z notation, arrays are commonly represented using seq. Is there another way to specify a multi dimensional array?

Thanks in advance.

Answer 1

I think a relation between nodes would be a better representation for an incidence matrix. Lets assume that we have a type node:

 [node]

Then a graph could be modelled as a relation between nodes:

graph : node \rel node

This would be a directed graph because there could be an edge n1->n2 in graph but not n2->n1. If you need an undirected graph you can add a further restriction:

graph\inv = graph

(The inverse of graph is the same as graph, i.e. if n1->n2 in graph, then n2->n1 must be in graph, too.)

If you really want to model an incidence matrix as a multidimensional array, you can define a function that maps from a position in the array to an integer, e.g.:

matrix: (node \cross node) \fun {0,1}

The relation between the two representations can be expressed as:

\forall n1,n2:node @ (n1,n2)\in graph \iff graph( (n1,n2) ) = 1