Quelle examples.pvs Sprache: PVS

%% examples.pvs
%%
%% These examples deal with arbitrary real-valued expressions, for that reason the theory
%% imports strategies instead of strategies4Q.
%%

examples : theory
BEGIN

  IMPORTING strategies

  x,y : var real

  %%%% Examples of numerical

  sqrt23 : LEMMA
    sqrt(2)+sqrt(3)-pi ## [|0.002, 0.007|]
%% The expression (! 1 1) refers to formula 1, 1st term: sqrt(2)+sqrt(3)-pi
%|- sqrt23 : PROOF
%|- (numerical (! 1 1) :verbose? t)
%|- QED

  sin6sqrt2 : LEMMA
    sin(6*pi/180)+sqrt(2) ## [|1.517, 1.520|]
%% The expression (! 1 1) refers to formula 1, 1st term: sin(6*pi/180)+sqrt(2)
%|- sin6sqrt2 : PROOF (numerical (! 1 1)) QED

  %%%% Examples of interval

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

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

  v     : VAR posreal % Ground speed [knots]
  phi   : VAR {deg:real| Tan?(pi*deg/180)} % Bank angle [deg]

  %% Turn rate [deg/sec]
  tr(v,phi) : MACRO real =
    LET PI = pi IN
      ((180*g)/(PI*v*0.514) )*tan((PI*phi)/180)

  tr_250_35 : LEMMA
    LET tr = tr(250,35) IN
      3 <= tr AND tr <= 3.1
%|- tr_250_35 : PROOF (interval) QED

  tr_200_250_abs_35 : LEMMA
    abs(phi) <= 35 AND
    v   ## [| 200, 250 |] IMPLIES
    abs(tr(v,phi)) <= 3.825
%|- tr_200_250_abs_35 : PROOF
%|- (then (skeep) (interval))
%|- QED

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

  X : posreal = 0.5828

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

  common_point: LEMMA EXISTS (x,y,theta,r:real):
    abs(x) <= 1 AND abs(y) <= 1 AND abs(theta) <= 3 AND r ## [|0,1|] AND
    x^2 + y^2 < 3-2*sqrt(2)+0.1 AND (x-(1+r*cos(theta)))^2 + (y-(1+r*sin(theta)))^2 < 0.1
%|- common_point : PROOF (interval :verbose? t) 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 (interval) QED

% The following problems were suggested by Behzad Akbarpour

  epsilon : real = 0.1

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

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

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

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

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

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

  ex7_ba : LEMMA
    x ## [|0,1|] IMPLIES
    exp(x-x^2) - epsilon <= 1 + x
%|- ex7_ba : PROOF (interval) 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
    FORALL (x:real | x ## [| 0, 2.39*10^(-9) |]):
    -0.0059 - 0.000016*exp(-2.55*10^8*x) + 0.031*exp(-5.49*10^7*x) <= 0.03
%|- Tunnel_3_IL : PROOF (interval) QED

  Tunnel_3_IL_LU : LEMMA
    FORALL (x:real | x ## [| 0, 8.17*10^(-8) |]):
    -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 (interval) QED

END examples

quality96%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.