|Date||2015-07-06 13:00 CET|
|Participants||Marcel Verhoef, Nick Battle, Peter Gorm Larsen (chair), Ken Pierce, Shin Sahara, Tomohiro Oda, Hiroshi Sako, Peter Tran-Jørgensen, Shin Sahara, Tomohiro Oda. Minutes by Peter Tran-Jørgensen.|
The request for clarification on constructors being declared static has been agreed and the LRM will be updated soon. See RM #32
Regarding RM #27 the LB has discussed a solution to simply allow operation calls in pre-post and generate run-time errors if the state is modified.
In addition Nick has made a “hack” version as a short term solution to the problem. It simply runs the type check of pre and post conditions with the language version set to classic. Nick will push his work to a branch and we’ll then set up a build job for it to make it accessible.
Finally KP is updating the community process to mention Requests for Clarificaiton explicitly so we have a workflow for these.
v0 of the Isabelle VDM embedding has been completed. At the moment, it’s just the CML embedding minus the reactive definitions and with syntax that’s closer to VDM. The embedding can be found at https://github.com/isabelle-utp/.
The Codegen-based VDM to Isabelle translator has been updated to generate syntax for the new embedding. Also, it is now available as an IDE plugin. It is still too experimental to release (in fact, it depends on an unreleased version of ASTCreator so it cannot even be built by the build server at the moment).
The Alloy translation is now capable of translating (and slicing) VDM-SL models with types and values. It’s also possible to discharge type invariant satisfiability POs via Alloy. Work is proceeding on translating functions at the moment. See https://github.com/EduardoPessoa/PI_MFES for more.
The MC/DC Code Coverage plugin is now integrated in the interpreter via the DBGPv2 protocol. Any model can be intereted and MC/DC data (in the form of an .xml file) will be generated and placed alongside the exiting .covtl files. There is no way to visualize this data at the moment, though that is ongoing work. See https://github.com/jmcPereira/overture for more.
PJ has developed a first version of the VDM-SL to JML generator that generates JML annotations corresponding to the pre/post conditions, state invariants and named type invariants in a VDM-SL model. Just like the VDM-SL to Java generator, the JML generator can currently only be invoked via the command-line although the plan is to also make it accessible via the Overture IDE.
Anders Telkelsen has been hired as release manager by AU for the INTO-CPS project spending a day a week on this. He will also make releases of the Overture tools in the future. It is expected that a next release will be made after the LB issue 27 have been resolved.
See download stats on the downloads page
Also see Planned Publications.
MV will try to remove the stuff we have left on SourceForge.