3

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.

MaXim
  • 63
  • 1
  • 5

1 Answers1

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
danielp
  • 1,179
  • 11
  • 26
  • What is /rel in Z-notation – Jut Dec 26 '21 at 12:22
  • If some nodes have no incident edges, graph : node \rel node how work? – Jut Dec 26 '21 at 12:43
  • "A \rel B" (LaTeX syntax) is "A <-> B" the set of all relations between A and B. – danielp Jan 04 '22 at 18:57
  • The solution above (implicitly) assumes that the set `node` contains all edges of graph. If a node N has no incident edges, there wouldn't be a pair in graph where N is on the left or right side. But `[node]` declares the set as a constant, so you wouldn't be able to change the set of edges in the graph. One approach would be to define a constant `[NODE]` that contains all possible edges and define a subset `edges \subseteq NODE` with `graph: edges \rel edges`. – danielp Jan 04 '22 at 19:03