samowre
commented
6 years ago Hi Steve,
In general, PVS does allow type expressions in place of a type identifier.
The missing method is a bug, which I need to look at. Could you please send your spec, so I can more easily recreate and fix this?
Type extensions are described in the PVS 4.0 release notes (M-x pvs-release-notes). It's short, so I'm including it below.
Thanks, Sam
Record and Tuple Type Extensions
Record and tuple types may now be extended using the 'WITH' keyword. Thus, one may create colored points and moving points from simple points as follows. point: TYPE = [# x, y: real #] colored_point: TYPE = point WITH [# color: Color #] moving_point: TYPE = point WITH [# vx, vy: real #] Similarly, tuples may be extended: R3: TYPE = [real, real, real] R5: TYPE = R3 WITH [real, real] For record types, it is an error to extend with new field names that match any field names in the base record type. The extensions may not be dependent on the base type, though they may introduce dependencies within themselves. dep_bad: TYPE = point WITH [# z: {r: real | xx + yy < 1} #] dep_ok: TYPE = point WITH [# a: int, b: below(a) #] Note that the extension is a type expression, and may appear anywhere that a type is allowed.
stever00
I am writing something mainly for myself on transliterating Z to PVS. (I know...I'm mad...)
At one point what I WANT to write is (using _ to mimic the priming of Z names...since PVS does not allow primes in identifiers)
Transaction0 : TYPE = [# date : DATE, description : TEXT, amount_ : MONEY #]
(I am modelling the Delta-inclusion idiom from Z here...)
SingleState : TYPE = [# ssaccount : finseq[Transaction_0] #]
SingleState : TYPE = [# ssaccount : finseq[Transaction_0] #]
Then I write this (to mimic inclusion)
PhiDoSomeBusiness : TYPE = {dsm : Transaction0 WITH SingleState WITH SingleState_ | TRUE}
(somewhat simplified, especially using the predicate TRUE).
This give the (bizarre?) error message
Error: No next method for method
If I don’t use the type expression (with the WITHs above) and invent a new identifier instead, as in
Transaction0 : TYPE = [# date : DATE, description : TEXT, amount_ : MONEY #]
SingleState : TYPE = [# ssaccount : finseq[Transaction_0] #]
SingleState : TYPE = [# ssaccount : finseq[Transaction_0] #]
DSM_Type : TYPE = Transaction0 WITH SingleState WITH SingleState_
PhiDoSomeBusiness : TYPE = {dsm : DSM_Type | TRUE}
then it compiles and tcs fine.
So, two things: what does the error mean?; and, this seems to be a general weakness in PVS in that it does not allow type expressions where a type identifier is allowed. But I might be wrong.
Is the fact that WITH can be used to form type expressions in this way documented anywhere? (I found out about it after asking Paolo Masci for help :) )
Thanks!
Steve