Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: continuous_lambda.pvs Sprache: PVS

Original von: PVS^©

abstract_max[T: TYPE, N: nat, size: [T -> upto[N]], P: pred[T]]: THEORY
%------------------------------------------------------------------------------
%
%  The need for a function that returns the largest object that
%  satisfies a particular predicate arises in many contexts.  Thus it is
%  useful to develop an "abstract" max theory that can be instantiated in
%  multiple ways to provide different max functions.  Such a theory must
%  be parameterized by
%
%    -------------------------------------------------------------------------
%    | T: TYPE          | the base type over which max is defined            |
%    | size:[T -> nat]  | the size function by which objects are compared    |
%    | P: pred[T]       | the property that the max function must satisfy    |
%    -------------------------------------------------------------------------
%
%  Author:
%
%      Ricky W. Butler   NASA Langley
%
%  Version 2.0           Last modified 10/21/97
%
%  Maintained by:
%
%     Rick Butler        NASA Langley Research Center
%                        [email protected]
%
%------------------------------------------------------------------------------
BEGIN

   ASSUMING

   T_ne: ASSUMPTION EXISTS (t: T): P(t)

   ENDASSUMING

   IMPORTING max_upto

   TP: TYPE = {t: T | P(t)}

   n: VAR upto[N]

   S,SS: VAR T

   is_one(n): bool = (EXISTS (S: T): P(S) AND size(S) = n)

   prep0: LEMMA nonempty?({n: upto[N] | is_one(n)})

   max_f: upto[N] = max({n: upto[N] | is_one(n)})

   prep1: LEMMA nonempty?({S: T | size(S) = max_f AND P(S)})

   maximal?(S): bool = P(S) AND
                       (FORALL (SS: T): P(SS) IMPLIES size(S) >= size(SS))

   max: {S: T | maximal?(S)}

   max_def: LEMMA maximal?(max)

   max_in : LEMMA P(max)

   max_is_max: LEMMA P(SS) IMPLIES size(max) >= size(SS)

END abstract_max

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

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.