Quelle digraph_ops.pvs Sprache: 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

quality94%

¤ Dauer der Verarbeitung: 0.1 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.