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

*To*: pvs-help@csl.sri.com*Subject*: Mathematical and PVS syntactic equivalence?*From*: Francois Chabot <fch@fun.cediti.be>*Date*: Thu, 19 Jun 1997 18:20:32 +0200*CC*: fch@fun.cediti.be*Organization*: CEDITI - FUNDP*Sender*: fch@fun.cediti.be

Hello, Giving a set of reals S, I am trying to specify a + operation which constructs another set being the same as S except that every member has been added a fixed constant: In PVS I wrote: REALSET: TYPE = setof[real] ; + (I: REALSET, delta: real): REALSET = {t:real | EXISTS(i: real): member(i, I) AND t = i + delta} Mathematically speaking I would rather write something like: ; + (I: REALSET, delta: real): REALSET = {i + delta | member(i, I)} (By the way, are the two specifications equivalent?) I am wondering if it is possible to specify the + operation in a way which would be syntactically (and maybe semantically) closer to the mathematical one... Thank you for your help... -- - François ((((( g( o - )g -oOO--(_)--OOo------------------------------------------------------- | François Chabot Voice: +32-71-259-430 | | CEDITI - FUNDP Fax: +32-71-372-064 | | Avenue Georges Lemaître, 21 email: fch@fun.cediti.be | | .ooo0 6041 Gosselies http://www.fun.cediti.be/~fch/ | | ( ) 0ooo. Belgium | ---\ (--( )-------------------------------------------------------- \_) ) / (_/

- Prev by Date:
**Tcl/Tk** - Next by Date:
**Re: Mathematical and PVS syntactic equivalence?** - Prev by thread:
**Re: composing projections** - Next by thread:
**Re: Mathematical and PVS syntactic equivalence?** - Index(es):