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

Re: help, !





Hi,

I do use the 2.3 Version of PVS with the 1.2.2.36 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"
definition. 
I used the finite_set library downloaded from
http://pvs.csl.sri.com/pvs/libraries/

Thank you very much!
ela

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 1.2.2.36)
> 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
DDEL Lab,
Univ of Cincinnati.
 
 
Don`t be superstitious; it brings bad luck!:)
 
____________________________________


test : THEORY

  begin

   regs : TYPE+;
   links : TYPE+;


   IMPORTING finite_sets[links]


   new_reg(r_set:set[regs]) : regs = 
            epsilon(difference(fullset[regs],r_set))

   rec_func(l_set:finite_set[links],r_set: set[regs]) : 
	      RECURSIVE set[regs] = 
	IF empty?(l_set) THEN emptyset[regs]
	ELSE (
	  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)))
	)
	ENDIF
    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