Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

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

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

```
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools