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

[PVS-Help] I want to ask you some questions


Dear the receiver:

     hello, Please forgive me that I don't know how to call you.I am a PVS user of China,and in my study of PVS ,I come across some problems.Two of these is following:
1.  I want to use pvs to express the axiomatization of Propositional Projection Temporal Logic(PPTL),but I don't know how to express "prj",that is (P1,P2,P3,....Pm) prj Q ,where Pi(1<=i<=m) and Q is a formula in PPTL.I'd like to use " list",is it suitable?
2. in following specification ,there is a mistake in if _expression_ ,but I can't understand why and how to correct ,so can you help me if you have time ? Thank you very much.

 a part of the specification is :

sequ[ T : TYPE ] : THEORY


    sequ : TYPE = [# infinite : bool, len : nat, seq : ARRAY[{ i:nat | infinite or i<=len } -> T ] #] 

  END sequ

ftp : var sequ[form] %form is formulas

prjns(ftp)(i:nat,l:nat,n:{j:nat|j>=1}) : sequ[form] =
     let m=(n-1)*(l-i+1) in (#infinte := infinite(ftp),len := len(ftp)+m,seq :=

         ( LAMBDA (k: nat):
        (if ( k <= l )  then seq(ftp)(k)

          elsif (k< m+l) then

           (LAMBDA (t:{j:nat|1<=j<=l-i+1}): seq(ftp)(i+t-1))

          else (LAMBDA (x:{j:nat|l<j<=len(ftp)}): seq(ftp)(x))   endif))#)

this is the mistake:
Expecting an _expression_
No resolution for IF with arguments of possible types:
  (k <= l) : booleans.bool
  seq(ftp)(k) : form_adt.form
     IF (k < m + l)
    THEN (LAMBDA (t: {j: nat | b2n(1 <= j) <= l - i + 1}): seq(ftp)(i + t - 1))
  ELSE (LAMBDA (x: {j: nat | b2n(l < j) <= len(ftp)}): seq(ftp)(x)) : [{j:
                                                                          naturalnumbers.nat |
                                                                                         (reals.<=                                                                                     (1,j)),
                                                                                          i))} ->

P.S : thank you a lot,