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

[PVS-Help] some problems in learing PVS



Hi,
   I have some problems in learning PVS and I hope someone can help me.Thanks!
   1.expression :DATATYPE
       BEGIN
         variable(n:nat) :vr?
         svariable(sn:nat) :svr?
       END expression
expression is defined above,but in my proving of some related formulas,variable(v(Bpc)) occurs,where Bpc : var (vr?) and v:[(vr?->nat] ,which is generated by PVS automatically,how can I calculate the value of "variable(v(Bpc))" ?Why proving command should I use?(It ought to be equal to Bpc and I have tried "beta" "assert",but they don't work).
    2.I have defined a type as follows :
     lenh(k : nat) :{x:nat|x>=k}, but now I want to define a variable of it, h : var lenh(k),but it causes an error "there is no resolution for k",how should I correct?
    3.In proving process, I want to prove P1\/p2 with induction, but in odd cases, P1 holds while in even cases,P2 holds.How should I use command
?
    4.I want to  write a recursive function named subform(f:form),where form is an abstract datatype.Then problems arise:
     fl : var list[form]
     prj(fl) is a constructor in form and also considered as a form,and it  will uses subform(nth(fl,n)) for every elements in list[form],but in the definiton of subform,it uses prj(fl).Then I have an chicken and egg problem.How can I solve this problem?



09年新晋3D主流网游《天下贰》,网易六年亿资打造