[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: Andre Renaud <ajr74@student.canterbury.ac.nz>*Subject*: Re: Boolean predicate to function*From*: Dave Stringer-Calvert <dave_sc@csl.sri.com>*Date*: Sun, 04 Mar 2001 19:12:37 -0800*cc*: pvs@csl.sri.com*In-Reply-To*: Message from Andre Renaud <ajr74@student.canterbury.ac.nz> of "Mon, 05 Mar 2001 14:51:45 +1300." <3AA2F131.8881DB83@student.canterbury.ac.nz>*Sender*: pvs-owner@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

**References**:**Boolean predicate to function***From:*Andre Renaud <ajr74@student.canterbury.ac.nz>

- Prev by Date:
**Boolean predicate to function** - Next by Date:
**Three letter name space is getting crowded** - Prev by thread:
**Boolean predicate to function** - Next by thread:
**Three letter name space is getting crowded** - Index(es):