[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] I want to ask you some questions
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 ? 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.