Re: [PVS-Help] TCC Question (Stack followup)

```David Coppit wrote:
> On Mon, 3 Oct 2005, Jeff Maddalon wrote:
>
>> Now back to the version with TCCs.  Since the TCCs arise in the
>> definition of
>> way as
>> type.
>
>
> First, thanks to jeff and Bruno for helping me to understand the issue.
>
> One final question: What do I do in cases where the value of the return
> type cannot be easily expressed in terms of the arguments?
>
> e.g. This works:
>
>   multiple_add_sub(x:nat, y:nat): RECURSIVE { u: nat | u=x } =
>     IF y=0 THEN
>       x
>     ELSE
>     ENDIF
>   MEASURE y
>
> but this does not:
>
>   multiple_add_sub(x:nat, y:nat): RECURSIVE { u: nat | y>0 => u>0 } =
>     IF y=0 THEN
>       x
>     ELSE
>     ENDIF
>   MEASURE y
>

You don't have to write x=u. For typecheking, the important property
is that multiple_add_sub(x, y) > 0 when x>0 so there are many options.
You could write

multiple_add_sub(x:nat, y:nat): RECURSIVE { u: nat | x>0 => u>0 }

or  multiple_add_sub(x:nat, y:nat): RECURSIVE { u: nat | u >= x  }

etc.

> In the above I was trying to just provide the type information and not
> x=u. If I have to provide x=u, I wonder what I would do for a nasty
> function whose value isn't easily expressed in terms of the arguments:
>
>   complex(x:nat, y:nat): RECURSIVE { u: nat | u=??? } =
>     IF y=0 THEN
>       x
>     ELSE
>       complex( (x+1) * y * complex(x+2,y-1), y-1)-1
>     ENDIF
>   MEASURE y
>

That's the same thing here. The type {u: nat | x>0 => u>0 } would work.

Bruno

> Thanks,
> David
>
> _____________________________________________________________________
> David Coppit                           david@coppit.org
> The College of William and Mary        http://coppit.org/
>
> "They have computers, and they may have other weapons of mass destruction."
> Former Attorney General Janet Reno, speaking at LLNL of modern criminals
>

--
Bruno Dutertre                             | bruno@csl.sri.com
CSL, SRI International                     | fax: 650 859-2844
333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717

```