Quellcode-Bibliothek max_subgraphs.pvs Interaktion und
PortierbarkeitPVS

max_subgraphs[T: TYPE]: THEORY
BEGIN

   IMPORTING  subgraphs[T], max_upto

   G: VAR graph[T]

   Gpred(G): TYPE = {P: pred[graph[T]] | (EXISTS (S: graph[T]):
                                             subgraph?(S,G) AND P(S))}

   n: VAR nat

   is_one_of_size(G: graph[T], P: Gpred(G),n: nat): bool =
            (EXISTS (S: Subgraph(G)): P(S) AND size(S) = n)

   prep0: LEMMA FORALL (G: graph[T], P: Gpred(G)):
       nonempty?[upto[size(G)]]({n: upto[size(G)] | is_one_of_size(G,P,n)})

   max_size(G: graph[T], P: Gpred(G)): upto[size(G)] =
             max({n: upto[size(G)] | is_one_of_size(G,P,n)})

   prep    : LEMMA FORALL (G: graph[T], P: Gpred(G)):
                            nonempty?[Subgraph(G)]({S: Subgraph(G)
                                | size[T](S) = max_size(G,P) AND P(S)})


   maximal?(G: graph[T], S: Subgraph(G),P: Gpred(G)): bool = P(S) AND
                       (FORALL (SS: Subgraph(G)): P(SS) IMPLIES
                                                        size(SS) <= size(S))

%  Existence TCC satisfied by
%    choose({S: Subgraph(G) | size(S) = max_size AND P(S)})


   max_subgraph(G: graph[T], P: Gpred(G)): {S: Subgraph(G) | maximal?(G,S,P)}

   max_subgraph_def    : LEMMA FORALL (P: Gpred(G)):
                                     maximal?(G,max_subgraph(G,P),P)

   max_subgraph_in     : LEMMA FORALL (P: Gpred(G)): P(max_subgraph(G,P))

   max_subgraph_is_max : LEMMA FORALL (P: Gpred(G)):
                          (FORALL (SS: Subgraph(G)): P(SS) IMPLIES
                                          size(SS) <= size(max_subgraph(G,P)))

END max_subgraphs

quality54%

¤ 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.11Bemerkung: Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.

Quellcode-Bibliothek max_subgraphs.pvs Interaktion und PortierbarkeitPVS

Haftungshinweis

Bemerkung:

Quellcode-Bibliothek max_subgraphs.pvs Interaktion und
PortierbarkeitPVS