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/Fortran/Fortran77-Compiler/ (Columbo Version 0.7^©) Datei vom 9.3.2015 mit Größe 2 MB

Impressum cont_vect3_real.pvs Interaktion und
PortierbarkeitPVS

cont_vect3_real: THEORY
%------------------------------------------------------------------------------
%  Continuous functions [ Vect3 -> real]
%
%  Author: Rick Butler     NASA Langley Research Center  2/1/2009
%
%------------------------------------------------------------------------------
BEGIN

  IMPORTING limit_vect3_real

  f, f1, f2      : VAR [Vect3 -> real]
  g              : VAR [Vect3 -> nzreal]
  u              : VAR real
  x, x0          : VAR Vect3
  epsilon, delta : VAR posreal
  n              : VAR nat

  %--------------------
  %  Continuity at x0
  %--------------------

  continuous_vr?(f, x0) : bool =
      FORALL epsilon : EXISTS delta : FORALL x :
         norm(x - x0) < delta IMPLIES abs(f(x) - f(x0)) < epsilon

  continuity_def : LEMMA
        continuous_vr?(f, x0) IFF convergence(f, x0, f(x0))

  continuity_def2 : LEMMA
        continuous_vr?(f, x0) IFF convergent?(f, x0)

  %------------------------------------------
  %  Operations preserving continuity at x0
  %------------------------------------------

  sum_continuous_vr  : LEMMA continuous_vr?(f1, x0) AND continuous_vr?(f2, x0)
                           IMPLIES continuous_vr?(f1 + f2, x0)

  diff_continuous_vr : LEMMA continuous_vr?(f1, x0) AND continuous_vr?(f2, x0)
                           IMPLIES continuous_vr?(f1 - f2, x0)

  prod_continuous_vr : LEMMA continuous_vr?(f1, x0) AND continuous_vr?(f2, x0)
                           IMPLIES continuous_vr?(f1 * f2, x0)

  const_continuous_vr: LEMMA continuous_vr?(const_fun(u), x0)

  scal_continuous_vr : LEMMA continuous_vr?(f, x0) IMPLIES continuous_vr?(u * f, x0)

  neg_continuous_vr  : LEMMA continuous_vr?(f, x0) IMPLIES continuous_vr?(- f, x0)

  div_continuous_vr  : LEMMA continuous_vr?(f, x0) AND continuous_vr?(g, x0)
                            IMPLIES continuous_vr?(f/g, x0)

  inv_continuous_vr  : LEMMA continuous_vr?(g, x0) IMPLIES continuous_vr?(1/g, x0)

  expt_continuous_vr : LEMMA continuous_vr?(f, x0) IMPLIES continuous_vr?(f^n, x0)

  %---------------------------------
  %  Continuity of f in its domain
  %---------------------------------

  continuous_vr?(f): bool = FORALL x0: continuous_vr?(f, x0)

% ------------ Alternate forms and names for convenience ---------------

  sum_cont_vr_fun  : LEMMA continuous_vr?(f1) AND continuous_vr?(f2)
                           IMPLIES continuous_vr?(f1 + f2)

  diff_cont_vr_fun : LEMMA continuous_vr?(f1) AND continuous_vr?(f2)
                           IMPLIES continuous_vr?(f1 - f2)

  prod_cont_vr_fun : LEMMA continuous_vr?(f1) AND continuous_vr?(f2)
                           IMPLIES continuous_vr?(f1 * f2)

  const_cont_vr_fun: LEMMA continuous_vr?(const_fun(u))

  scal_cont_vr_fun : LEMMA continuous_vr?(f) IMPLIES continuous_vr?(u * f)

  neg_cont_vr_fun  : LEMMA continuous_vr?(f) IMPLIES continuous_vr?(-f)

  div_cont_vr_fun  : LEMMA continuous_vr?(f) AND continuous_vr?(g)
                            IMPLIES continuous_vr?(f/g)

  inv_cont_vr_fun  : LEMMA continuous_vr?(g) IMPLIES continuous_vr?(1/g)

  expt_cont_vr_fun : LEMMA continuous_vr?(f) IMPLIES continuous_vr?(f^n)

  %--- Properties ---%

  continuous_vr_fun: TYPE+ = { f | continuous_vr?(f) }

  nz_continuous_vr_fun: TYPE = { g | continuous_vr?(g) }

  h, h1, h2: VAR continuous_vr_fun
  h3: VAR nz_continuous_vr_fun

  sum_fun_continuous_vr : JUDGEMENT  +(h1, h2) HAS_TYPE continuous_vr_fun

  diff_fun_continuous_vr: JUDGEMENT  -(h1, h2) HAS_TYPE continuous_vr_fun

  prod_fun_continuous_vr: JUDGEMENT  *(h1, h2) HAS_TYPE continuous_vr_fun

  const_fun_continuous_vr: JUDGEMENT const_fun(u) HAS_TYPE continuous_vr_fun

  scal_fun_continuous_vr: JUDGEMENT  *(u, h) HAS_TYPE continuous_vr_fun

  neg_fun_continuous_vr : JUDGEMENT -(h) HAS_TYPE continuous_vr_fun

  div_fun_continuous_vr : JUDGEMENT /(h, h3) HAS_TYPE continuous_vr_fun

  inv_fun_continuous_vr : LEMMA continuous_vr?(1/h3)

  expt_fun_continuous_vr: LEMMA continuous_vr?(f) IMPLIES continuous_vr?(f^n)

END cont_vect3_real

quality88%

¤ 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.0.0Bemerkung: Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Bot Zugriff

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.