sir,
i want to express the following code in pvs.
This code is just for a test.
void rtest
{
float da, daprev,cmd,dloc;
dloc=0;
if daprev< 0 then
dloc=dtest(daprev,cmd);
endif
da=dloc;
}
float dtes(x:float,y:float)
{
float z;
z=x+y;
return z;
}
the corresponding pvs files are.....
rtest:THEORY
BEGIN
IMPORTING conf_float32
IMPORTING dtest
flag: VAR bool
da,daprev,cmd,dloc:VAR conf_float32
state:TYPE=[bool,conf_float32,conf_float32,conf_float32,conf_float32]
s1:state
unreachable:state=(FALSE,0,0,0,0)
reachable:[state->bool]=LAMBDA(s:state): (s`1=TRUE)
s2:state=IF s1`1=false then s1 else(s1`1,s1`2,s1`3,s1`4,0)
s3:state=IF less_conf_float32(s2`3,0) = true then s2 else unreachable endif
s4:state=IF s3`1=false then s3 else(s3`1,s3`2,s3`3,s3`4,dtest(s3`3,s3`4)) endif
s5:state= if reachable(s4) then s4 else s2 endif
s6:state=IF s5`1=false then s5 else (s5`1,s5`5,s5`3,s5`4,s5`5) endif
end rtest
dtest(x:conf_float32,y:conf_float32):theory
begin
importing conf_float32
flag:var bool
z:var conf_float32
state:TYPE=[bool,conf_float32,conf_float32,conf_float32]
s1:state
unreachable:state=(FALSE,0,0,0)
reachable:[state->bool]=LAMBDA(s:state): (s`1=TRUE)
s2:state=IF s1`1=false then s1 else(s1`1,s1`2,s1`3,add_conf_float32(s1`2,s1`3))endif
s3:state=IF s2`1=false then s2 else (s2`1,s2`2,s2`3,s2`4) endif
end dtest
when i tried to import dtest using "importing dtest"
the error message came.it was displayed when typechecking the pvs file "rtest.pvs".my aim is statical verification of this code. similarly i also want to use array concept in the code.how can i represent array in pvs.i want to verify whether any "array out of bound" shall occur when code executes.
sujith
|