| products/sources/formale Sprachen/Java/openjdk-20-36_src/test/jdk/com/sun/security/sasl/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: control.ml Sprache: PVSOriginal von: PVS© |
|
||||||
|
sqrt: THEORY
%------------------------------------------------------------------------ % % Square root of non-negative real % % Supercedes older version: sqrt_ax % % Authors: Rick Butler NASA % Cesar Munoz NIA %------------------------------------------------------------------------ BEGIN IMPORTING sq,sign, % sq(a): nonneg_real = a*a sqrt_exists nnx, nny, nnz: VAR nonneg_real a,x,y,z,xx: VAR real sqrt(nnx): {nnz : nnreal | nnz*nnz = nnx} sqrt_pos : JUDGEMENT sqrt(px: posreal) HAS_TYPE posreal % -------------------- Special Arguments -------------------- sqrt_0 : LEMMA sqrt(0) = 0 sqrt_1 : LEMMA sqrt(1) = 1 sqrt_eq_0 : LEMMA sqrt(nnx) = 0 IMPLIES nnx = 0 sqrt_eq_1 : LEMMA sqrt(nnx) = 1 IMPLIES nnx = 1 % -------------------- Basic Properties -------------------- sqrt_lem : LEMMA sqrt(nny) = nnz IFF nnz * nnz = nny sqrt_def : LEMMA sqrt(nnx) * sqrt(nnx) = nnx sqrt_square : LEMMA sqrt(nnx * nnx) = nnx sqrt_sq : LEMMA x >= 0 IMPLIES sqrt(sq(x)) = x sqrt_sq_neg : LEMMA x < 0 IMPLIES sqrt(sq(x)) = -x sqrt_sq_abs : LEMMA sqrt(sq(x)) = abs(x) sqrt_sq_sign : LEMMA sqrt(sq(x)) = sign(x)*x sq_sqrt : LEMMA x >= 0 IMPLIES sq(sqrt(x))=x sqrt_times : LEMMA sqrt(nny * nnz) = sqrt(nny) * sqrt(nnz) sqrt_div : LEMMA nnz /= 0 IMPLIES sqrt(nny / nnz) = sqrt(nny) / sqrt(nnz) abs_sqrt : LEMMA abs(sqrt(nnx)) = sqrt(nnx) sqrt_scal : LEMMA abs(a)*sqrt(nnx) = sqrt(sq(a)*nnx) % --------------------- Inequalities -------------------- sqrt_lt : LEMMA sqrt(nny) < sqrt(nnz) IFF nny < nnz sqrt_le : LEMMA sqrt(nny) <= sqrt(nnz) IFF nny <= nnz sqrt_gt : LEMMA sqrt(nny) > sqrt(nnz) IFF nny > nnz sqrt_ge : LEMMA sqrt(nny) >= sqrt(nnz) IFF nny >= nnz sqrt_eq : LEMMA sqrt(nny) = sqrt(nnz) IFF nny = nnz sqrt_less : LEMMA nnx > 1 IMPLIES sqrt(nnx) < nnx sqrt_more : LEMMA nnx > 0 AND nnx < 1 IMPLIES sqrt(nnx) > nnx sqrt_lt_0 : LEMMA nnx < 0 IFF sqrt(nnx) < 0 sqrt_le_0 : LEMMA nnx <= 0 IFF sqrt(nnx) <= 0 sqrt_gt_0 : LEMMA nnx > 0 IFF sqrt(nnx) > 0 sqrt_ge_0 : LEMMA nnx >= 0 IFF sqrt(nnx) >= 0 sqrt_lt1 : LEMMA nnx < 1 IFF sqrt(nnx) < 1 sqrt_le1 : LEMMA nnx <= 1 IFF sqrt(nnx) <= 1 sqrt_gt1 : LEMMA nnx > 1 IFF sqrt(nnx) > 1 sqrt_ge1 : LEMMA nnx >= 1 IFF sqrt(nnx) >= 1 sqrt_plus_le : LEMMA sqrt(nnx+nny) <= sqrt(nnx) + sqrt(nny) sqrt_cauchy : LEMMA FORALL (a,b,c,d: real): a*c + b*d <= sqrt(sq(a)+sq(b)) * sqrt(sq(c)+sq(d)) sqrt_4 : LEMMA sqrt(4) = 2 sqrt_9 : LEMMA sqrt(9) = 3 sqrt_16 : LEMMA sqrt(16) = 4 sqrt_25 : LEMMA sqrt(25) = 5 AUTO_REWRITE+ sqrt_4 AUTO_REWRITE+ sqrt_9 AUTO_REWRITE+ sqrt_16 AUTO_REWRITE+ sqrt_25 AUTO_REWRITE+ sqrt_0 AUTO_REWRITE+ sqrt_1 AUTO_REWRITE+ sqrt_square AUTO_REWRITE+ sqrt_sq AUTO_REWRITE+ sqrt_sq_neg AUTO_REWRITE+ sq_sqrt END sqrt ¤ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
