Meta-VDM: a reflection-style access to the VDM AST structure for VDM meta-modelling and tool prototyping on top of Overture

[leouk]

Identification of the Originator

Leo Freitas (leo.freitas@newcastle.ac.uk)

Target of the request, defining the affected components of the language definition

AST and Overture

Motivation for the request

To enable a reflection-style access to VDM structures within a VDM specification itself.

Description of the request

Enable writing a VDM model that has as its values/parameters etc features of another (user-level / concrete) VDM model itself. Or to enable to introspect VDM model properties using VDM itself, hence extending Overture, formally, to cope with/generate prototype tools for VDM in VDM, akin to what was done in the Mural theorem prover.

In a way this is just a step further from available (meta-)structure such as inv_T and pre/post_f for type T and function F, which can already even be passed as parameters to other functions. Say, in my other (meta-)VDM model I would also like to query the structure of T (e.g. its accessors and their type signatures) or f (e.g. type signature of f) or whatever else.

description of the modification

I don't know what modification would this entail

benefits from the modification

As described above, but might there be more.

possible side effects

Don't know

A test suite for validation of the modification in the executable models (if appropriate).

TODO

[tomooda]

Leo, It's an interesting proposal. I was thinking about a template engine for VDM source before your post :-)

I have a couple of questions.

1. Do you want it in the form of standard library, say "ASTUtil.vdmsl" or something like that? Or do you want it in the form of new language feature such as ast_ expression by which we can say ast_op to obtain the AST of the operation op?
2. Do you want write accesses to AST to generate new functions/operations/modules/classes at runtime?
3. If write access is possible, do you want it happen at load-time (handled by pre-processors) or at runtime (handled by interpreters)?

[leouk]

Hi Tomo,

On 16 Aug 2016, at 20:50, Tomohiro Oda notifications@github.com<mailto:notifications@github.com> wrote:

Leo, It's an interesting proposal. I was thinking about a template engine for VDM source before your post :-)

Great :-)… I think Marcel and Peter mentioned something similar. This is a nice convergence of ideas!

I have a couple of questions.

1. Do you want it in the form of standard library, say "ASTUtil.vdmsl" or something like that? Or do you want it in the form of new language feature such as ast_ expression by which we can say ast_op to obtain the AST of the operation op?

Yes. I think both? The ASTUtil.vdmsl would be useful to enable prototyping of meta VDM-tools within Overture itself. This reminds me of what I read in the mural theorem prover, and what the Maude tool developers and extends do all the time (e.g. a church-hosser checker, or specific decision procedures, even OO as just another Maude module referring to their corresponding ASTUtils.vdmsl).

The idea to have an ast_ expression is also useful. This would probably be more efficient than via the library and could be used by Overture tool extenders to go beyond just the meta-tool specification towards an implementation?

1. Do you want write accesses to AST to generate new functions/operations/modules/classes at runtime?

Ah… I haven’t thought it that far. When I mentioned reflection it was more read-only to enable capturing / collection of model-based information. The idea to enable write-access is interesting, if potentially dangerous. Worth discussing, perhaps in the next meeting? I am way in transit to Brazil for the August one though :-(

1. If write access is possible, do you want it happen at load-time (handled by pre-processors) or at runtime (handled by interpreters)?

Again, this is interesting. If we enable write access, we should at least also couple it with (meta-) well formedness conditions to enforce some sanity to the process. I need to think that bit through. After reading this it occurred to me why write-access wasn’t on my mind: I haven’t developed tools for low-level VDM, but just to either generate VDM or generate something else from the given VDM.

What potential use do you see for the two varieties of writable ASTs?

Best, Leo

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHubhttps://github.com/overturetool/language/issues/37#issuecomment-240216984, or mute the threadhttps://github.com/notifications/unsubscribe-auth/ABvtwVpjWs1PoAnd4AL6_bMm5wHbwMxEks5qghR7gaJpZM4JRqXl.

[peterwvj]

Based on the outcome of today's Language Board net meeting, the members of the Language Board have all agreed to reject this RM. Generally, the members find this RM rather incomplete and that it does not propose some specific language change for the LB to consider. This makes it difficult for us to progress the RM as it is. You are welcome to submit a revised version of the RM at any time.