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

["Jerry James" <loganjerry@xxxxxxxxx>]

2008/5/4 applehopedream <applehopedream@xxxxxxx>:
> 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?

I don't know anything about PPTL, so I'll leave this question to
someone who does.

> 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.

The problem is that your function is defined to return sequ[form], but
your ELSIF and ELSE branches both evaluate to a function from some
restriction on nat to sequ[form].

Have you found the NASA PVS library [1]?  It contains a
"co_structures" library that defines finite and infinite sequences and
a number of operators on them.  If it is missing something you need,
please let me know.

References:
[1] http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html
-- 
Jerry James
http://loganjerry.googlepages.com/