The type language---records in particular

[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)

Transaction_0_ : 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 : Transaction_0_ 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

Transaction_0_ : TYPE = [# date_ : DATE, description_ : TEXT, amount_ : MONEY #]

SingleState : TYPE = [# ssaccount : finseq[Transaction_0] #]

SingleState_ : TYPE = [# ssaccount_ : finseq[Transaction_0] #]

DSM_Type : TYPE = Transaction_0_ 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

[samowre]

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 | x*x + y*y < 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]

Sam, Thanks for the info. My spec is now rather large, but this is everything (and more) you need I hope. Steve

…

On 23/10/2018, at 12:21 PM, Sam Owre ***@***.***> wrote: 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 | x*x + y*y < 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. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#57 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AIVYXN1ubTNVRmcWTwnC4ftxXJnQNganks5unvucgaJpZM4XzWcX>.

[samowre]

Steve, I don't see your specs. Github does not allow many file types to be included, so you may need to send them to me directly. Thanks, Sam