# PVS Bug 876

Synopsis: Theory interpretations in PVS3.2
Severity: serious
Priority: medium
Responsible: owre (Sam Owre)
State: open
Class: sw-bug
Arrival-Date: Mon Nov 29 11:20:00 2004
Originator: "Cesar A. Munoz"
Organization: nianet.org
Release: PVS 3.2
Environment:
System:
Architecture:
Description:
I have discovered a family of errors related to typechecking of theory
interpretations in PVS3.2:
Assume:
quadratic : theory
begin
sqrt_ax(x:nnreal): {y:nnreal | y*y = x}
end quadratic
quadratic_io : theory
begin
SQRT : [nnreal->nnreal]
quio : theory = quadratic{{sqrt_ax := SQRT}}
end quadratic_io
1. Typechecking quadratic_io yields:
Illegal reference to SQRT
May not use theory declarations with actuals or mappings that reference
entities declared in this theory.
2. Change the declaration of SQRT to
SQRT : [real->nnreal]
The typechecker returns:
Error: No methods applicable for generic function
3. Delete the declaration of SQRT. Load the PVSio library that defines
SQRT. Then, the file typechecks correctly. Exit PVS, load PVS,
typechecking the file a second time results in:
Error: the assertion (filename theory) failed.
Cesar
PS. The second problem is probably related to:
http://www.csl.sri.com/cgi-bin/pvs/pvs-bug?id=866
--
Cesar A. Munoz H., Senior Staff Scientist mailto:munoz@nianet.org
National Institute of Aerospace mailto://C.A.Munoz@larc.nasa.gov
144 Research Drive http://research.nianet.org/~munoz
Hampton, VA 23666, USA Tel. +1 (757) 766 1539 Fax +1 (757) 766 1855
How-To-Repeat:
Fix: