| products/Sources/formale Sprachen/PVS/co_structures/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: interval_bandb.pvs Sprache: PVSUntersuchung PVS© |
|
||||||
|
%% interval_lnexp.pvs
interval_lnexp : THEORY BEGIN IMPORTING lnexp_fnd@exp_approx, lnexp_fnd@ln_approx, interval X,Y : VAR Interval x : VAR real n : VAR nat Exp(n)(X) : (Pos?) = [|exp_lb(lb(X),n),exp_ub(ub(X),n)|] Exp_fundamental: LEMMA X << Y IMPLIES Exp(n)(X) << Exp(n)(Y) Ln(n)(X) : Interval = if lb(X) > 0 AND ub(X) > 0 then [|ln_lb(lb(X),n),ln_ub(ub(X),n)|] else EmptyInterval endif % lemmas Ln_fundamental: LEMMA Pos?(Y) AND Proper?(X) AND X << Y IMPLIES Ln(n)(X) << Ln(n)(Y) Exp_inclusion : LEMMA x ## X IMPLIES exp(x) ## Exp(n)(X) % En En(n) : (Pos?) = Exp(n)([|1|]) Ln_inclusion : LEMMA Pos?(X) AND x ## X IMPLIES ln(x) ## Ln(n)(X) %% Safe version of ln and exp IMPORTING safe_arith safe_Ln(n) : [Interval->Interval] = Safe1(Ln(n)) safe_Exp(n) : [Interval->Interval] = Safe1(Exp(n)) %% Proper version of ln and exp IMPORTING proper_arith Xp : VAR ProperInterval XP : VAR PosInterval Proper_Ln : JUDGEMENT Ln(n)(XP) HAS_TYPE ProperInterval Proper_Exp : JUDGEMENT Exp(n)(Xp) HAS_TYPE ProperInterval proper_Ln(n)(XP) : ProperInterval = Ln(n)(XP) proper_Exp(n)(Xp) : PosInterval = Exp(n)(Xp) END interval_lnexp ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.24Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤ |
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
ZieleEntwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
