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

[PVS-Help] Fw:some problems in learing PVS

---------- 转发邮件信息 ----------
发件人:"applehopedream <applehopedream@163.com>"
发送日期:2009-10-21 17:44:50
收件人:pvs <pvs-help@csl.sri.com>
主题: some problems in learing PVS
   I have some problems in learning PVS and I hope someone can help me.Thanks!
   1.expression :DATATYPE
         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?