peterwvj
commented
7 years ago The LB decided to reject this RM. Below is a copy of the email that was sent to the submitter of the RM to explain why the RM was rejected.
Thank you for submitting your recent RM regarding libraries within VDM. We held an Language Board meeting today, and started to discuss what to do with this.
There are a couple of points that we should perhaps clarify. Firstly, the LB is responsible for changes to the VDM language (syntax/semantics), but we do not control the tools (ie. Overture and VDMTools). So changes concerned with the way projects link with libraries is not something that we can progress with an RM. Tool feature changes like this are usually the result of MSc/PhD projects or community contributions. Strictly, the LB cannot even guarantee that the tool writers will implement language changes - it is easier with Overture, as I can often make changes, but with VDMTools we can only give guidance to its Japanese maintainers, and the tools are sometimes out of step.
The second point is that the LB is already responsible for the maintenance of the existing standard libraries (IO, MATH, CSV and VDMUtils). In reality, these libraries have simply been inherited from VDMTools, and not significantly changed since. That isn't to say that other libraries wouldn't be useful, of course.
While discussing your RM it became clear that we do not have a way for anyone to submit a module or classes for inclusion in the "Standard Library Suite". Furthermore, we do not have any guidelines on style or what we would look for in such a submission. This is clearly a problem, and we should address it.
So regarding the RM itself, we are not sure that we can progress it as it stands. The tool suggestion it contains (linkable libraries) is very sensible, but we can only progress this by passing the idea over to the Core group as an enhancement. The RM has drawn attention to our own shortcomings regarding the absence of a "library process", but again we cannot really progress that via the RM process - it is something that we must handle in the regular business of the LB.
So the feeling was that, unless we have misunderstood your request, the RM as it stands should be rejected. We will work on creating a separate process for submission of new libraries, and we will raise the issue of library linkage with Core as a suggested tool enhancement.
Of course, we would be happy to discuss this further if you wish.
Identification of the Originator
Paul Chisholm
Target of the request, defining the affected components of the language definition
Creation of a standard library, language definition not affected
Motivation for the request
The VDM languages are founded on a rich set of data types based on discrete mathematics. While these are powerful data types, there are many general purpose types and functions not included with the language or tools. VDM and Overture combined provide a powerful framework for the creation of specifications, but once one seriously starts building specifications it becomes clear that much groundwork needs to be performed in order to build complete specifications. No doubt many users of VDM/Overture over the years have repeatedly created the same foundational specifications on which to build. VDM needs a core library of general purpose items that can be used widely to assist the community to build specifications.
A collection of examples is provided with an Overture release. These examples provide guidance and techniques, but are mostly not reusable except in very specific circumstances (two exceptions are ISO8601 and VCParser-master). The proposed library would be similar in nature but be limited to items that are truly general in nature. Furthermore, it should be possible to use such items simply by importing in a module header, so that only one copy is ever needed in a single environment (a new release of Overture should not require that all library modules be explicitly re-imported to pick up changes).
No programming language would ever be used widely unless it had a comprehensive set of libraries to ease implementation effort. Specification is no different. One needs to focus on the task at hand without being distracted by having to build foundational items. A collection of libraries seems a pre-requisite for serious industrial use.
Description of the request
A mechanism to be included in Overture that would allow modules to be incorporated as a standard library. This library would be under the governance of the LB to ensure any inclusions truly are general and that quality is maintained (consistent formatting, best practice adopted, comprehensive documentation, etc).
The collection of modules in the VDM-SL ISO8601 example are the kind of thing that is envisaged. The examples demonstrate a problem. Modules that appear in ISO8601 also appear in the SL examples DepartureTMI and VCParser-master because they are used by those other example projects, and to make them standalone there are multiple copies of some modules. Clearly a maintenance issue which would be a somewhat bigger problem in an industrial setting. If we had a library then the example projects would refer to but not include the modules.
description of the modification
No change to the VDM languages. Overture and other tools would need to provide some way to access library modules without the need to import other projects.
benefits from the modification
possible side effects
None
A test suite for validation of the modification in the executable models (if appropriate).
None