Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: graphs.pvs Sprache: PVS

Original von: PVS^©

graphs[T: TYPE]: THEORY
%-------------------------------------------------------------------------------
%
% Defines:
%
%      Graph[T] -- graph over domain T
%      vert(G)  -- vertices of graph G
%      edges(G) -- set of edges in a graph G
%
%  Authors:
%
%      Ricky W. Butler   NASA Langley
%      Jon Sjogren       AFOSR
%
%  Version 1.0           Last modified 12/20/96
%
%  Maintained by:
%
%     Rick Butler        NASA Langley Research Center
%                        [email protected]
%
%  NOTE:
%
%-------------------------------------------------------------------------------
BEGIN

  IMPORTING %finite_sets@finite_sets[T],
            doubletons[T]
            %finite_sets@finite_sets[doubleton[T]]

  R: VAR PRED[[T, T]]
  x,y,v: VAR T

  pregraph: TYPE = [# vert : finite_set[T],
                      edges: finite_set[doubleton[T]] #]

  graph: TYPE = {g: pregraph | (FORALL (e: doubleton[T]): edges(g)(e) IMPLIES
                                     (FORALL (x: T): e(x) IMPLIES vert(g)(x)))}

  e: VAR doubleton[T]
  G: var graph

  edg(x,(y:{y:T | y /= x})): doubleton[T] = dbl[T](x,y)

  edge?(G)(x,y): bool = x /= y AND edges(G)(dbl[T](x,y))

  edge?_comm : LEMMA edge?(G)(y, x) IMPLIES edge?(G)(x, y)

  edges_vert      : LEMMA e(x) AND edges(G)(e) IMPLIES
                             (EXISTS y: x /= y AND vert(G)(y) AND e(y))

  other_vert      : LEMMA e(v) AND edges(G)(e)
                         IMPLIES (EXISTS (u: T): u /= v AND vert(G)(u)
                                                 AND e = dbl[T](u, v))

  edge_has_2_verts: LEMMA x /= v AND e(x) AND e(v)
                                   IMPLIES e = dbl(x,v)

%To aid in discharging TCCs
edges_vert_in: LEMMA e = dbl[T](x, y) AND edges(G)(e)
                       IMPLIES vert(G)(x) AND vert(G)(y)

vert_in: LEMMA edge?(G)(x,y) IMPLIES vert(G)(x) AND vert(G)(y)

% -------------- size of graphs --------------------

  size(G): nat = card[T](vert(G))

  empty?(G): bool = empty?(vert(G))

  singleton?(G): bool = (size(G) = 1)

  isolated?(G): bool = empty?(edges(G))

  empty?_rew          : LEMMA empty?(G) = (card(vert(G)) = 0)

  edges_of_empty      : LEMMA empty?(G)
                                 IMPLIES edges(G) = emptyset[doubleton[T]]

  singleton_edges     : LEMMA singleton?(G) IMPLIES  empty?(edges(G))

  edge_in_card_gt_1   : LEMMA edges(G)(e) IMPLIES card(vert(G)) > 1

  not_singleton_2_vert: LEMMA NOT empty?(G) AND NOT singleton?(G)
                                IMPLIES (EXISTS (x,y: T): x /= y AND
                                     vert(G)(x) AND vert(G)(y))

  infgraph: TYPE = [# vert : set[T],
                      edges: set[doubleton[T]] #]

  graph?(g: infgraph): bool = is_finite[T](vert(g))
                                AND is_finite[doubleton[T]](edges(g))
                                AND (FORALL (e: doubleton[T]): edges(g)(e)
                                     IMPLIES (FORALL x: e(x) IMPLIES vert(g)(x)))

  singleton_graph(v): (singleton?) = (# vert := singleton[T](v),
                                       edges := emptyset[doubleton[T]] #)

  Graph: TYPE = {g: graph | nonempty?(vert(g))}

END graphs

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