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

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