| products/Sources/formale Sprachen/JAVA/openjdk-20-36_src/test/hotspot/jtreg/vmTestbase/nsk/monitoring/ThreadMXBean/GetThreadAllocatedBytes/illegalArgumentsTest_proxy_custom/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: perpendicular_3D.pvs Sprache: PVSOriginal von: PVS© |
|
||||||
|
convergence_ops : THEORY %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Limits and operations on sequences of reals %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% BEGIN IMPORTING convergence_sequences, epsilon_lemmas s, s1, s2 : VAR sequence[real] s3 : VAR sequence[nzreal] a : VAR real l, l1, l2 : VAR real n, m, N : VAR nat %--------------------------------- % limits of sum, product, etc. %--------------------------------- cnv_seq_sum : LEMMA convergence(s1, l1) AND convergence(s2, l2) IMPLIES convergence(s1 + s2, l1 + l2) cnv_seq_neg : LEMMA convergence(s1, l1) IMPLIES convergence(-s1, -l1) cnv_seq_diff : LEMMA convergence(s1, l1) AND convergence(s2, l2) IMPLIES convergence(s1 - s2, l1 - l2) cnv_seq_prod : LEMMA convergence(s1, l1) AND convergence(s2, l2) IMPLIES convergence(s1 * s2, l1 * l2) cnv_seq_const : LEMMA convergence(const_fun(a), a) cnv_seq_scal : LEMMA convergence(s1, l1) IMPLIES convergence(a * s1, a * l1) cnv_seq_inv : LEMMA convergence(s3, l2) AND l2 /= 0 IMPLIES convergence(1 / s3, 1 / l2) cnv_seq_div : LEMMA convergence(s1, l1) AND convergence(s3, l2) AND l2 /= 0 IMPLIES convergence(s1 / s3, l1 / l2) cnv_seq_abs : LEMMA convergence(s1, l1) IMPLIES convergence(abs(s1), abs(l1)) cnv_seq_order : LEMMA convergence(s1, l1) and convergence(s2, l2) AND (FORALL n : s1(n) <= s2(n)) IMPLIES l1 <= l2 convergence_shift: LEMMA convergence(s,l) IFF convergence(LAMBDA n: s(n+m),l) %------------- % Squeezing %------------- squeezing_variant : LEMMA convergence(s1, l) and convergence(s2, l) AND (FORALL n : N <= n IMPLIES s1(n) <= s(n) and s(n) <= s2(n)) IMPLIES convergence(s, l) squeezing_const1 : LEMMA convergence(s1, l) AND (FORALL n : N <= n IMPLIES l <= s(n) AND s(n) <= s1(n)) IMPLIES convergence(s, l) squeezing_const2 : LEMMA convergence(s1, l) AND (FORALL n : N <= n IMPLIES s1(n) <= s(n) AND s(n) <= l) IMPLIES convergence(s, l) squeezing : LEMMA convergence(s1, l) and convergence(s2, l) AND (FORALL n : s1(n) <= s(n) and s(n) <= s2(n)) IMPLIES convergence(s, l) squeezing_gen : LEMMA convergence(s1, l) and convergence(s2, l) AND (FORALL n : n >= N IMPLIES s1(n) <= s(n) and s(n) <= s2(n)) IMPLIES convergence(s, l) abs_convergence : COROLLARY convergence(s, 0) IFF convergence(abs(s), 0) %---------------------------------- % Same properties with convergent %---------------------------------- convergent_sum : LEMMA convergent?(s1) AND convergent?(s2) IMPLIES convergent?(s1 + s2) convergent_neg : LEMMA convergent?(s1) IMPLIES convergent?(-s1) convergent_diff : LEMMA convergent?(s1) AND convergent?(s2) IMPLIES convergent?(s1 - s2) convergent_prod : LEMMA convergent?(s1) AND convergent?(s2) IMPLIES convergent?(s1 * s2) convergent_const : LEMMA convergent?(const_fun(a)) convergent_scal : LEMMA convergent?(s1) IMPLIES convergent?(a * s1) convergent_inv : LEMMA convergent?(s3) AND limit(s3) /= 0 IMPLIES convergent?(1 / s3) convergent_div : LEMMA convergent?(s1) AND convergent?(s3) AND limit(s3) /= 0 IMPLIES convergent?(s1 / s3) convergent_abs : LEMMA convergent?(s1) IMPLIES convergent?(abs(s1)) squeezing_abs_0 : LEMMA % BUTLER convergence(s1, 0) AND (FORALL n : abs(s(n)) <= s1(n)) IMPLIES convergence(s, 0) squeezing_abs_0_gen : LEMMA % BUTLER (convergence(s1, 0) AND (EXISTS N: (FORALL n : n >= N IMPLIES abs(s(n)) <= s1(n)))) IMPLIES convergence(s, 0) %--------------------------------- % Types of convergent sequences %--------------------------------- v1, v2 : VAR (convergent?) u : VAR { s3 | convergent?(s3) } convergent_nz?(u) : bool = limit(u) /= 0 v3 : VAR (convergent_nz?) %-------------- % Judgements %-------------- constant_seq1: JUDGEMENT const_fun(a) HAS_TYPE (convergent?) constant_seq2: JUDGEMENT const_fun(b: nzreal) HAS_TYPE (convergent_nz?) conv_seq_plus: JUDGEMENT +(v1, v2) HAS_TYPE (convergent?) conv_seq_minus: JUDGEMENT -(v1, v2) HAS_TYPE (convergent?) conv_seq_times: JUDGEMENT *(v1, v2) HAS_TYPE (convergent?) conv_seq_scal: JUDGEMENT *(a, v1) HAS_TYPE (convergent?) conv_seq_neg: JUDGEMENT -(v1) HAS_TYPE (convergent?) conv_seq_abs: JUDGEMENT abs(v1) HAS_TYPE (convergent?) conv_seq_div1: JUDGEMENT /(v1, v3) HAS_TYPE (convergent?) conv_seq_div2: JUDGEMENT /(a, v3) HAS_TYPE (convergent?) %----------------------------- % Combinations of sequences %----------------------------- limit_sum : LEMMA limit(v1 + v2) = limit(v1) + limit(v2) limit_neg : LEMMA limit(- v1) = - limit(v1) limit_diff : LEMMA limit(v1 - v2) = limit(v1) - limit(v2) limit_prod : LEMMA limit(v1 * v2) = limit(v1) * limit(v2) limit_inv : LEMMA limit(1 / v3) = 1 / limit(v3) limit_div : LEMMA limit(v1 / v3) = limit(v1) / limit(v3) limit_const : LEMMA limit(const_fun(a)) = a limit_scal : LEMMA limit(a * v1) = a * limit(v1) limit_abs : LEMMA limit(abs(v1)) = abs(limit(v1)) %--------------------------------------------------- % Expansion of convergence (for computing limits) %--------------------------------------------------- limit_equiv : LEMMA convergence(s, l) IFF convergent?(s) AND limit(s) = l limit_order : PROPOSITION convergence(s1, l1) AND convergence(s2, l2) AND (FORALL n : s1(n) <= s2(n)) => l1 <= l2 %---------------------------------------------------------------------------- % NOTE: See "convergence_special" in lnexp library for convergence of % sequences involving x^a where a is real % % NOTE: See "series" in series library for convergence of |x|^n and x^n %---------------------------------------------------------------------------- END convergence_ops ¤ Dauer der Verarbeitung: 0.22 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
