Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: vect_fun_ops.pvs Sprache: PVS

Original von: PVS^©

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

BEGIN

   IMPORTING digraphs[T]

   G, G1, G2: VAR digraph[T]
   t1,t2: VAR T
   x,v: VAR T
   e,e2: VAR edgetype[T]

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

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

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

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

%  --------------------- 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 in?(v,e)) 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 in?(v,e) IMPLIES
                               del_vert(del_edge(G,e),v) = del_vert(G,v)

END digraph_ops

¤ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht 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.