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

Re: bug?



> 
> To demonstrate the problem I've extracted a few lines from my
> specification:
> 
> test[t: TYPE, c:nat]: THEORY 
> BEGIN
>   P(a:t): int
> END test
> 
> test2[t: TYPE, c:nat]: DATATYPE 
> BEGIN
>   Q(a:t): int
> END test2
> 
> I have the following question. What is the reason that when I try to
> typecheck that text, PVS (PVS 2.1 Test (patch level 2.399)) yields the
> message:
> 
>   Error: No methods applicable for generic function
>   #<STANDARD-GENERIC-FUNCTION MODULE-INSTANCE> with args (NIL) of
>   classes (NULL)
> 
> for the line:
>   Q(a:t): int
> 
> If I continue typechecking I get another message:
>   Could not determine the full theory instance for t
> 
> However, there is no problem with the theory test which has the same
> parameters and the problem disappears if I remove the constant c from
> the datatype.
> 
> Is it a bug, or my understanding of parameterized datatypes is wrong?
> 
> Thanks,
> Michal
> 
> 

You've found a bug.  Sorry.

Anytime you get the Error: .... message, big bug.  Mail it off to
pvs-bugs@csl.sri.com

If you remove the c:nat clause from your theroy-formal clause, your
spec will typecheck.

 test2[t: TYPE]: DATATYPE 
 BEGIN
   Q(a:t): int
 END test2

The documentation says that what goes between the brackets can be an
arbitrary theory-formal clause, but apparently the implementation is
not that robust.

John


==============================++====================
Dr. John Hoffman              ||                    
Secure Computing Corporation  || What do you want to
2675 Long Lake Road           || read for, when you 
Roseville, MN  55124          || can watch TV?      
hoffman@securecomputing.com   ||                    
Fax  :(612)628-2701           ||  - Matilda's Father
Phone:(612)628-2808           ||                    
==============================++====================