++++++++++++++++++ FME2001: - Review reports for paper 60 +++++++++++++++++++++ - 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: 60 CATEGORY: 1 TITLE: Mechanized Analysis of Behavioral Conformance in the Eiffel Base Libraries AUTHOR(S): Steffen Helke Thomas Santen -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): As indicated in the title, but implicitly defines a notion of inheritance for languages like Object-Z which also allows for change of data representation. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 4 0 = Out of scope 1 = Marginal interest 2 = Minority interest 3 = Majority interest 4 = Outstanding interest Numeric Rating: 4 Please comment your rating: The OO programming notion of inheritance is semantically too weak, this paper is a simple step towards fixing that. 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: 5 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: Checking whether the inheritance in a (presumably) well-designed class library is semantically well-behaved seems a rather mechanical exercise, and that is indeed how the HOL-related part of the work appears to have turned out. However, implicitly the authors have merged Z ideas on data refinement with Liskov&Wing subtyping better than I have seen previously. 6. How WORTHWILE is the goal of the authors? Comment: Very, see above. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Quite clearly. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Yes, as far as I can see. 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: I am not sure whether this work has immediate practical relevance in the sense of Eiffel programmers sleeping more soundly in the knowledge that their base class library is OK. However, merging subtyping and inheritance is important. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Very well written, clearly readable throughout, except for the penultimate paragraph on page 12. At least, I don't understand it, but I would welcome a discussion on the relation between contravariance and weakening preconditions. Some minor typos: feasability should be feasibility inhertance in Abstract An important *piece of* information (middle page 1) Condition 1, page 13: CCls should be C 11. Were there any formatting or mechanical problems with this paper?: No Are the figures and length acceptable?: Yes Are the references correct?: Yes 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: I will contact the authors directly to point them to some of our own work that relates to the less well explored areas of Z refinement that they touch on (including the "pushout"). +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 60 CATEGORY: 1 TITLE: Mechanized Analysis of Behavioral Conformance in the Eiffel Base Libraries AUTHOR(S): Steffen Helke Thomas Santen -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper describes a mechanized analysis of some of the class libraries provided with the Eiffel programming language. The objective is to prove behavioral conformance of the inheritance relationships amongst those classes analyzed. 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: The paper reports on formal analysis of a commercial product. It is thus an interesting combination of formal theory and practical requirements. 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: 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: The application of theorem proving technology to the soundness analysis of a commercial OO programming language. 6. How WORTHWILE is the goal of the authors? Comment: From the point of view of an Eiffel user, the relationships which are analyzed in the paper are critical. Therefore the goal of the authors is a valuable one. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: This goal is explained and justified adequately in the introduction, but it is not directly referred to in the conclusion. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Most of the technical material is based on references, so it is difficult to judge soundness. However the material that does appear is 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: The results of the analysis are described and justified both in terms of their implications for Eiffel and from a practical applicability point of view. Thus the justification is quite satisfactory. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The paper is well-written. Just a few minor comments: p3 line 9 - One usually uses the term "descendants" in this context, rather than "heirs". p5 line -4 - "no" |-> "not" p6 para 2 - Sentence beginning "For example, there are no assertions..." This needs more explanation. p6 para 3 - Why not use normal Object-Z? In what sense is it inadequate for your purposes? p7 line 2 - It seems a little strange to use COLLECTION as an example here , when the limitations of CONTAINER were described on the previous page. p7 para 4 - It is unclear what v_i is in [[v_1,...,v_n]]; for instance is it a (value, multiplicity) pair? p13 line 1 - "analogon" |-> "analog" p13 para 4 - One usually talks about reification with respect to VDM rather than refinement. p16 def of M' - This is very difficult to read due to the spacing (in particular the first R term is very difficult) 11. Were there any formatting or mechanical problems with this paper?: No Are the figures and length acceptable?: The paper is 23 pages, but the length is necessary and therefore accetable. Are the references correct?: Yes 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: p11 - The normal reference for Z data refinement is: Jifeng He, C. A. R. Hoare, J. W. Sanders: Data Refinement Refined. ESOP 1986: 187-196 +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++