Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: field_examples.pvs Sprache: PVS

Original von: PVS^©

%% Examples of strategies in Field 6.0
%% Cesar Munoz
%% http://shemesh.larc.nasa.gov/people/cam/Field
%% NASA LaRC

field_examples : THEORY
BEGIN

  a,b,c    : VAR real
  pa,pb,pc : VAR posreal
  nza,nzb  : VAR nzreal

  f1 : LEMMA
    a > 1 AND b > 1 =>
    (a+1)/((a+1)/(b+1)) - b = 1
%|- f1 : PROOF (then (skeep) (field)) QED

  f2 : LEMMA
    b >1 AND a > 1 =>
    (b-1)/((b-1)/(a-1)) - a = -1
%|- f2 : PROOF (then (skeep) (field)) QED

  f3 : LEMMA
    b >1 AND a > 1 =>
    (b-1)/((b-1)/(a-1)) - a < 0
%|- f3 : PROOF (then (skeep) (field)) QED

  f4 : LEMMA
    (pa+1)/((pa+1)/(pb+1)) - pb >= 1
%|- f4 : PROOF (then (skeep) (field)) QED

  f5 : LEMMA
    (1+pb+(pa*pb+pa))/(1+pa) - pb = 1
%|- f5 : PROOF (then (skeep) (field)) QED

  f6 : LEMMA
    a > 1 IMPLIES
    a/((a-1) * (a+1)) - 1 /((a-1)*(a+1)) >= 1 /(a+1) - 1
%|- f6 : PROOF (then (skeep) (field)) QED

  f7: LEMMA
    1 - pa*(pb+1) = (pa-1)/(pb+1) IMPLIES
    1/(1+ pb/(1+ 1/(1+pb))) = pa
%|- f7 : PROOF (then (skeep) (field)) QED

  f8: LEMMA
    1 - pa*(pb+1) = (pa-1)/(pb+1) IMPLIES
    1/(1+ pb/(1+ 1/(1+pb))) >= pa
%|- f8 : PROOF (then (skeep) (field)) QED

  f9: LEMMA
    1 - pa*(pb+1) = (pa-1)/(pb+1) IMPLIES
    1/(1+ pb/(1+ 1/(1+pb))) <= pa
%|- f9 : PROOF (then (skeep) (field)) QED

  f10 : LEMMA
    a*(pa+b)/(pa+1) - b*(pa+a)/(pa+1) = 0 IMPLIES a = b
%|- f10 : PROOF (then (skeep) (field - :cancel? t)) QED

  f11 : LEMMA
    a /= 1 IMPLIES
    1 / (1-a) = 1 + a + a * a + (a*a*a)/(1-a)
%|- f11 : PROOF (then (skeep) (field 2)) QED

  cf1 : LEMMA
    4*(pa*pb) + (pa*6)*pa = pa*((c+1)*2) =>
    2*pb + 3*pa - 1 = c
%|- cf1 : PROOF (then (skeep) (cancel-formula -)) QED

  cf2 : LEMMA
    4*(pa*pb) + (pa*6)*pa <= pa*((c+1)*2) =>
    2*pb + 3*pa - c <= 1
%|- cf2 : PROOF (then (skeep) (cancel-formula -)) QED

  cf3 : LEMMA
    4*((pa+1)*pb) + ((pa+1)*6)*(pa+1) = -(pa+1)*((c+1)*2) IMPLIES
    2*pb + 3*(pa+1) + c + 1  = 0
%|- cf3 : PROOF (then (skeep) (cancel-formula -)) QED

  cf4 : LEMMA
   c+2 < 0 IMPLIES
   c*(c+2)*pa + pa*2*(c+2) > pb*pa*(c+2)
%|- cf4 : PROOF (then (skeep) (cancel-formula)) QED

  cf5 : LEMMA
   c+2 < 0 AND
   c*(c+2)*pa + pa*2*(c+2) < b*pa*(c+2) IMPLIES
   b < 0
%|- cf5 : PROOF (then (skeep) (cancel-formula -2)) QED

  gr1 : LEMMA
    a /= -4 IMPLIES
    (a+3)*(a*a+9*a+20)/(a+4) = (a+3)*(a+5)
%|- gr1 : PROOF (grind-reals) QED

  gr2 : LEMMA
    a /= 6 AND a /= 0 AND b = 3/(a*a-6*a) IMPLIES
    (a+3)/(a*(a-6)) = 1/(a-6)+b
%|- gr2 : PROOF (grind-reals) QED

  gr3 : LEMMA
    a /= 6 AND a /=0 IMPLIES
    (a+3)/(a*(a-6)) = 1/(a-6)+3/(a*(a-6))
%|- gr3 : PROOF (grind-reals) QED

%%% The following examples are taken from developments at NASA LaRC
  IMPORTING reals@sqrt

  A           : VAR nzreal
  B,C,Delta,x : VAR real
  eps         : VAR {x:real|x=1 OR x=-1}

  quadratic : LEMMA
    Delta = (B * B) - (4 * (A * C)) AND
    Delta >= 0 AND
    x = (eps * sqrt(Delta) - B) / (2 * A)
    IMPLIES A * x * x + B * x + C = 0
%|- quadratic : PROOF
%|- (then (skeep :preds? t) (replaces (-6 -8)) (field 2))
%|- QED

  t,vix,viy,vox,voy,s : VAR real
  D                   : VAR posreal

  kb3d : LEMMA
    vox > 0 AND
    s*s - D*D > D AND
    s * vix * voy - s * viy * vox /= 0 AND
    ((s * s - D * D) * voy - D * vox * sqrt(s * s - D * D)) /
     (s * (vix * voy - vox * viy)) * s * vox /= 0 AND
    voy * sqrt(s * s - D * D) - D * vox /= 0
    IMPLIES
    (viy * sqrt(s * s - D * D) - vix * D) /
    (voy * sqrt(s * s - D * D) - vox * D)
     =
    (D * D - s * s) /
    (((s * s - D * D) * voy - D * vox * sqrt(s * s - D * D)) /
      (s * (vix * voy - vox * viy)) * s * vox) +
    vix / vox
%|- kb3d : PROOF (grind-reals) QED

END field_examples

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.