[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 
>   P(a:t): int
> END test
> test2[t: TYPE, c:nat]: DATATYPE 
>   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
>   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

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

 test2[t: TYPE]: DATATYPE 
   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.


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           ||