Gedichte Musik Bilder Quellcodebibliothek Diashow Normaldarstellung
Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/FOL/   (Beweissystem Isabelle Version 2025-1©)  Datei vom 16.11.2025 mit Größe 16 kB image not shown  

SSL graph_ops.pvs   Interaktion und
PortierbarkeitPVS

 
%------------------------------------------------------------------------
% 
%  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

89%


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.10Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤

*Eine klare Vorstellung vom Zielzustand




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.