Re: Boolean predicate to function

[Dave Stringer-Calvert <dave_sc@csl.sri.com>]

> foo_return(a : nat): nat = 
> 	FORALL(b : nat):
> 		if (foo(a, b)) then
> 			b
> 		else
> 			0
> 		endif

Andre:

There are two things going on here:

The type of your "FORALL" expression above is "bool", not the expected
(according to the declaration) type "nat".  This tickles a bug in the
typechecker, which gives you the failed assertion message.  I'll put this
on our bug tracking system today.

If what you want is to return a value that when used as the second
argument to foo() would cause foo() to be TRUE, then you could use one of
the following forms:

   foo1(a : nat) : nat =
     epsilon({b : nat | foo(a,b)})

   foo2(a : nat) : nat =
     choose({b : nat | foo(a,b)})

   foo3(a : nat) : nat =
     the({b : nat | foo(a,b)})

"epsilon", "choose" and "the" are builtin functions (you can see them in
the prelude with M-x vpf).  They have distinct properties, which you'll
need to decide between depending on what you're trying to accomplish.


foo1 will return a value that satisfies foo(a,b), or if foo(a,b) is false
for all values of b (wrt the current value of a) it will return an
arbitary nat.  This form generates no TCCs.

foo2 will return a nat that is satisfies foo(a,b).  A TCC is generated to
oblige you to prove that such a nat exists for all values of a:

   foo2_TCC1: OBLIGATION
     FORALL (a: nat): nonempty?[nat]({b: nat | foo(a, b)});

foo3 will return the *unique* nat which satifies foo(a,b) for the current
value of a.  A TCC is generated obligating you to prove that a value
exists, and is unique:

   foo3_TCC1: OBLIGATION
     FORALL (a: nat): singleton?[nat]({b: nat | foo(a, b)});


Hope that helps,
Dave

---
Dr Dave Stringer-Calvert,  Senior Project Manager,  Computer Science Lab
SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA
Phone: (650) 859-3291 Fax: (650) 859-2844 David.Stringer-Calvert@sri.com