Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
abstract_min.pvs
Sprache: Unknown
|
abstract_min[T: TYPE, size: [T -> nat], P: pred[T]]: THEORY
%------------------------------------------------------------------------------
%
% The need for a function that returns the smallest object that
% satisfies a particular predicate arises in many contexts. Thus it is
% useful to develop an "abstract" min theory that can be instantiated in
% multiple ways to provide different min functions. Such a theory must
% be parameterized by
%
% -------------------------------------------------------------------------
% | T: TYPE | the base type over which min is defined |
% | size:[T -> nat] | the size function by which objects are compared |
% | P: pred[T] | the property that the min 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 min_nat
n: VAR nat
S,SS: VAR T
is_one(n): bool = (EXISTS (S: T): P(S) AND size(S) = n)
prep0: LEMMA nonempty?({n: nat | is_one(n)})
min_f: nat = min({n: nat | is_one(n)})
prep1: LEMMA nonempty?({S: T | size(S) = min_f AND P(S)})
minimal?(S): bool = P(S) AND
(FORALL (SS: T): P(SS) IMPLIES size(S) <= size(SS))
min: {S: T | minimal?(S)}
min_def: LEMMA minimal?(min)
min_in : LEMMA P(min)
min_is_min: LEMMA P(SS) IMPLIES size(min) <= size(SS)
END abstract_min
[ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
]
|
|
