Quellcode-Bibliothek graph_connected.pvs

graph_connected[T: TYPE]: THEORY

BEGIN

   IMPORTING graph_ops[T], graph_deg[T], walks[T],
             graph_conn_defs[T], 
             graph_conn_piece, graph_piece_path,  % FOR PROOF ONLY
             graph_path_conn, graph_complected    % FOR PROOF ONLY

   G,G1,G2,H1,H2: VAR graph[T]


   conn_eq_path       : THEOREM connected?(G) = path_connected?(G)

   path_eq_piece      : THEOREM path_connected?(G) = piece_connected?(G)

   piece_eq_conn      : THEOREM piece_connected?(G) = connected?(G)

   conn_eq_complected : THEOREM connected?(G) = complected?(G)

%WHERE (defined in graph_conn_defs[T]) 
%
%   connected?(G): RECURSIVE bool = singleton?(G) OR
%                                   (EXISTS (v: (vert(G))): deg(v,G) > 0 
%                                       AND connected?(del_vert(G,v))) 
%                  MEASURE size(G)
%
%   path_connected?(G): bool = (FORALL (x,y: (vert(G))): x /= y IMPLIES
%                                   (EXISTS (w: Walk(G)): seq(w)(0) = x AND 
%                                                         seq(w)(length(w)-1) = y))
%
%   piece_connected?(G): bool = NOT empty?(G) AND
%                               (FORALL H1,H2: G = union(H1,H2) AND
%                                         NOT empty?(H1) AND NOT empty?(H2)
%                                  IMPLIES NOT empty?(intersection(vert(H1),
%                                                                   vert(H2))))
%
%   complected?(G): bool = IF isolated?(G) THEN singleton?(G) 
%                          ELSIF (EXISTS (v: (vert(G))): deg(v,G) = 1) THEN
%                           (EXISTS (x: (vert(G))): deg(x,G) = 1 AND
%                              connected?(del_vert(G,x)))
%                          ELSE
%                             (EXISTS (e: (edges(G))):
%                              connected?(del_edge(G,e)))
%                          ENDIF
%
% are defined in graph_conn_defs.pvs

END graph_connected