|Date||2015-08-16 13:00 CET|
|Participants||HS, KP, PGL, NB, PJ, TO. Minutes by PJ.|
Nick has implemented a first version of pure operations in both VDMJ and Overture. There has been some initial testing and a few issues have been reported. PGL will take care of updating the LRM when we get to that.
Shin reported VDMTools to be stable. Other than that there’s nothing new.
I’ve updated VDMJ and Overture to support the “pure operation” feature described by RM#27. This is only enabled in “vdm10” mode (not classic). I need people to test the feature before we merge the change into the main branch. The Overture changes are currently on a separate “ncb/pureoperations” branch. Note also that VDMJ has moved from SourceForge to GitHub (as SF was down for a couple of weeks!). See https://github.com/nickbattle/vdmj.
I (PJ) found some flaws in the way that the JML generator handles atomic execution and state invariants that I have fixed. A new release of the JML generator will ship with the next release of Overture.
When the pure operation implementation is considered stable Overture 2.3 will be released. Peter will talk to Anders (the release manager) about this.
Nothing new reported.
See download stats on the downloads page
Also see Planned Publications.