++++++++++++++++++ FME2001: - Review reports for paper 26 +++++++++++++++++++++ - 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: 26 CATEGORY: 2 TITLE: Patterns and Simulation Relations for Behavioural Subtyping AUTHOR(S): Heike Wehrheim -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper defines two notions of behavioral subtyping (weak and optimal) in the presence of extra methods in terms of the CSP failure divergence semantics. It defines two subtyping patterns and proves that each of them induces one of the notions of behavioral subtyping. 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: Behavioral subtyping is strongly related to object-orientation and therefore should be a majority interest for FME from the perspective of bringing formal methods into practice. 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: The two notions of subtyping appear to have been published in [FW00]. Thus, the contribution of the paper is to state the two subtyping patterns - which are not very surprising - and to prove them sound against the failure-divergence semantics of behavioral subtyping. 6. How WORTHWILE is the goal of the authors? Comment: The goal, namely to state a number of subtyping patterns which are proven to induce behavioral subtyping, is very worthwhile. Proving behavioral subtyping against the semantics of classes is extremely complex for non-trivial classes. Therefore, to find a set of (practically useful) patterns of subtyping is very interesting. Such a set could also induce a style of programming that would make object-oriented code less brittle with respect to "unexpected behavior". 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Sufficiently well. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: yes. 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 the weak point of the paper: Since the definitions of weak and optimal subtypes have been published before, the paper should discuss the adequacy of the two subtyping patterns from a practical point of view. A malicious reader might argue that the patterns just reflect the most obvious ways of constructing weak and optimal subtypes. No point whatsoever is made to justify the practical appropriateness of the patterns. I very much miss a paragraph along the lines of saying that, in practical applications, inheritance is used in a specific way, which can formally be modeled somehow as a combination of data refinement and the patterns introduced in the paper. If examples of those applications could be cited, that would be a very convincing way of justifying the appropriateness of those patterns for practical work. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: In general, the quality of the writing is ok, but there are some problems with the English. I suggest to have the paper corrected by a native speaker. 11. Were there any formatting or mechanical problems with this paper?: It is not (yet) formatted in LNCS style Are the figures and length acceptable?: Probably. It has 13 pages now, so it will likely have less than 20 in LNCS style. Are the references correct?: yes, but use plain citation style to accord with LNCS formatting requirements. 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: Some general questions: - Is optimal subtyping not too strong a requirement? I suspect most subtypes constructed in practice (and for which polymorphism is to be used) are NOT optimal subtypes. - How can one extend the state by new attributes and get a behavioral subtype in your framework? - What happens if all mutators are introduced as new methods AND sharing is allowed? (A VERY common pattern of inheritance) Detailed comments: Section 1: "certain properties ... are known to be inherited" - which properties? for the uninitiated: explain the difference between "subtyping" and "behavioral subtyping" more precisely use a more precise language: "and _here_ it also allows a designer" - where? "they induce a behav. subtyping relation on their semantics" - the references of "they" and "their" are unclear - who induces what? footnote: what is an "integrated formal method with modelcheckers"? Section 2: What does it mean that "a buffer is still living"? How can an object NOT be alive? typo "$x_j?$ which acts as a[n] guard" typo "a \emph{process} who" -> "... which" Fig. 1: It would be more interesting to see the behavior of Buffer(2) Why is the distinction between events and operations unimportant for the paper? How can the *conjunction* of effect predicates lead to behavioral subtyping? Does it not strengthen the precondition?! Section 3: typo: "This new methods" -> "Those new methods" How does optimal subtyping relate to the "extension rule" of [LW94]? You briefly mention substitutability properties of weak and optimal subtyping. Does one also get the subtyping relations one wants to get? Is their optimal subtyping necessary for substitutability in the context of sharing? Further: Is it necessary to guarantee substitutability in general, or would it be more adequate to have a weaker notion of subtyping which establishes substitutability under conditions that are usually fulfilled in practice? Section 4: To the best of my knowledge, "approbriate" is not an English word - do you mean "appropriate"? "These two simulation relations should easily be generalisable" - be precise: are they or are they not? typo in last sentence: "give _u_s" Section 5: What is a "correct subtype"? The "conclusion" to me is rather inconclusive. "Related work" would be a more adequate title. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 26 CATEGORY: 2 TITLE: Patterns and Simulation Relations for Behavioural Subtyping AUTHOR(S): Heike Wehrheim -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper deals with behavioral subtyping in formal object-oriented specifications (using a Z-like notation and a labelled transition system semantics). Two (mainly) syntactic patterns which guarantee correct subtyping are presented. 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: Correct subtyping is an important issue in formal object-oriented software development. 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. Why? The rating 2 is given because I consider the paper to contain not enough new content w.r.t. previous publications of the author; cf. ORIGINALITY. 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: Syntax, semantics and the two subtyping relations were already presented in previous papers. The only new content are the two patterns (7 lines) and the proof of their correctness (which anyway looks somehow obvious). 6. How WORTHWILE is the goal of the authors? Comment: Is ok. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Is ok. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Mostly ok. 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 patterns can be applied by specifiers without knowledge of the LTS semantics. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: A) In the buffer example one should require alive' = alive for put etc. (Or is there any frame assumption?) B) The menaing of the conjunctions on the bottom of page 5 should be precisely explained. C) Defintion 8 is only a small extension of Definition 7. It is not necessary to repeat all the details of Def. 7. D) Typos: approbriate -> appropriate (several times on page 9) last sentence before the conclusion: ... give as -> give us 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: Are the references correct?: Is ok. 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: It seems that patterns P1 and P2.1 are unneccessary restrictive because one should be able to extend post-conditions of old methods in subclasses if only new attributes are changed (while pre-conditions, enabled-conditions and old attributes remain unchanged). +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 26 CATEGORY: 2 TITLE: Patterns and Simulation Relations for Behavioural Subtyping AUTHOR(S): Heike Wehrheim -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): This paper proposes syntactic subtyping patterns for the state-based part of the specification of classes. These patters guarantee by construction that a subclass is in a behavioural subtyping relation with its superclass. The paper presents a proof of the correctness of these patterns with respect to the respective semantic definitions of subtyping. 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: Behavioural subtyping is an important issue in object-oriented formalisms. It has been very actively studied in recent years, with several papers being published in conferences related to Formal Methods. Furthermore, with the recent advent of 'components of the shelf' approaches and technologies, it has an increasing area of application. 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: 2 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 original technique for behavioural subtyping that is independent of the underlying specification formalism. The technique is almost purely syntactic, being a promising candidate not only for practical applications (also by non-experts), but equally for automatic verification. 6. How WORTHWHILE is the goal of the authors? Comment: it makes perfect sense and it is very promising. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: it is reasonably explained, with clear examples. However, the formalism in which the operational semantics of classes and the subtyping relations are defined (labelled transition systems) is not motivated. Why this particular one and not any other? there are alternatives that have a vast body of research and of theoretical results. My concern is the amount of effort that might be necessary for the automation procedure. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: the definitions are reasonable, and the proofs look like sound, but I did not check. 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 already answered these questions. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: the English is far from being very good. I would recommend a professional revision by a native speaker. 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: yes Are the references correct?: did not check 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: I think it is very important to comment on the possible automatic verification of the relations, giving hints on how can this be done. Regarding terminology, I don't like the identification classes and types. Instead of saying 'subclasses are subtypes' ii would be more rigorous to say 'subclasses are in the subtype relation with'. It is in fact the operational description of a class (considered a type) that is in the subtype realtion with the description of another class. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++