Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/PVS/digraphs/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 5 kB

Quellcode-Bibliothek digraph_deg.pvs Sprache: 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

quality94%

¤ 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.0.25Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

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.