++++++++++++++++++ FME2001: - Review reports for paper 51 +++++++++++++++++++++ - Dear author(s) : this file was extracted automatically from a very large - mailbox. In case you find any problem concerning mail encodings (or any - other kind of anomaly disturbing your understanding of the reviews) please - email any of the PC cochairs (pamela@research.att.com,jno@di.uminho.pt). ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ PAPER NUMBER: 51 CATEGORY: 2 TITLE: vdmML: using XML to represent VDM on the Web. AUTHOR(S): Brian M. Matthews -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): This paper presents an initial investigation into the use of XML to VDM-SL. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 0 = Out of scope 1 = Marginal interest 2 = Minority interest 3 = Majority interest 4 = Outstanding interest Numeric Rating: 3 Please comment your rating: 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 1 = Strong reject 2 = Weak reject 3 = Could go either way 4 = Weak accept 5 = Strong accept Numeric Rating: 3 NB: There should be a correlation between the two rates above. 4. CONFIDENCE LEVEL: Please provide a rating oof your expertise in the area addressed by the paper, using the scale: 1 = Know virtually nothing about this area 2 = Not too knowledgeable, but I know a bit 3 = Know a moderate amount, about average I'd say 4 = Not my main area of work, but I know a lot about it 5 = My area of work, I know it extremely well Numeric Rating: 3 NB: PC members are responsible for ensuring that 1 is not used here. 5. ORIGINALITY. What is NEW and SIGNIFICANT in the work reported here? Comment: XML have so far been largely ignorred by the FM community. Thus, the new part of the work here is that it takes up this technology. 6. How WORTHWILE is the goal of the authors? Comment: Very 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Yes 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Technically speaking this is a tool paper without any real semantic contents and that is naturally its weakness. 9. APPLICABILITY. If the work is primarily theoretical or conceptual, are the implications in terms of applicability adequately justified? If the paper is about a new formal technique, are satisfactory arguments presented in favor of the new technique? If a methodology is proposed, is it sound? If experimental results are presented, is their relevance justified? Comment: The work presented is conceptually and the implications of the work are adequately described. However, I feel that an important aspect of how to produce vdmML practically by special editors are missing. Without this I feel that the value of vdmML would be quite limited. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: OK. 11. Were there any formatting or mechanical problems with this paper?: There is a number of places where lines are much too long Are the figures and length acceptable?: Yes otherwise Are the references correct?: Yes 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: Here are a few minor comments: p1,bullet 1: Exchange format already available in ASCII p7: many lines are much too long p9,l4: end of sentence missing p10,l12: symbols missing p11: many lines are much too long p14,bullet 1+2: should be combined p14,bullet 3: ideally but hard to achieve +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 51 CATEGORY: 2 TITLE: vdmML: using XML to represent VDM on the Web. AUTHOR(S): Brian M. Matthews -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): This paper reports on-going work to provide an XML format for VDM specifications based on the existing MathML format. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 1 = Marginal interest Numeric Rating: 1 Please comment your rating: The work reported is not finished and the paper does not really provide much of real interest to the FME audience, except for arguing that an XML format for VDM would be a good thing to develop. 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 2 = Weak reject Numeric Rating: 2 NB: There should be a correlation between the two rates above. 4. CONFIDENCE LEVEL: Please provide a rating oof your expertise in the area addressed by the paper, using the scale: 4 = Not my main area of work, but I know a lot about it Numeric Rating: 4 NB: PC members are responsible for ensuring that 1 is not used here. 5. ORIGINALITY. What is NEW and SIGNIFICANT in the work reported here? Comment: Virtually nothing new. Even the proposal for an XML format for VDM has been previously proposed, as the author reports. The reuse of MathML does not seem to be a significant contribution. 6. How WORTHWILE is the goal of the authors? Comment: An XML format for VDM is a worthwhile goal but, in my opinion, it should not be a one person effort. A generic formal methods XML format does not seem to be reasonable. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Reasonably well. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Reasonably sound. 9. APPLICABILITY. If the work is primarily theoretical or conceptual, are the implications in terms of applicability adequately justified? If the paper is about a new formal technique, are satisfactory arguments presented in favor of the new technique? If a methodology is proposed, is it sound? If experimental results are presented, is their relevance justified? Comment: N/A 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Ok, though it contains minor errors. 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: Are the references correct?: Some lines in the code do not respect the right margin. 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: I believe that a discussion on this subject should be carried out within the VDM community, rather than be a proposal of a single person. When a fairly discussed standard XML format for VDM is finished, then it might be reasonable to publish it in a major formal methods conference such as the FME. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 51 CATEGORY: 2 TITLE: vdmML: using XML to represent VDM on the Web. AUTHOR(S): Brian M. Matthews -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper nicely presents an XML representation of VDM specifications. The proposal aims to be compatible with existing standards like MathML, and takes into account future evolutions of XML. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 0 = Out of scope 1 = Marginal interest 2 = Minority interest 3 = Majority interest 4 = Outstanding interest Numeric Rating: 3 Please comment your rating: XML appears nowadays as the obvious way to enable the interchange of information on the web and between tools. Providing XML formats for formal methods is a mandatory task for all formal methods in the coming years. 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 1 = Strong reject 2 = Weak reject 3 = Could go either way 4 = Weak accept 5 = Strong accept Numeric Rating: 4 NB: There should be a correlation between the two rates above. 4. CONFIDENCE LEVEL: Please provide a rating oof your expertise in the area addressed by the paper, using the scale: 1 = Know virtually nothing about this area 2 = Not too knowledgeable, but I know a bit 3 = Know a moderate amount, about average I'd say 4 = Not my main area of work, but I know a lot about it 5 = My area of work, I know it extremely well Numeric Rating: 3 NB: PC members are responsible for ensuring that 1 is not used here. 5. ORIGINALITY. What is NEW and SIGNIFICANT in the work reported here? Comment: The paper proposes an XML format for VDM specifications + associated translation tools into ASCII, HTML and LaTeX 6. How WORTHWILE is the goal of the authors? Comment: Definitely useful for the VDM community, especially for the tool builders, because it favours the interoperability of tools 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Very well 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Not really applicable here. But the paper presents nicely the basic design choices and principles of the XML format proposed. 9. APPLICABILITY. If the work is primarily theoretical or conceptual, are the implications in terms of applicability adequately justified? If the paper is about a new formal technique, are satisfactory arguments presented in favor of the new technique? If a methodology is proposed, is it sound? If experimental results are presented, is their relevance justified? Comment: The work is more technological in nature. It proposes a way to code VDM specifications in XML. The big question is: will this format be adopted by the VDM community as the standard way of encoding VDM into XML. I don't think the paper gives much evidence about this commercial or social issue. But it seems that the choices are reasonable and tend to make a good connection with existing standards and evolutions of XML, which is what we expect from a VDM/XML encoding. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Excellent! The paper is very nicely written for somebody not familiar with XML 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: Are the references correct?: OK 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: detailed comments: page 1. You claim that your tool favours the exchange between different VDM tools. I am not sure this really makes sense because (1) there exists a standard ASCII syntax for VDM (why not use it) (2) there exists only one real commercial VDM tool (VDMtools by IFAD), so interchange is not a major issue in the VDM community. I think that interchange with tools from other communities is more the issue, like the possibility to interchange with Mathematica, or with general purpose theorem provers, or with some XML-based tools like the consistency checker of Finkelstein's team at UCL. page 2, line 4:"provdes" page 4:you should explain what and means at this point (it is explained later but at this point the reader would like that information) page 6. In the footnote you mention the fact that modules are not covered. Is there any technical difficulty in adding modules? Moreover, although not standard, modules are widely used by the VDMtools users. page 7. You mention the fact that your DTD does not prevent a specification from having two state definitions. I also thought that a VDM specification may only have a single set of type definitions (and the same for functions, operations and values) page 7. The example you take is probably a correct VDM specification, but it is somehow surprising to me because it seems to make a recursion in the post-condition. Maybe a more classical example could be used here. Also take care that the ~ did not print in my version of the paper page 8 some XML text does not fit into the page (same at page 11) Also, is it really necessary to put such a long XML text? Only some portions of it are really of interest for the rest of the paper. page 9. In section 4.3 you mention the fact that your mixing of attributes does not conform to MathML. It seems to me that this is a serious drawback if it means that these portions of the text cannot be supported by MathML tools like Mathematica. In this case, the use of MathML is just there to avoid reinventing the wheel, not for interoperability reasons. A similar problem appears at page 10 (footnote 4), because you use MathML symbols with a different semantics. This means that users could apply MathML tools to these sections, and make semantically based transformations that are not correct without being warned of the problem... page 10. You explain how to translate from XML to various formats. How do you address the reverse process: how to translate from various formats (like ASCII) to XML? page10. stlyesheet is mispelled page 13. You mention two interesting transformations which go beyond a purely technological paper: (a) the generation of proof obligations using XSLT (b) the translation into Z or B. Maybe you can use the available space to further develop these aspects (in order to better address the scientific character of the conference) page 14. Your "ambitious longer term aim" seems definitely ambitious, because it means that for example, the Z and VDM communities should eventually agree on the semantics of their languages. When you see that today, they even use different syntax for standard operators (e.g. ran and rng), it means that there is still a lot of patience needed. page 14. at the end of section 7 you consider that some base structures, like modules could be proposed. Your text seems to consider that modules are an independent/orthogonal concepts. I am not really sure it is the case. I think that modules (could) carry a lot of semantics and are not just a syntactical structuring concept. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++