[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 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 pvs-bugs@csl.sri.com 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
> 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
> -------
Ela Teica
Univ of Cincinnati.
Don`t be superstitious; it brings bad luck!:)

test : THEORY


   regs : TYPE+;
   links : TYPE+;

   IMPORTING finite_sets[links]

   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
          add(nr,rec_func(remove(one,l_set), add(nr,r_set)))
    MEASURE card(l_set)

    try: LEMMA FORALL(l_set:finite_set[links],r_set:set[regs]) :
	    (nonempty?(l_set) and nonempty?(difference(fullset[regs],r_set)))
	        IMPLIES nonempty?(rec_func(l_set,r_set))

end test