[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: help, !
I do use the 2.3 Version of PVS with the 220.127.116.11 patch level.
I'm getting the same error every time i'm trying to prove
the lemma in the source attached, and in several other cases
which i couldn't isolate in a simple example as this one.
I hit the error when i'm trying to expand the "rec_func"
I used the finite_set library downloaded from
Thank you very much!
On Tue, 23 May 2000, John Rushby wrote:
> Ela Teica said:
> > I have problems with 'expanding' recursive
> > definitions. get the message:
> > "Error: the assertion (EVERY #'CDR BINDINGS) failed.
> > [condition type: SIMPLE-ERROR]"
> Any time you messages like this, it means PVS has crashed into
> Lisp--that's a bug and we'd like to be told about (it's best to do
> this via firstname.lastname@example.org because then it automatically gets
> logged and tracked).
> However, I cannot recreate this problem using the released version of
> PVS. Are you sure you have the current version? It should say
> PVS Version 2.3 (patch level 18.104.22.168)
> on the PVS Welcome Screen.
> If you can recreate the problem with the current PVS, then please send
> us the script that does it.
> John Rushby
Univ of Cincinnati.
Don`t be superstitious; it brings bad luck!:)
test : THEORY
regs : TYPE+;
links : TYPE+;
new_reg(r_set:set[regs]) : regs =
rec_func(l_set:finite_set[links],r_set: set[regs]) :
RECURSIVE set[regs] =
IF empty?(l_set) THEN emptyset[regs]
LET one:links = epsilon[links](l_set),
nr: regs = new_reg(r_set) IN
try: LEMMA FORALL(l_set:finite_set[links],r_set:set[regs]) :
(nonempty?(l_set) and nonempty?(difference(fullset[regs],r_set)))