|
%% 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
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.2Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
