Process for maintaining the standard libraries

[peterwvj]

As we discussed at the meeting held at the 12th of February 2017, we need to develop a process for managing non-RM issues. This issue is led by @kgpierce .

[nickbattle]

Changed the title of this, after the LB meeting on 12th March.

[paulch42]

Attached is a note containing some motivation for progressing this issue and some initial thoughts. VDM Library.pdf

[kgpierce]

Thanks for getting us started Paul! This is really useful. I think as the Language Board we should restrict ourselves to the process for managing submissions and maintenance of the libraries, and let the tool developers and core decide on how to incorporate such libraries into the tools. It's really useful to record them from an end user perspective.

[nickbattle]

Paul's suggestions seem to be a a sensible direction for this. A couple of points occurred to me.

We (LB) should probably give a hint for the overall structure of the set of libraries, so we have maths and collections and text processing areas, for example, like a Java package structure. That will help us avoid duplicating functionality and draw submitters' attention to what is already provided. I also think that we must require at least SL and PP implementations (RT may be an area of its own with specialized classes) - it seems natural to start with SL, but libraries must be generally accessible when published. Happy to insist on modules for SL rather than flat specs. There might be a case for PP-only libraries if classes implement a particular OO pattern that is not relevant in an SL world.

Happy with the idea of LB review of libraries, though one extra principle may be that we avoid duplication of functions. For example, if a spec needs a library to sort a sequence, the internals of the sort are not important (ie. this isn't a model of a sort, it's a model that has a sorted requirement on its data). Libraries are opaque in that sense. So as long as a sort is reasonably general and efficient, I don't see reason to have several sorting libraries.

[ldcouto]

Hi,

I agree that the LB should not be concerned with the tool implementation of libraries. But I think we need to get someone to look at it. The libraries will not be of much use without at least minimal tool support. At the moment, we lack the resources to do much. Probably the most we can do is add a mechanism to copy the libraries as text files (similar to the current ones). I guess a student project could be used for this but, as Ken says, that's for core to think about.

Also , it would also be good to have 1 example library ready to go when we announce the process. This way people can see what is expected in terms of quality. Perhaps Paul's previous submission can be used?

[kgpierce]

Hello,

I agree with Luis, perhaps Paul can share the libraries (here) that prompted the RM submission and we can use them as a "straw man" to see how review might go? We can also make a wiki page to get these suggestions into a coherent process (is there a way to have them unlisted until we're ready to go live?), as I think they'll be hard to track here.

I think Nick's additions are reasonable, and PP + SL or PP only seems to make sense. I'm not sure about RT: I assume e.g. a sorting library in PP could be used in RT with default timings (so without any changes to the library), and that the end user can wrap calls in cycles / duration to tweak timing as necessary?

I also wondered about native libraries with jar files. Are we expecting submissions to be mainly VDM, or to using calls to native Java such as Collections? How would this affect the submission / review procedure?

[paulch42]

Attached are the latest versions of the modules I use in my specifications. Dates and times are a vital aspect of the specification work I do so I took the effort to create a comprehensive module for dates and times following ISO 8601/RFC 3339.

The other modules are less complete. While they do contain what I would consider fairly generic functions, they have grown as required to support other specifications. No attempt has been made to design a complete set of functions for sets, sequences, etc such as you would find in the Haskell prelude for example.

Also attached are some test modules I created.

One point about the ISO 8601 module. I explicitly made the functions executable to allow model checking. However, the 'implementation' is very inefficient to the extent that it is next to useless for serious model checking. I decided not to change it to be more efficient because that would inevitably change the nature to be more implementation oriented than specification oriented, and for me an understandable specification is the primary goal. This is something we will need to consider. Perhaps a candidate for a native library as mentioned by Ken. If native libraries are an option, then we have both the native library in Java and the VDM module that is the specification of the Java library module.

Archive.zip

[tomooda]

Here's an initial draft of template for LRM (Library Request for Modification). It assumes that we will have a github repository for the standard library, and a pull request is sent before submitting an LRM to the issue tracker.

1. Identification of the Originator.
2. Type of modification (creation / extension / deprecation )
3. Target dialects (VDM-SL / VDM++ / VDM-RT)
4. Target of the request, defining the affected components of the standard library.
5. URL of the pull request (test suite(s) must be included).
6. Motivation for the request.
7. Description of the request, including
   • description of the modification;
   • benefits from the modification such as application domains;
   • possible side effects.

[ldcouto]

Looks good. For number 4, do we want to account for brand new components?

[tomooda]

I expect new component names be listed in 4.

[paulch42]

Notes:

• A new GitHub repository in which library modules are maintained will be created.
• There will be a template for the submission of library proposals. See https://github.com/overturetool/language/issues/41#issuecomment-304629798. The template will be available as a markdown source listing on the wiki.
• Issues proposing additions/changes to the standard library will be labelled with ????
• There will be style guidelines to ensure quality and consistency across the library modules.
• The will be a review checklist against which the LB members will assess a proposal.
• The LB will publish a package hierarchy to reflect the evolving library structure.
• The inclusion of the standard library in tools that implement VDM is not within the purview of the LB.
• In the first instance standard library modules will be restricted to VDM modules and classes. Native modules/classes will be considered once the VDM library process is established.

Draft procedure:

1. Proposer creates new module/class or updates existing library module/class. The module must be consistent with the style guidelines and package hierarchy.
2. Proposer obtains and populates the template for submission of library proposals.
3. Proposer submits completed template by raising an issue in the 'language' repository (https://github.com/overturetool/language).
4. It is preferred the proposer forks the https://github.com/overturetool/documentation repository and submits the proposal as a pull request. In cases where the proposer is not able to do this, the submission may be attached to the proposal issue. At this stage the proposer may also submit a test module, but that is not mandatory.
5. The LB allocates reviewers to the submission. At latest this takes place at the next LB meeting after submission, but could be earlier. A library proposal must be reviewed by not less than two LB members.
6. Allocated LB members review proposal, using the review checklist. Three possible outcomes: accepted as is, accepted with revision, and rejected.
7. The proposer is notified of the outcome with appropriate justification. Response will be provided within 8 weeks of submission.
8. If accepted with change the proposer addresses the comments and resubmits. The same LB members as did the review verify the requested change has been made.
9. Once a module or revision has been accepted the proposer (if they did not do so earlier) submits a test module (in the case of a revision this will be an update to the existing test module).
10. LB members review the test module and verify the submission passes all tests.
11. On successful completion, the new or revised module/class is committed to the standard library GitHub repository.

Test modules:

• There will be a 1-1 mapping between library modules and test modules.
• It must be possible to run all tests in a module with a single command.
• A test module must include at least one test for every type invariant.
• A test module must include at least one test for the equality relation of a type where such a relation is defined.
• A test module must include at least one test for the order relation of a type where such a relation is defined.
• A test module must include at least one test for every function/operation/method in the module under test.
• A test of a function/operation/method must, where relevant, address the pre- and post-condition of the function/operation/method.
• For VDM-SL proposals, test submissions should be presented as a module that contains a single test runner operation (or function) that computes the conjunction of the individual tests, e.g.

runFullSuite: () ==> bool
runFullSuite() ==
  return test1() and test2() and ... testN();

• For VDM++/VDM-RT proposals, test submissions should be implemented as VDMUnit tests.

[ldcouto]

Template and proposal look fine to me. Some comments:

1. Template for issue should be created as a markdown source listing on wiki so people can copy-paste.
2. We should create a label for library modification issues
3. Pull requests should be made from the https://github.com/overturetool/documentation repository. This should be made explicit
4. I'd like some kind of guidance on how many LB members must do a review. I'd like to see 2 minimum

[peterwvj]

• For clarify, replace all occurrences of "Git repository" with "GitHub repository"

• I agree with Luis, just change 4) to say that "It is preferred the proposer forks the https://github.com/overturetool/documentation repository, and submits the proposal as a pull request...".

• I think we need to clarify what we mean by "test module". I would expect the test module to be a set of unit tests that can easily be executed in a single run (e.g. by running runFullSuite). In VDM++/VDM-RT this can easily be implemented using VDMUnit.

[paulch42]

I have updated the draft procedure incorporating comments from Luis and Peter, and added a section on test modules. If I didn't adequately capture any comment please go in and edit as required. A couple of points:

• I added Luis suggestion of a label for library issues. I left it as ???? so please change to something you think is appropriate.
• In reality most library submissions will be executable. Do we want to make that a rule or should we allow submissions that are not executable (which would impact on the requirement for a test module).

[peterwvj]

Thanks for doing this, Paul, it looks good. Regarding the point "For VDM-SL proposals, test submissions...", I'm not sure we need this. It's probably easier to write a test runner that simply computes the conjunction of the individual tests, e.g.

runFullSuite: () ==> bool
runFullSuite() ==
  test1() and test2() and ... testN();

[paulch42]

Sounds good to me Peter, we want to make it as easy as possible. Can you edit the draft as per your suggestion.

[peterwvj]

That's done.

[nickbattle]

This looks good.

I don't really like VDMUnit, and it would be nice if all of the library tests used the same sort of pattern, like the runFullSuite example - though it can be useful to return "seq1 of bool" and possibly have a postcondition that asserts that "elems RESULT = {true}". (On the other hand, a postcondition fail can interrupt automatic execution of the full suite of suites, but then these things must never fail!)

[peterwvj]

As agreed at today's LB NM, the library submission workflow is considered complete. This will be announced via core.