[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] importing theory



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
                        


Connect more, do more and share more with Yahoo! India Mail. Learn more.