Quelle graph_conn_defs.pvs Sprache: PVS

graph_conn_defs[T: TYPE]: THEORY

BEGIN

   IMPORTING graph_deg[T]

   G,G1,G2: VAR graph[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)

   IMPORTING walks[T]

   path_connected?(G): bool = NOT empty?(G) AND
                              (FORALL (x,y: (vert(G))): % x /= y IMPLIES
                                   (EXISTS (w: Walk(G)): seq(w)(0) = x AND
                                                         seq(w)(length(w)-1) = y))

   H1,H2: VAR graph[T]
   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

END graph_conn_defs

quality99%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.