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

*To*: PVS Help <pvs-help@xxxxxxxxxxx>*Subject*: Re: [PVS-Help] R_pred*From*: Jerome <jerome@xxxxxxxxxxxxxx>*Date*: Fri, 07 Nov 2008 15:18:02 -0800*In-reply-to*: <12250.1226099289@positron.csl.sri.com>*List-help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-id*: PVS-Help <pvs-help.csl.sri.com>*List-post*: <mailto:pvs-help@csl.sri.com>*List-subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <20081106233402.GA16079@cs.caltech.edu> <49144822.5010608@nianet.org> <20081107205525.GD3397@cs.caltech.edu> <12250.1226099289@positron.csl.sri.com>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*User-agent*: Thunderbird 2.0.0.17 (X11/20080925)

Jerome:

When you have a theory parameter given as

R: TYPE FROM nnreal

a subtype predicate R_pred is automatically generated so that R = {s : nnreal | R_pred(s)}.

Now, when you add two expressions a and b of type R and want the result a+b to be of type R, you need to show that

R_pred(a) and R_pred(b) => R_pred(a+b).

One way to avoid this problem is to just use nnreal in place of R. The other option is to add an assumption about R in the ASSUMING section that R is closed under addition.

-Shankar

Jerome <jerome@xxxxxxxxxxxxxx> wrote:

R: TYPE FROM nnreal

Within the theory, distance and W are functions from some type to R:

distance: [D -> R] W: [D, D -> R]

Thus, to discharge [1] do I need to show that the addition of two non-negative real numbers is still a non-negative real number? My original question stems more from surprise (and lazyness) that this wasn't taken care of by some prelude magic :)

Is this what [1] wants me to show? And, in general, how do I interpret the _pred convention? Thanks

jerome

**References**:**[PVS-Help] R_pred***From:*Jerome

**Re: [PVS-Help] R_pred***From:*Cesar Munoz

**Re: [PVS-Help] R_pred***From:*Jerome

**Re: [PVS-Help] R_pred***From:*Natarajan Shankar

- Prev by Date:
**Re: [PVS-Help] R_pred** - Next by Date:
**[PVS-Help] Trees and prewalks** - Previous by thread:
**Re: [PVS-Help] R_pred** - Next by thread:
**[PVS-Help] Trees and prewalks** - Index(es):