Quelle graphs.pvs Sprache: 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
%                        R.W.Butler@larc.nasa.gov
%
%  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

quality88%

¤ 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.