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

*To*: jaco@win.tue.nl (Jaco van de Pol)*Subject*: Re: WITH and dependent types*From*: Sam Owre <owre@csl.sri.com>*Date*: Thu, 09 Oct 1997 01:57:15 -0700*cc*: pvs-help@csl.sri.com, wsinjh@win.tue.nl*In-reply-to*: Your message of "Thu, 25 Sep 1997 11:16:06 +0200." <199709250916.LAA20756@wsintt20.win.tue.nl>

Jaco, The language document is out of date, and badly needs to be updated. Otherwise there is no real bug here. As you noted, an override expression with multiple assignments can be separated into a sequence of single assignments only if dependent types are not involved. For dependent record (or tuple) types, the assignments are all done in parallel. In effect, the left-hand sides are all evaluated and then updated with the right-hand sides. Thus [ X |-> add(x,X(s)), (f)(x) |-> x] is equivalent to [(f)(x) |-> x, X |-> add(x,X(s))] With function updates, the domain of the function may be extended if necessary to include the new element. This means that (finite) functions may be built from the empty function. Thus in f(s) WITH [x|-> x] the typechecker checks whether x is of a subtype of the domain type for f, and if it cannot determine it the type for the WITH expression is {y: setof[nat] | X(y) OR y = x} This is why the second form works. I hope this is an adequate explanation; if not, I'm happy to discuss it further. Regards, Sam > Hi, > > I found the following inconvenience in the WITH mechanism, > in combination with dependent types. In fact I wonder > what is the intended behaviour of PVS? > > Given the type S: TYPE = [# X: setof[nat] , f: [(X)->(X)] #], > the function add is defined as follows: > add(s:S, x:nat):S = s WITH > [ X |-> add(x,X(s)), > (f)(x) |-> x] > > This gives two TCCs: > > add_TCC1: OBLIGATION (FORALL (s: S, x: nat): add[nat](x, X(s))(x)); > add_TCC2: OBLIGATION (FORALL (s: S, x: nat): X(s)(x)); > > The first is OK (subtype-tcc). The second is not provable. The more > verbose variant below correctly generates only the first TCC. > > add(s:S, x:nat):S = s WITH > [X |-> add(x,X(s)), > f |-> f(s) WITH [x|-> x]] > > I would expect that either both definitions fail or both succeed. > Both succeed is more practical. Both fail is in accordance with > the PVS language document, which says that multiple overwrites > are rewritten as single overwrites. Note that > (s WITH [X |-> add(x,X(s))] ) WITH [(f)(x) |-> x] > is clearly ill-typed, due to the dependent types.

**References**:**WITH and dependent types***From:*jaco@win.tue.nl (Jaco van de Pol)

- Prev by Date:
**How can I prove this?** - Next by Date:
**How to provide a range of <fnums>** - Prev by thread:
**WITH and dependent types** - Next by thread:
**Re: WITH and dependent types** - Index(es):