++++++++++++++++++ FME2001: - Review reports for paper 49 +++++++++++++++++++++ - 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: 49 CATEGORY: 2 TITLE: From CSP-OZ to Java with Processes AUTHOR(S): Ana Cavalcanti Augusto Sampaio -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper exposes a method to translate a specification in CSP-OZ into a Java programs. The paper presents and discuss the main translating rules. 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 possibility of going from specification to executable program is useful for a lot of domains: prototyping, animation of specifications, model checking, test construction... A general translation method (even if not yet fully developped, proved and automated) allows to ease the translation. 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. [Edited, original= Numeric rating: 4 for CSP processes, 3 for Java, 2 for OZ] 5. ORIGINALITY. What is NEW and SIGNIFICANT in the work reported here? Comment: The main interest is showing how to systematically translate form CSP-OZ to Java. The paper gives a fair idea of what are the problems arising from the fact that the target environment (Java, and a library for Occam) is a general and well accepted system and not an ad-hoc environment where one can adapt the semantics according to his translating needs. 6. How WORTHWILE is the goal of the authors? Comment: A general method to obtain executable programs form specification is useful for a lot of reasons: prototyping, animation of specifications, test construction.. The method is not yet complete, proved or automated, and may not be suitable for efficient implementations, but some of these points are discussed and problems are shown. 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: The main problem with this article is that it tries to cover too much. Some discussed points are difficult to follow as they are not enough explained (due to a lack of space?). Paragraph 4 is very long (it exposes the method), but sometimes too detailled and sometimes not detailled enough. - For example I do not understand the purpose of the discussion about the fact that local channels communicate no values: Is this a limitation of the translating method, of CSP-OZ (but in that case you should not have to ``prove'' this)? And what is the interest of this kind of construction? - Same remark on the interest of discussing Integer vs int. (PS: I do not suggest to add more explanations, but simplification or suppression.) On the other side some points are not clear enough. For example: - What are the arguments and the semantics of ``Guard''. - The paper says that ``the Guard constructor is to be implemented''. Have you done it? - There are CSP constructs which are difficult to translate, or need a lot of rewriting (interrupt, interleaving). It is not clear if they are supported now, in the future, or are a definitive restriction to the translation. Is this a problem of Java, or of the CTJ library? And are they useful in classic CSP-OZ specifications? 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 method seems to be sound and to cover a reasonnably large subset of CSP. The paper presents the principles of the method, and provides no attempt to formalize or prove the translation rules. As the paper states, this is not a trivial problem (mapping CSP and Java semantics is not a simple task), Some unanswered question are: - do the authors plan to automatize the method (develop a tool, or integrate in a existing environment)? - Since the translation of CSP is not complete, are the unsupported constructs current or very useful in classic CSP-OZ ? I do not know enough about methods to develop the control part of a CSP-OZ specifications, but surely any method implies preference for some constructions, and ignorance of others. Therefore I should be interested to know how the restrictions interfere with a methodic development of specifications. Or can we avoid the badly supported constructs by using an adequate refinement method? 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The quality of writing is correct (I am not a english native :-). But there is some typing errors (varibles, operatores, unneccessary, modfify, tranform ...) Also the notations are not stable, and sometimes names of variables change into the same phrase. For example: - com_get: com is in boldface normally but sometimes in italics - on top of page 3 val (line 2) becomes v in line 3 - at the beginning of 4.1, why is c translated into cons? I suggest a careful check of both spelling and consistency of notations. 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: Interesting work but presentation should be improved. I strongly encourage the authors to provide less technical details or only a partial coverage of the translation rules. This would make it easier for the reader to understand the basic principles and the structure of these translation rules which are currently hidden by the mass of details. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 49 CATEGORY: 2 TITLE: From CSP-OZ to Java with Processes AUTHOR(S): Ana Cavalcanti Augusto Sampaio -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): CSP-OZ is translated into Java. The paper is not concerned with the OZ parts of the translation, assumes a refinement calculus will suffice. The CSP translation uses a Java csp library. 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: Link between theory and a practical language. 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 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: Although it is worthwhile work, given the fact that a csp.lang library is available in Java, it is not at all surprising that a translation like this can be made. It is disappointing to see how complicated the resulting Java is and how many restrictions on CSP appear throughout. The bits of refinement calculus shown are completely obvious and trivial, and can be safely omitted. 6. How WORTHWILE is the goal of the authors? Comment: Worthwhile alright. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Reasonably. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: They appear to be, though I am disappointed (and thus not convinced) that so often different things need to be done depending on what kind of variable is concerned. 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: Yes fine. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The spelling is terrible, a spell checker would easily find the many variations on "nondeterministic" and many other typos. The language is OK otherwise, but silly errors (esp of case) have crept up in many places. I think the main drawback of this paper is that it does not clearly separate the interesting details from the drudgery. I see restrictions and complications coming from at least 3 directions: - Java as a sometimes clumsy programming language - the tightening of Object-Z variable use conventions, made in the combination with CSP - the restrictions emposed by csp.lang on "real CSP". As a result, the translations appear ridiculously complex, and it is hardly ever clear which of these three causes the complication at various points. 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: The definition of enable_c (p3) is suspect. By existentially quantifying over the input, restrictions on the input are discounted in general - *except* when they are universally false (for this specific before state), which will also lead to enable_c becoming false - is this really the intention? If so, the matching text is incorrect. Page 4: unclear what is meant by "the CSP part ... in [12]", and whether that is acceptable for a relatively unknown language. Page 6: emphasis not on techniques on data refinement that are applicable: the fact that they are applicable is a not entirely trivial compositionality result, see recent work by Smith and Derrick. Page 7, discussion on local vs non-local channels is unclear, this leads to many questions later on. Page 7: Channel-of-Any seems to be a misnomer, as it really is a Channel-of-None. Channel-of-Any would better refer to Channel-of-Object, which is probably the class that is wrapped up (with castings) in any Channel-of-Type. The examples of refinement calculus are very trivial. Clearly the specification statement on page 8 could be replaced by the Boolean assignment res = enable_ci just like it is done for integer assignments in a later example. Page 9: ci is an input schema?? Page 14: unclear why local channels and input channels have to be distinguished, and why is there an alternative to waiting for the input to happen?? The output channel prefix rule *does* use the Guard constructor as it stands. Section 4.4 says nothing interesting. The separation of pre and postcondition is entirely obvious; most refinement rules are concerned with assignment, which is exactly the case for which you know that you don't really need to introduce specification statements in the first place. It is also obvious (eg for Init) that you can shift predicates from a schema to a specification statement. Conclusions: indeed the resulting Java is very slow, through the overhead of processes. I would add that the resulting Java is mostly obvious, too, where it concerns the translation of the CSP part of CSP-OZ into the CJT library. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 49 CATEGORY: 2 TITLE: From CSP-OZ to Java with Processes AUTHOR(S): Cavalcanti, Sampaio -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): Contains rules to transform a CSP-OZ specification into a Java program. 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: 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: 6. How WORTHWILE is the goal of the authors? Comment: 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: 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 don't know Java, so I am not a good judge of the technical details of this paper. In this review, I assume that they are largely correct. I am very dubious about the value of this approach. There are a great many complicated rules, none of them validated by formal specification (impractical) or implementation (much more practical). As I read the conclusions, the authors propose to do much more work in this style. My prediction of the result is an enormous collection of complex, informal rules which interact in unexpected ways, which cannot actually be implemented, and which would yield ridiculously inefficient code if they were implemented. The goals of the authors are good, but it seems to me that they need to find a different approach to them. They need to validate every step of their work, as they go, with implementation and evaluation. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: Are the references correct?: Many words are misspelled. 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 ++++++++++++++++++++++