%% interval_examples.pvs %% %% These examples deal with arbitrary real-valued expressions, for that reason the theory %% imports strategies instead of strategies4Q. %% interval_examples : theory BEGIN IMPORTING interval_arith@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 interval_examples