Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: digraph_deg.pvs Sprache: PVS

Original von: PVS^©

digraph_deg[T: TYPE]: THEORY
%------------------------------------------------------------------------
%
%  Defines degree of a vertex
%  ------------------------------------------------
%
%      Authors: Ricky W. Butler   NASA Langley Research Center
%               Kristin Y. Rozier NASA Langley Research Center
%
%  Defines:
%
%    incident_edges(v,G) -- returns set of edges attached to vertex v
%
%    in_deg(v,G), out_deg(v,G) -- number of edges attached to vertex v
%
%------------------------------------------------------------------------

BEGIN

   IMPORTING digraphs[T], digraph_ops[T]

   v: VAR T
   G,GS: VAR digraph[T]

   incoming_edges(v,G): finite_set[edgetype[T]]
                              = {e: edgetype[T] | edges(G)(e) AND e`2 = v}

   outgoing_edges(v,G): finite_set[edgetype[T]]
                              = {e: edgetype[T] | edges(G)(e) AND e`1 = v}

   incident_edges(v,G)  : finite_set[edgetype[T]]
                              = {e: edgetype[T] | edges(G)(e) AND in?(v,e)}

   incoming_edges_subset: LEMMA subset?(incoming_edges(v,G),edges(G))

   outgoing_edges_subset: LEMMA subset?(outgoing_edges(v,G),edges(G))

   incident_edges_subset: LEMMA subset?(incident_edges(v,G),edges(G))

   in_deg(v,G): nat = card(incoming_edges(v,G))

   out_deg(v,G): nat = card(outgoing_edges(v,G))

   %This definition of degree doesn't work for digraphs
   %deg(v,G): nat = card(incident_edges(v,G))

   deg(v,G): nat = in_deg(v,G) + out_deg(v,G)

   P : VAR pred[digraph[T]]
   n : VAR nat
   e: VAR edgetype[T]
   x,y: VAR T

   self_loop?(e): bool = (e`1 = e`2)
   %possible alternate: self_loop?(e,G): bool = edges(G)(e) AND (e`1 = e`2)

   incoming_edges_emptyset: LEMMA edges(G) = emptyset[edgetype[T]] IMPLIES
                                  incoming_edges(v,G) = emptyset[edgetype[T]]

   outgoing_edges_emptyset: LEMMA edges(G) = emptyset[edgetype[T]] IMPLIES
                                  outgoing_edges(v,G) = emptyset[edgetype[T]]

   %Define incident edges independently from in & out so self-loops aren't
   %counted twice (i.e. incident edges /= in_edges + out_edges)
   incident_edges_emptyset: LEMMA edges(G) = emptyset[edgetype[T]] IMPLIES
                                  incident_edges(v,G) = emptyset[edgetype[T]]

   deg_del_edge_incoming  : LEMMA e = (x,y) AND edges(G)(e) IMPLIES
                                  in_deg(y, G) = in_deg(y, del_edge(G, e)) + 1

   deg_del_edge_outgoing  : LEMMA e = (x,y) AND edges(G)(e) IMPLIES
                                  out_deg(x, G) = out_deg(x, del_edge(G, e)) + 1

   deg_del_non_edge       : LEMMA NOT in?(y,e)  IMPLIES
                                  deg(y, G) = deg(y, del_edge(G, e))

   deg_del_non_edge_incoming : LEMMA NOT y = e`2  IMPLIES
                                  in_deg(y, G) = in_deg(y, del_edge(G, e))

   deg_del_non_edge_outgoing : LEMMA NOT y = e`1  IMPLIES
                                  out_deg(y, G) = out_deg(y, del_edge(G, e))

   deg_del_edge    : LEMMA in?(y,e) AND edges(G)(e) AND NOT self_loop?(e)
                             IMPLIES deg(y, G) = deg(y, del_edge(G, e)) + 1

   deg_del_self_loop : LEMMA in?(y,e) AND edges(G)(e) AND self_loop?(e)
                             IMPLIES deg(y, G) = deg(y, del_edge(G, e)) + 2

   deg_del_edge_ge_incoming : LEMMA in_deg(y, G) >= in_deg(y, del_edge(G, e))

   deg_del_edge_ge_outgoing : LEMMA out_deg(y, G) >= out_deg(y, del_edge(G, e))

   deg_del_edge_ge : LEMMA deg(y, G) >= deg(y, del_edge(G, e))

   deg_del_edge_le_incoming : LEMMA in_deg(y, G) - 1 <= in_deg(y, del_edge(G, e))

   deg_del_edge_le_outgoing : LEMMA out_deg(y, G) - 1
                                         <= out_deg(y, del_edge(G, e))

   deg_del_edge_le : LEMMA deg(y, G) - 2 <= deg(y, del_edge(G, e))

   in_deg_edge_exists       : LEMMA in_deg(v,G) > 0 IMPLIES
                             (EXISTS e: (e`2 = v) AND edges(G)(e))

   out_deg_edge_exists      : LEMMA out_deg(v,G) > 0 IMPLIES
                             (EXISTS e: (e`1 = v) AND edges(G)(e))

   deg_edge_exists          : LEMMA deg(v,G) > 0 IMPLIES
                             (EXISTS e: in?(v,e) AND edges(G)(e))

   deg_to_card     : LEMMA FORALL (SG: simple_digraph):
                               deg(v,SG) > 0 IMPLIES size(SG) >= 2

   del_vert_deg_0  : LEMMA deg(v,G) = 0 IMPLIES
                               edges(del_vert(G,v)) = edges(G)

   singleton_loops: LEMMA FORALL (SG: simple_digraph): singleton?(SG)
                          IMPLIES FORALL (e | edges(SG)(e)): self_loop?(e)

   singleton_edges: LEMMA FORALL (SG: simple_digraph): singleton?(SG) IMPLIES
                            incoming_edges(v, SG) = outgoing_edges(v, SG)

   singleton_deg: LEMMA FORALL (SG: simple_digraph):
                            singleton?(SG) IMPLIES in_deg(v, SG) = out_deg(v, SG)

   in_deg_1_sing    : LEMMA in_deg(v, G) = 1 IMPLIES
                           (EXISTS e: incoming_edges(v, G) = singleton(e) AND
                                      e`2 = v AND edges(G)(e))

   out_deg_1_sing   : LEMMA out_deg(v, G) = 1 IMPLIES
                           (EXISTS e: outgoing_edges(v, G) = singleton(e) AND
                                      e`1 = v AND edges(G)(e))

   deg_1_sing       : LEMMA deg(v, G) = 1 IMPLIES
                           (EXISTS e: incident_edges(v, G) = singleton(e) AND
                                      in?(v,e) AND edges(G)(e))

   deg_1_in_out     : LEMMA deg(v, G) = 1 IMPLIES
                           (in_deg(v, G) = 1 AND out_deg(v, G) = 0)
                           OR (in_deg(v, G) = 0 AND out_deg(v, G) = 1)

   deg_1_edge: LEMMA deg(v,G) = 1 IMPLIES
  EXISTS (e:{e:edgetype | edges(G)(e)}, u:{u:T | vert(G)(u)}):
                        (e = (v,u) OR e = (u,v))
   AND v /= u

END digraph_deg

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