|
%------------------------------------------------------------------------------
% Sqrare root properties of Complex Numbers.
%
% Author: David Lester, Manchester University
%
% Version 1.0 4/11/07 Initial version (DRL)
%------------------------------------------------------------------------------
complex_sqrt: THEORY
BEGIN
IMPORTING polar, trig_aux
r: VAR real
nnx: VAR nnreal
npx: VAR npreal
x,y,z: VAR complex
n0x,n0y,n0z: VAR nzcomplex
sqrt(z):complex = from_polar(sqrt(abs(z)),arg(z)/2)
sqrt_nz_is_nz : JUDGEMENT sqrt(n0z) HAS_TYPE nzcomplex
sqrt_eq_0 : LEMMA sqrt(z) = 0 IFF z = 0
sqrt_sq : LEMMA sqrt(sq(z)) = IF -pi/2 < arg(z) AND arg(z) <= pi/2
THEN z ELSE -z ENDIF
sq_sqrt : LEMMA sq(sqrt(z)) = z
sqrt_times: LEMMA sqrt(x*y) = IF -pi < arg(x)+arg(y) AND arg(x)+arg(y) <= pi
THEN sqrt(x)*sqrt(y)
ELSE -sqrt(x)*sqrt(y) ENDIF
sqrt_neg : LEMMA sqrt(-z) =
IF arg(z) <= 0 THEN complex_i*sqrt(z) ELSE
-complex_i*sqrt(z) ENDIF
sqrt_inv : LEMMA sqrt(1/n0z)
= IF arg(n0z) = pi THEN -1/sqrt(n0z) ELSE 1/sqrt(n0z) ENDIF
sqrt_div : LEMMA sqrt(x/n0y)
= IF (arg(n0y) = pi & arg(x) > 0) OR
arg(n0y) = 0 OR
(-pi < arg(x)-arg(n0y) & arg(x)-arg(n0y) <= pi)
THEN sqrt(x) / sqrt(n0y) ELSE -sqrt(x) / sqrt(n0y) ENDIF
END complex_sqrt
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.1Angebot
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
|
