Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Thm.sig Sprache: PVS

Original von: PVS^©

%% metit_examples.pvs

metit_examples : theory
BEGIN

  IMPORTING trig@atan,
            lnexp@ln_exp,
     interval_arith@interval

  x,y : var real

  simple : LEMMA
    FORALL(x:real):
       x*(1-x) <= 1/4
  %|- simple : PROOF (metit) QED

  simple_abs : LEMMA
    FORALL (x:real,y:posreal):
      abs(x*y) <= 1 IMPLIES x*y <= abs(x)*y
% The proof command (metit) also works. This example illustrates that
% metit can be called with multiple formulas.
%|- simple_abs : PROOF
%|- (then (skeep :preds? t) (metit (-3 -4 1)))
%|- QED

  v   : VAR posreal
  phi : VAR real

  sqrtx3 : LEMMA
    x ## [|1,2|] IMPLIES
    sqrt(x)+sqrt(3) <  pi + 0.01
%|- sqrtx3 : PROOF (metit) QED

  g : MACRO posreal = 9.8 % [m/s^2]

  tr_35 : LEMMA
    abs(phi) <= 35 AND
    v   ## [| 200, 250 |] IMPLIES
    abs(180*g*tan(phi*pi/180)/(pi*v*0.514)) ## [|0.000, 3.825|]
%|- tr_35 : PROOF (metit) QED

  V: MACRO posreal=250*0.514  %[m/s]

  tr(phi:(Tan?)): MACRO real = g*tan(phi)/V

  tr_35_le : LEMMA
    3*pi/180 <= tr(35*pi/180)
%|- tr_35_le : PROOF (metit) QED

  sqrt23 : LEMMA
    sqrt(2)+sqrt(3)-pi ## [|0.002, 0.007|]
%|- sqrt23 : PROOF (metit) QED

  sin6sqrt2 : LEMMA
    sin(6*pi/180)+sqrt(2) ## [|1.517, 1.520|]
%|- sin6sqrt2 : PROOF (metit) QED

  G(x|x < 1): MACRO real = 3*x/2 - ln(1-x)

  X : MACRO posreal = 0.5828

  A_and_S : LEMMA
    G(X) > 0
%|- A_and_S : PROOF (metit) QED

  r(x) : MACRO real = x - (11184811/33554432) * x^3
                        - (13421773/67108864) * x^5

  ex(x) : MACRO real = atan(x) - r(x)

  atan_implementation : LEMMA
    abs(x) <= 0.33 IMPLIES
    abs(ex(x)) <= 2^-9
%|- atan_implementation : PROOF (metit) QED

% The following problem provided by Anthony Narkawicz comes from
% the proof of the repulsive criteria in ACCoRD

ajn : LEMMA
    FORALL(sx,sy,vx,vy,nvx,nvy,nwx,nwy,eps,pt,px:real) :
       px > 0 AND pt > 0 AND (eps = 1 OR eps = -1)
       AND nvx * sx + nvy * sy + nvx * nvx * pt + nvy * nvy * pt >= 0
       AND sx * vx + sy * vy < 0 AND sx * vy * eps - sy * vx * eps <= 0
       AND nvy * sx * eps - nvx * sy * eps < 0
       AND nvx * vy * eps - nvy * vx * eps < 0
       AND nvy * sx * eps - nvx * sy * eps <= 0
       AND -1 * (nwx * sy * eps) - nvy * nwx * eps * pt + nwy * sx * eps +
            nvx * nwy * eps * pt
            < 0
       AND nwx * sx + nwy * sy + nvx * nwx * pt + nvy * nwy * pt >
            nvx * sx + nvy * sy + nvx * nvx * pt + nvy * nvy * pt
       AND nwx * vy * eps - nwy * vx * eps < 0
       IMPLIES
       -1 * (nvx * sy * eps * pt) - nwx * sy * eps * px +
        nvy * sx * eps * pt
        + nwy * sx * eps * px < 0

%|- ajn : PROOF
%|- (metit)
%|- QED

% The following problems were suggested by Behzad Akbarpour

  epsilon : MACRO real = 0.1

  ex1_ba : LEMMA
    x ## [|0,1|] IMPLIES
    x - x^2  - epsilon <= ln (1 + x)
%|- ex1_ba : PROOF (metit) QED

  ex2_ba : LEMMA
    x ## [|0,0.9|] IMPLIES
    ln(1-x) - epsilon <= -x
%|- ex2_ba : PROOF (metit) QED

  ex3_ba : LEMMA
    x ## [|0,1/2|] IMPLIES
    -x - 2*sq(x) - epsilon <= ln(1 - x)
%|- ex3_ba : PROOF (metit) QED

  ex4_ba : LEMMA
    x ## [|0,1|] IMPLIES
    abs(ln(1+x) - x) - epsilon <= sq(x)
%|- ex4_ba : PROOF (metit) QED

  ex5_ba : LEMMA
    x ## [|-1/2,0|] IMPLIES
    abs(ln(1+x) - x) - epsilon <= 2*sq(x)
%|- ex5_ba : PROOF (metit) QED

  ex6_ba : LEMMA
    x ## [|0,1|] IMPLIES
    exp(x) - epsilon <= 1 + x + sq(x)
%|- ex6_ba : PROOF (metit) QED

  ex7_ba : LEMMA
    x ## [|0,1|] IMPLIES
    exp(x-x^2) - epsilon <= 1 + x
%|- ex7_ba : PROOF (metit) QED

  quadratic : LEMMA
    FORALL(a,b,c,t:real) :
      a > 0 AND
      a*sq(t) + b*t + c < 0 IMPLIES
      sq(b) > 4*a*c
%|- quadratic : PROOF (metit) QED

%% The following examples are taken from
%% Formal verification of analog designs using MetiTarski
%% William Denman, Behzad Akbarpour, Sofiene Tahar, Mohamed H. Zaki, and Lawrence C. Paulson,
%% FMCAD 2009

  Tunnel_3_IL : LEMMA
    x ## [| 0, 2.39*10^(-9) |] IMPLIES
    -0.0059 - 0.000016*exp(-2.55*10^8*x) + 0.031*exp(-5.49*10^7*x) <= 0.03
%|- Tunnel_3_IL : PROOF (metit) QED

  Tunnel_3_IL_LU : LEMMA
    x ## [| 0, 8.17*10^(-8) |] IMPLIES
    -0.0006427443996*exp(-2.559889987*(10^8*x)) - 0.07600397043 +
     0.1443470449*exp(-4.211001275*(10^6*x))
      ## [| 0, 0.08 |]
%|- Tunnel_3_IL_LU : PROOF (metit) QED

%% The following problem is taken from
%% A. Ayad and C. Marche, Multi-prover verification of floating-point programs,
%% 5th IJCAR 2010.
  Ayad_Marche : LEMMA
    FORALL (r:real) : abs(r) <= 1 IMPLIES
      abs(0.9890365552 + 1.130258690*r + 0.5540440796*r*r - exp(r)) <= (1-2^-16)*2^-4
%|- Ayad_Marche : PROOF (metit) QED

END metit_examples

¤ Dauer der Verarbeitung: 0.3 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.