Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/VDM/VDMPP/SAFERPP/ (Wiener Entwicklungsmethode ^©) Datei vom 13.4.2020 mit Größe 1 kB

SSL quadratic.pvs Interaktion und
PortierbarkeitPVS

%----------------------------------------------------------------------------
%
%  Authors: Cesar Munoz, Alfons Geser                   NASA ICASE
%
%  NOTE:
%        Introduced root(a,b,c,eps). x1 and x2 are defined as macros for
%        backward compatibility.
%        Predicate solvable has been eliminated.
%        not_solvable_quadratic is a LEMMA rather than an AXIOM
%        Definitions of x1 and x2 revised.
%        bac renamed discr
%        Consequences of canonical_sq added.
%        Vieta's equations (lemma vieta1 and vieta2) added.
%        x1_eq_x2 added.
%
%----------------------------------------------------------------------------

quadratic : THEORY
BEGIN
  IMPORTING sqrt, sign

  a      : VAR nonzero_real
  aa,b,c : VAR real
  x      : VAR real
  eps    : VAR Sign
  k      : VAR nzreal

  canonical_sq : LEMMA
    a*sq(x) + b*x + c  =
    a*sq(x + b/(2*a)) + (4*a*c - sq(b))/(4*a)

  discr(a,b,c) : real = sq(b) - 4*a*c

  discr_symm : LEMMA
    discr(a,b,c) = discr(-a,-b,-c)

  discr_scalar : LEMMA
    discr(k*a,k*b,k*c) = sq(k)*discr(a,b,c)

  a_gt_0_discr_gt_0 : LEMMA
    a > 0 AND a*sq(x) + b*x + c < 0 IMPLIES
    discr(a,b,c) > 0

  a_gt_0_discr_ge_0 : LEMMA
    a > 0 AND a*sq(x) + b*x + c <= 0 IMPLIES
    discr(a,b,c) >= 0

  a_lt_0_discr_gt_0 : LEMMA
    a < 0 AND a*sq(x) + b*x + c > 0 IMPLIES
    discr(a,b,c) > 0

  a_lt_0_discr_ge_0 : LEMMA
    a < 0 AND a*sq(x) + b*x + c >= 0 IMPLIES
    discr(a,b,c) >= 0

  discr_ge_0 : LEMMA
    a*sq(x) + b*x + c = 0 IMPLIES
    discr(a,b,c) >= 0

  root(a:nonzero_real,b:real,c:real|discr(a,b,c)>=0,eps:Sign):real =
    (-b + eps*sqrt(discr(a,b,c)))/(2*a)

  root_symm : LEMMA
    discr(a,b,c) >= 0 IMPLIES
      root(a,b,c,eps) = root(-a,-b,-c,-eps)

  root_scalar : LEMMA
    discr(a,b,c) >= 0 IMPLIES
      root(k*a,k*b,k*c,eps) = root(a,b,c,sign(k)*eps)

  x1(a:nonzero_real,b:real,c:real|discr(a,b,c)>=0) : MACRO real =
    root(a,b,c,1)

  x2(a:nonzero_real,b:real,c:real|discr(a,b,c)>=0) : MACRO real =
    root(a,b,c,-1)

  vieta1: LEMMA
    discr(a,b,c) >= 0 =>
    x1(a,b,c)+x2(a,b,c) = -b/a

  vieta_add: LEMMA
    discr(a,b,c) >= 0 =>
    root(a,b,c,eps)+root(a,b,c,-eps) = -b/a

  vieta2: LEMMA
    discr(a,b,c) >= 0 =>
    x1(a,b,c)*x2(a,b,c) = c/a

  vieta_mult: LEMMA
    discr(a,b,c) >= 0 =>
    root(a,b,c,eps)*root(a,b,c,-eps) = c/a

  root_neq_0 : LEMMA
    discr(a,b,c) >= 0 AND
    c /= 0 IMPLIES
    root(a,b,c,eps) /= 0

  root_eq_0 : LEMMA
    discr(a,b,c) >= 0 IMPLIES
      (c = 0 AND (b = 0 OR eps = sign(b)) IFF
       root(a,b,c,eps) = 0)

  c_eq_0 : LEMMA
   discr(a,b,c) >= 0 AND
   b = 0 AND
   a*c >= 0
   IMPLIES
    c = 0

  root_eq : LEMMA
    discr(a,b,c) >= 0 IMPLIES
    (discr(a,b,c) = 0 IFF x1(a,b,c) = x2(a,b,c))

  roots_eq_0 : LEMMA
    discr(a,b,c) >= 0 IMPLIES
      (b = 0 AND a*c >= 0
      IFF
      root(a,b,c,-eps) = 0 AND root(a,b,c,eps) = 0)

  root_inv : LEMMA
    discr(a,b,c) >= 0 AND
    c /= 0 IMPLIES
    root(a,b,c,eps) = 1/root(c,b,a,-eps)

  root_le : LEMMA
    discr(a,b,c) >= 0 IMPLIES
    root(a,b,c,-sign(a)) <= root(a,b,c,sign(a))

  root_lt : LEMMA
    discr(a,b,c) > 0 IMPLIES
    root(a,b,c,-sign(a)) < root(a,b,c,sign(a))

  roots_le_ge_0 : LEMMA
   discr(a,b,c) >= 0 IMPLIES
   (a*c <= 0 AND
    (c=0 AND b=0 OR eps=sign(a))
    IFF
    root(a,b,c,-eps) <= 0 AND
    root(a,b,c,eps) >= 0)

  roots_lt_gt_0 : LEMMA
   discr(a,b,c) >= 0 IMPLIES
   (a*c < 0 AND eps=sign(a)
    IFF
    root(a,b,c,-eps) < 0 AND
    root(a,b,c,eps) > 0)

  sign_ab_roots_ge_0 : LEMMA
    discr(a,b,c) >= 0 AND
    a*c >= 0
    IMPLIES
    -sign(a*b)*root(a,b,c,eps) >= 0

  roots_ge_0 : LEMMA
    discr(a,b,c) >= 0
    IMPLIES
      (a*c >= 0 AND a*b <= 0
       IFF
       root(a,b,c,-eps) >= 0 AND
       root(a,b,c,eps) >= 0)

  roots_le_0 : LEMMA
    discr(a,b,c) >= 0 IMPLIES
    (a*c >= 0 AND a*b >= 0
     IFF
     root(a,b,c,-eps) <= 0 AND
     root(a,b,c,eps) <= 0)

  sign_ab_roots_gt_0 : LEMMA
    discr(a,b,c) >= 0 AND
    a*c > 0
    IMPLIES
    -sign(a*b)*root(a,b,c,eps) > 0

  roots_gt_0 : LEMMA
    discr(a,b,c) >= 0 IMPLIES
    (a*c > 0 AND a*b <= 0
     IFF
     root(a,b,c,-eps) > 0 AND
     root(a,b,c,eps) > 0)

  roots_lt_0 : LEMMA
    discr(a,b,c) >= 0 IMPLIES
    (a*c > 0 AND a*b >= 0
     IFF
     root(a,b,c,-eps) < 0 AND
     root(a,b,c,eps) < 0)

  root_gt_0 : LEMMA
    discr(a,b,c) >= 0 IMPLIES
    ((a*c > 0 AND a*b <= 0) OR
     (a*c <= 0 AND eps=sign(a) AND (c /= 0 OR a*b < 0))
     IFF
     root(a,b,c,eps) > 0)

  root_ge_0 : LEMMA
    discr(a,b,c) >= 0 IMPLIES
    ((a*c >= 0 AND a*b <= 0) OR
     (a*c <= 0 AND eps = sign(a))
     IFF
     root(a,b,c,eps) >= 0)

  root_lt_0 : LEMMA
    discr(a,b,c) >= 0 IMPLIES
    ((a*c > 0 AND a*b >= 0) OR
     (a*c <= 0 AND eps=-sign(a) AND (c /= 0 OR a*b > 0))
     IFF
     root(a,b,c,eps) < 0)

  root_le_0 : LEMMA
    discr(a,b,c) >= 0 IMPLIES
    ((a*c >= 0 AND a*b >= 0) OR
     (a*c <= 0 AND eps = -sign(a))
     IFF
     root(a,b,c,eps) <= 0)

  quadratic_aux : LEMMA
    discr(a,b,c) >= 0 =>
    a*sq(x)+b*x+c = a*(x-x1(a,b,c))*(x-x2(a,b,c))

  quadratic_eq_0 : LEMMA
    (a*sq(x) + b*x + c = 0 IFF
      discr(a,b,c) >= 0 AND
      (x = x1(a,b,c) OR
       x = x2(a,b,c)))

  solvable_quadratic : LEMMA
    discr(a,b,c) >= 0 IFF
    EXISTS (x) : a*sq(x) + b*x + c = 0

  not_solvable_quadratic : LEMMA
    NOT discr(a,b,c) >= 0 =>
    ((FORALL(x) : a * sq(x) + b*x + c > 0) OR
     (FORALL(x) : a * sq(x) + b*x + c < 0))

  quadratic_le_0 : LEMMA
    a*sq(x) + b*x + c <= 0 IFF
    ((discr(a,b,c) >= 0 AND
      ((a > 0 AND x2(a,b,c) <= x AND x <= x1(a,b,c)) OR
       (a < 0 AND (x <= x1(a,b,c) OR x2(a,b,c) <= x)))) OR
     (discr(a,b,c) < 0 AND c <= 0))

  quadratic_lt_0 : LEMMA
    a*sq(x) + b*x + c < 0 IFF
    ((discr(a,b,c) >= 0 AND
      ((a > 0 AND  x2(a,b,c) < x AND x < x1(a,b,c)) OR
       (a < 0 AND ((x < x1(a,b,c) AND x < x2(a,b,c)) OR
                   (x1(a,b,c) < x AND x2(a,b,c) < x))))) OR
     (discr(a,b,c) < 0 AND c < 0))

  quadratic_ge_0 : LEMMA
    a*sq(x) + b*x + c >= 0 IFF
    ((discr(a,b,c) >= 0 AND
      ((a < 0 AND x1(a,b,c) <= x AND x <= x2(a,b,c)) OR
       (a > 0 AND (x <= x2(a,b,c) OR x1(a,b,c) <= x)))) OR
     (discr(a,b,c) < 0 AND c >= 0))

  quadratic_gt_0 : LEMMA
    a*sq(x) + b*x + c > 0 IFF
    ((discr(a,b,c) >= 0 AND
      ((a < 0 AND x1(a,b,c) < x AND x < x2(a,b,c)) OR
       (a > 0 AND (x < x2(a,b,c) OR x1(a,b,c) < x)))) OR
     (discr(a,b,c) < 0 AND c > 0))

%% quadratic equations that may collapse to linear equations
%% and the solutions of such equations

  solvable?(aa,b,c): bool =
    (aa = 0 AND b /= 0 OR aa /= 0 AND discr(aa,b,c) >= 0)

  solution(aa,b,(c | solvable?(aa,b,c)), eps: Sign): real =
    IF aa = 0 THEN -c/b ELSE root(aa,b,c,eps) ENDIF

  quadratic_eq_0_full: THEOREM
    aa*sq(x) + b*x + c = 0 IFF
      aa = 0 AND b = 0 AND c = 0 OR
      solvable?(aa,b,c) AND (x = solution(aa,b,c,-1) OR x = solution(aa,b,c,1))

%% --- Some unexpanded forms ---
  quadratic(a,b,c: real)(x): real = a*sq(x) + b*x + c

  complete_square : LEMMA
    quadratic(a,b,c)(x) = a * sq(x + b/(2*a)) + (4*a*c - sq(b))/(4*a)

  quad_eq_0 : THEOREM
    quadratic(a,b,c)(x) = 0 IFF
      discr(a,b,c) >= 0 AND EXISTS (eps): x = root(a,b,c,eps)

  quad_eq_0_full: THEOREM
    quadratic(aa,b,c)(x) = 0 IFF
      aa = 0 AND b = 0 AND c = 0 OR
      solvable?(aa,b,c) AND EXISTS (eps): x = solution(aa,b,c,eps)

END quadratic

quality99%

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.20Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Eine klare Vorstellung vom Zielzustand

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.