search

rhit-csse-projects / RESOLVE

RESOLVE (REusable SOftware Language with VErification) is a specification and programming language designed for verifying correctness of object oriented programs.
https://www.cs.clemson.edu/resolve/
BSD 3-Clause "New" or "Revised" License
0 stars 0 forks source link

Specific variations of enhanced facilities not working -- output model needs revision/tweaking #9

Closed AdityaSenthilvel closed 1 month ago

AdityaSenthilvel commented 2 months ago

Enhancements to facilities apparently do not always need to be realized by a specific realization, but can instead be realized solely by the base concept. For instance facilities such as the following are permitted:

facility SF is StackTemplate(Integer, 4) enhanced by XCapability enhanced by YCapability realized by ArrayImpl Notice that no particular implementation is given for XCapability and YCapability -- only ArrayImpl, which also realizes the base concept, StackTemplate. Right now, it seems that our code generation model for Java (and C for that matter) do not consider this possibility.

Aside from the questions of code generation, there is also the question of how implementers of ArrayImpl are to know that they also have to implement the operations specified in XCapability and YCapability... Would the header of StackTemplate communicate this via an enhanced by ... clause? If so, would this have additional ramifications for concept module code generation?

In summary, soon I'll be proposing some tweaks to our current model of output code for java first to help account for these changes. I hope our current (reflection-based) dynamic proxy approach to java facility translation will not need to change too much, though we'll see.

I guess the first step to figuring all of this out might be coming up with a working non-toy example that illustrates a facility and specification used in this way (since, afaik, we have nothing in the current workspace that looks like this).

rhit-fosswe commented 1 month ago

Out of scope for our team (at least for now). Original ticket is from January 31, 2015. It hasn't been mentioned or updated since 2018, so it is likely not relevant (currently).