# PVS Bug 528

Synopsis: Boolean predicate to function
Severity: serious
Priority: medium
Responsible: dave_sc (Dave Stringer-Calvert)
State: analyzed
Class: sw-bug
Arrival-Date: Sun Mar 4 19:00:04 2001
Originator: Andre Renaud
Organization: student.canterbury.ac.nz
Release: PVS 2.3
Environment:
System:
Architecture:
Description:
I have a fairly simple PVS question. In my current encoding I have a lot
of functions defined in the form:
foo(a, b : nat) : bool =
...
These are generally a predicate which returns true if b is correct for
some a.
I have recently found the need to have these written in the following
style as well:
foo(a : nat): nat =
...
where I now return the value of b. Is there a simple way to write the
second function given the first? I've tried the following, but it isn't
particularly successful:
foo_return(a : nat): nat =
FORALL(b : nat):
if (foo(a, b)) then
b
else
0
endif
But I get the following error message:
Error: the assertion (COMPATIBLE? (TYPE LHS) (TYPE RHS)) failed
Thanks,
--
Andre Renaud
Computer Science Department, University of Canterbury
How-To-Repeat:
test: THEORY
BEGIN
foo(a,b : nat) : bool = a < b
foo(a : nat) : nat =
FORALL (b : nat) :
IF (foo(a,b)) THEN b ELSE 0 ENDIF
END test
M-x typecheck
[1] PVS(16): :bt
Evaluation stack:
MAKE!-EQUATION <-
MAKE-DEF-AXIOM <- (METHOD TYPECHECK* (CONST-DECL T T ...)) <-
(METHOD TYPECHECK* :AROUND ...) <-
(:INTERNAL (:EFFECTIVE-METHOD 4 NIL ...) 0) <- TYPECHECK-DECL <-
TYPECHECK-DECLS <- (METHOD TYPECHECK* (MODULE T T ...)) <-
(METHOD TYPECHECK (MODULE)) <- (METHOD TYPECHECK :AROUND ...) <-
(:INTERNAL (:EFFECTIVE-METHOD 1 T ...) 0) <- TYPECHECK-THEORIES <-
TYPECHECK-FILE <- LET <- [... EXCL::%EVAL ] <- THROW <-
[... EXCL::EVAL-AS-PROGN ] <- LET <- LET <-
[... EXCL::EVAL-AS-PROGN ] <- CATCH <- [... EXCL::%EVAL ] <- EVAL <-
TPL:TOP-LEVEL-READ-EVAL-PRINT-LOOP <- TPL:START-INTERACTIVE-TOP-LEVEL
Fix:
[davesc]
The error is fixed in 2.3.1
Note the specification is malformed as given, and should (and now
does) yield the error:
Typecheck error: Incompatible types for FORALL (b: nat):
IF (foo(a, b)) THEN b ELSE 0 ENDIF
Found: booleans.boolean
Expected: naturalnumbers.nat