| products/sources/formale Sprachen/PVS/lnexp_fnd/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: expt.pvs Sprache: PVSUntersuchung PVS© |
|
||||||
|
expt: THEORY
%---------------------------------------------------------------------------- % % Exponentiation: a^x where both a and x are real-valued % % Author: Rick Butler NASA Langley Research Center % Olga Lightfoot, QMUL % % Version 1.0 8/27/04 % %---------------------------------------------------------------------------- BEGIN IMPORTING ln_exp k,n,m: VAR nat x,t: VAR real epsilon: VAR posreal ^^(a: nnreal,x: {r:real | a /= 0 OR r /= 0}): nnreal = IF a = 0 THEN 0 ELSE exp(x*ln(a)) ENDIF a,b: VAR posreal px,py: VAR posreal nzx: VAR nzreal hathat_sum : LEMMA a^^(n + m) = (a^^n)*(a^^m) hathat_diff : LEMMA a^^(n - m) = (a^^n)/(a^^m) hathat_to_0 : LEMMA px^^0 = 1 hathat_to_1 : LEMMA a^^1 = a hathat_0 : LEMMA 0^^nzx = 0 hathat_1 : LEMMA 1^^x = 1 hathat_nat : LEMMA a^^n = a^n hathat_lt_cross: LEMMA a^^(1/px) < b IMPLIES a < b^^px hathat_gt_cross: LEMMA a^^(1/px) > b IMPLIES a > b^^px hathat_eq_0 : LEMMA a^^nzx = 0 IFF a = 0 hathat_eq_1 : LEMMA px^^x = 1 IFF (x = 0 OR px = 1) hathat_cross : LEMMA a^^(1/px)=b IMPLIES a=b^^px hathat_mult : LEMMA (a^^px)^^py=a^^(px*py) hathat_div : LEMMA (a/px)^^x = a^^x/px^^x hathat_abs : LEMMA abs(a^^x) = abs(a)^^x hathat_sum_posreal: LEMMA (a^^px)*(a^^py)=a^^(px+py) hathat_diff_posreal: LEMMA (a^^px)/(a^^py)=a^^(px-py) hathat_cont : LEMMA continuous?(LAMBDA x: a^^x) % hathat_cont_nn : LEMMA continuous?(LAMBDA (x: posreal): x^^t) % hathat_cont_nnpos : LEMMA continuous?(LAMBDA (x: nnreal): x^^a) AUTO_REWRITE+ hathat_to_0 AUTO_REWRITE+ hathat_to_1 AUTO_REWRITE+ hathat_0 AUTO_REWRITE+ hathat_1 % There are now multiple versions of f(x) = a^x % available in PVS. The prelude provides a version for a^n where n is natural % This theory provides a definition for non-negative a and x real % The complex library provides exp(z) for complex z, from which % we could defined another ^ (not yet done). % I am not happy with naming the lemmas "hathat" but I can't think % of a better name. One could explore the use of theory interpretations % to create an axiomatic version of ^ which is more general than % the current version in the prelude and use these other theories % to show that this axiomatic version is consistent. END expt ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.4Angebot 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 |
