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

quality93%

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