Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: graph_ops.pvs Sprache: PVS

Original von: PVS^©

%------------------------------------------------------------------------
%
%  Operations on a graph
%  ------------------------------------------------
%
%      Author: Ricky W. Butler   NASA Langley Research Center
%
%  Defines:
%
%      union(G1,G2)      -- creates graph that is a union of G1 and G2
%
%      del_vert(G,v)     -- removes a vertex and all adjacent edges from a graph
%
%      del_edge(e,G)     --  creates subgraph with edge e removed
%
%      num_edges(G): nat --  number of edges in a graph
%
%------------------------------------------------------------------------
graph_ops[T: TYPE]: THEORY

BEGIN

   IMPORTING graphs[T]

   G, G1, G2: VAR graph[T]
   t1,t2: VAR T
   x,v: VAR T
   e,e2: VAR doubleton[T]

   union(G1,G2): graph[T] = (# vert := union(vert(G1),vert(G2)),
                               edges := union(edges(G1),edges(G2)) #)

   del_vert(G: graph[T], v: T): graph[T] =
                        (# vert := remove[T](v,vert(G)),
                           edges := {e | edges(G)(e) AND NOT e(v)} #)

   del_edge(G,e): graph[T] = G WITH [edges := remove(e,edges(G))]

   num_edges(G): nat = card(edges(G))

   adjacent(G, (x:T)): finite_set[T] = {y: T| vert(G)(y) AND edge?(G)(x,y)}

%  --------------------- del_vert(G,v) lemmas ----------------

   del_vert_still_in   : LEMMA FORALL (x: (vert(G))):
                                     x /= v IMPLIES vert(del_vert(G, v))(x)

   size_del_vert       : LEMMA FORALL (v: (vert(G))):
                                   size(del_vert(G,v)) = size(G) - 1

   del_vert_le         : LEMMA size(del_vert(G,v)) <= size(G)

   del_vert_ge         : LEMMA size(del_vert(G,v)) >= size(G) - 1

   edge_in_del_vert    : LEMMA (edges(G)(e) AND NOT e(v)) IMPLIES
                                 edges(del_vert(G,v))(e)

   edges_del_vert      : LEMMA edges(del_vert(G,v))(e) IMPLIES
                                       edges(G)(e)

   del_vert_comm       : LEMMA del_vert(del_vert(G, x), v) =
                                    del_vert(del_vert(G, v), x)

   del_vert_empty?     : LEMMA FORALL (v: (vert(G))):
                                  empty?(vert(del_vert(G, v))) IMPLIES
                                      singleton?(G)

%  ---------- del_edge(G,e) ----------------------------------

   del_edge_lem       : LEMMA NOT member(e,edges(del_edge(G,e)))

   del_edge_lem2      : LEMMA edges(del_edge(G,e))(e2)
                          IMPLIES edges(G)(e2)

   del_edge_lem3      : LEMMA edges(G)(e2) AND e2 /= e IMPLIES
                          edges(del_edge(G,e))(e2)

   del_edge_lem5      : LEMMA NOT edges(G)(e) IMPLIES del_edge(G, e) = G

   vert_del_edge      : LEMMA vert(del_edge(G,e)) = vert(G)

   del_edge_num       : LEMMA num_edges(del_edge(G,e)) = num_edges(G)
                                       - IF edges(G)(e) THEN 1 ELSE 0 ENDIF

   del_edge_singleton : LEMMA singleton?(del_edge(G,e)) IMPLIES singleton?(G)

   del_vert_edge_comm : LEMMA del_vert(del_edge(G, e), v) =
                               del_edge(del_vert(G, v), e)

   del_vert_edge      : LEMMA e(v) IMPLIES
                               del_vert(del_edge(G,e),v) = del_vert(G,v)

END graph_ops

¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.