++++++++++++++++++ FME2001: - Review reports for paper 20 +++++++++++++++++++++ - 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: 20 CATEGORY: 2 TITLE: An Integrated Refinement Calculus For Z AUTHOR(S): Bing Wu D.R.W. Holton Luming M. Lai -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper presents a refinement calculus that allows the derivation of C programs from Z specifications. It extends Z with a new box: a schema with three parts, where the pre and the postcondition of the operations are separated. The work is based on existing refinement calculi for Z. 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: 1 Please comment your rating: The subject of the paper is very much in the scope of the the conference, but its scientific contribution is very limited. The new box introduced is actually just a graphical notation for Morgan's specification statements. The semantics provided for this construct makes this clear. The refinement laws presented are very similar to those of existing refinement calculi for Z. The paper itself makes reference to a work that presents and proves an extensive set of laws. The only contribution of the paper is an adaptation to the C notation. The case study presented is not illuminating. Most of the results presented are well-known. There are also a few technical flaws. 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: 1 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: 5 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: Very little: the adaptation of the rules to the C notation. 6. How WORTHWILE is the goal of the authors? Comment: On page 3, the authors claim to address the following problems: a. The absence of a refinement method for Z This is not true anymore. As the authors themselves mention, there are already refinement calculi for Z in the literature. b. The difference in the semantic models of refinement calculi, which are usually based on wp semantics, and Z A wp semantics for Z has already been published and is used by the authors. c. The fact that conjunction and disjunction of schemas are not monotonic with respect to refinement. The solution proposed has already been published. The reference is given by the authors themselves. d. The absence of tools. The paper proposes no solution to that, although it mentions the interest of doing so. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Not very well, as I explained above. The goal of developing a tool to support a refinement calculus for Z is very worthwhile, but is not explored at all in this particular paper. The other problems pointed out are already solved. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Not all of them. I detected the following problems. 1. Law 12 cannot be proved in the semantic framework presented. Also, it encompasses the use of data refinement. It's not really a law, but a list of things that one should worry about. 2. Law 14 contemplates a specification P, but the semantics presented later on considers only loops whose bodies are C programs. The semantics presented does not account for the unbounded nondeterminism that can arise if the body of a loop is an arbitrary specification. This well-known problem has several solutions already presented in the literature. Also, the application of this Law on page 11 is not appropriate. The application not only introduces the loop, but transforms the specification into C code. It's not clear what sort of laws are being implicitly applied. 3. Definition 5 is not an accurate description of what is meant by a constructor to be monotonic with respect to refinement. In that context, f was not supposed to be a refinement relation. 4. Example 4 on page 14 uses conjunction of assignments. This is not defined anywhere. 5. The wp semantics of the else-if is wrong as this C construct is not nondeterministic as Dijkstra's if. 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: This question does not seem to apply as the work is not really new. The tool mentioned, however, would be very useful indeed. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The writing is mildly acceptable, although there are quite a few grammar mistakes. Also, long parts of the text are copied ipsis literis from other people work. Finally, in some points notation like \alpha d and dashed predicates is used without explanation. The examples are long and not illuminating. A long list of standard laws is presented without any further explanation or examples. A few slightly interesting laws, that required some adaptation to the C notation, and even some that are not new but complex, are presented without comment or example. 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: Are the references correct?: Yes, as far as I could check. 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: It's contradictory to say that the aim is to keep the incremental software development style of Z through the development process by introducing modified Z. How would that help? It's not clear in the paper at all. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 20 CATEGORY: 2 TITLE: An Integrated Refinement Calculus For Z AUTHOR(S): Bing Wu D.R.W. Holton Luming M. Lai -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): This paper presents a framework and a methodology for refining Z specifications to C code. Initial specifications are stated in modified Z (Z schemas with pre and postconditions). The authors propose refinement rules, based on the refinement calculus, for modified Z. 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: 2 Please comment your rating: This paper doesn't seem to propose something significantly new. In particular, there is no comparison with some others methods, which support refinement (in particular B, which is very similar). 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: 2 NB: There should be a correlation between the two rates above. 4. CONFIDENCE LEVEL: Please provide a rating of 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: 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? 6. How WORTHWILE is the goal of the authors? Comment: The aim of this work is to propose an effective method to refine Z specifications in an incremental way, including conjonction and disjonction schema operators. As far I know, no satisfactory solution exists. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Problems introduced by incremental refinement could be more explained. In particular a more detailed comparison with B, which allows partwise refinement at the level of component, could be interesting. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: There are several technical problems. - In the example of law 1 conditions on ref? and amnt? must be also introduced in the postcondition part (as done after p5). - The example introduced in section 3.1, and used as an illustration for the refinement rules, does not fit the conditions of law 4 (contrary to that is to say). When the two conditions (ref? in 1..TeamSize and amnt? equals conf?) don't hold, the two operations of example 2 are defined. - Law 6 : what does mean Union{gi}\={} ? - Fig 1 : the assignment of the variable sales is omitted. - Law 14 : what means i is not modified (i is a logical variable !). This law strongly depends on the form of P. Example 3 seems me erroneous (you have to write com'(i)={i -> ...} and not com'=com + {i -> ..}), because the for all formula reduces to false. - Example 4 doesn't illustrate the non-monotonicity of schema conjonction, because false => false. A better example for S1 is (x'=1 \/ x'=2). 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 aim of this work is to develop a tool which supports refinement of Z specifications. But nothing is proposed for data refinement and, in particular, to represent Z set operations in C. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The structure of this paper must be improved. The semantics of the refinement relation must be introduced before the introduction of refinement laws. Laws 15-26 must be put in an annex. 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: Are the references correct?: It's OK. 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 20 CATEGORY: 2 TITLE: An Integrated Refinement Calculus For Z AUTHOR(S): Bing Wu D.R.W. Holton Luming M. Lai -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper presents an integration of the Refinement Calculus and the Z specification language. The integration supports the development of C code from Z specifications within the Refinement Calculus. The paper bridges the gap between Z and C by proposing a language called Modified Z and giving a wp semantics to all the involved languages and basing the integration on this semantics. 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: Z is one of the most often used formal specification language but its use is limited to specification as there is no good and reliable way to take a Z specification down to code. 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: 5 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: See 7 below. 6. How WORTHWILE is the goal of the authors? Comment: Questionable. See 7 below. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: My main problem is that the paper makes claims about Z beeing practical, more simpler and more understandable that for instance VDM and B. However, this claim is not justified at all and still this claim is the main driving force behind the paper. The other methods already have everything and even much more (solid formal foundation, methodologies, tool support for automatic code generation and aimation, graphical tools, refinement calculus, theorem-proving tools etc) that this paper tries to develop for Z. I am not convinced that the schema calculus of Z is more powerful than the structuring mechanisms available for instance in the B method. (I have worked with both Z and B so this is based on experience.) Maybe a more fruitful way would be to try to develod methodologies and guidelines to write and structure Z specifications than to extend Z to cover the entire development process. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: They seem sound, but as all the foundational work is done in technical reports I did not check the details. 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: This is difficutl to judge. The paper makes claims that C code is developed, but at least in this paper a small set of the guarded command language is the target language. I was not convinced. The other methods have tools that generate C code automatically. Also the methodological aspects of other methods are much more developed already (see 7 above). 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The writing could be improved. Also at first reading section 3 is not understandable as all the definitions and the semantics of the constructs in given in section 4. When reading section 3 one continuously ends up in concepts not defined. Especially as the Laws and examples seem to be a mixture of Z and C. Moreover, the paper expects that the reader is fluent with Z which is far from true when it come to the audience of FME. 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: Are the references correct?: 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: Have you checked the work of Boiten and Derrick? On page 3 the authors claim that the references 17,1,18 develop a Refinement Calculus for Z. But tjis is surely not true! Also on page 3, the distinction between open-view closed-view is not clear. Theorem 1 on page 15: bad English. Page 15 below Theorem 1: I did not understand the relevance of the sentence However,... means. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++