%-----------------------------------------------------------------------------
% Operators for convenience in writing length comparisons that include
% possibly infinite csequences.
%
% It might be nicer to have an "extended nat" type that includes a special
% "infinity" value. Then we could define the length operator on all
% sequences, which would simplify some other definitions. If you are
% interested in trying this approach, please contact me.
%
% Author: Jerry James <[email protected]>
%
% This file and its accompanying proof file are distributed under the CC0 1.0
% Universal license: http://creativecommons.org/publicdomain/zero/1.0/.
%
% Version history:
% 2007 Feb 14: PVS 4.0 version
% 2011 May 6: PVS 5.0 version
% 2013 Jan 14: PVS 6.0 version
%-----------------------------------------------------------------------------
csequence_length_comp[T1, T2: TYPE]: THEORY
BEGIN
IMPORTING csequence_length[T1], csequence_length[T2]
cseq1: VAR csequence[T1]
cseq2: VAR csequence[T2]
nseq1: VAR nonempty_csequence[T1]
nseq2: VAR nonempty_csequence[T2]
length_lt(cseq1, cseq2): bool =
is_finite(cseq1) AND
(is_finite(cseq2) IMPLIES length(cseq1) < length(cseq2))
length_le(cseq1, cseq2): bool =
is_finite(cseq2) IMPLIES
is_finite(cseq1) AND length(cseq1) <= length(cseq2)
length_eq(cseq1, cseq2): bool =
(is_infinite(cseq1) AND is_infinite(cseq2)) OR
(is_finite(cseq1) AND
is_finite(cseq2) AND length(cseq1) = length(cseq2))
length_ge(cseq1, cseq2): bool =
is_finite(cseq1) IMPLIES
is_finite(cseq2) AND length(cseq1) >= length(cseq2)
length_gt(cseq1, cseq2): bool =
is_finite(cseq2) AND
(is_finite(cseq1) IMPLIES length(cseq1) > length(cseq2))
length_lt_le: THEOREM
FORALL cseq1, cseq2:
length_lt(cseq1, cseq2) IMPLIES length_le(cseq1, cseq2)
length_gt_ge: THEOREM
FORALL cseq1, cseq2:
length_gt(cseq1, cseq2) IMPLIES length_ge(cseq1, cseq2)
length_eq_le: THEOREM
FORALL cseq1, cseq2:
length_eq(cseq1, cseq2) IMPLIES length_le(cseq1, cseq2)
length_eq_ge: THEOREM
FORALL cseq1, cseq2:
length_eq(cseq1, cseq2) IMPLIES length_ge(cseq1, cseq2)
length_lt_neq: THEOREM
FORALL cseq1, cseq2:
length_lt(cseq1, cseq2) IMPLIES NOT length_eq(cseq1, cseq2)
length_gt_neq: THEOREM
FORALL cseq1, cseq2:
length_gt(cseq1, cseq2) IMPLIES NOT length_eq(cseq1, cseq2)
length_eq_empty: THEOREM
FORALL cseq1, cseq2:
length_eq(cseq1, cseq2) IMPLIES (empty?(cseq1) IFF empty?(cseq2))
length_eq_rest: THEOREM
FORALL nseq1, nseq2:
length_eq(nseq1, nseq2) IFF length_eq(rest(nseq1), rest(nseq2))
END csequence_length_comp
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.17Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
