From: Matthias S. <Mat...@in...> - 2011-11-28 13:12:46
|
Hi Michael, Here is some feedback on the Rodin handbook. 1) Actually I have already used the email feedback feature. I asked for a confirmation that my feedback has been received, but I never got a confirmation. Apparently, there is a problem with the email feedback. 2) Proving / Provers: I find the following statement inappropriate: "New PP is unsound. There have been several bug reports. Some have been fixed, but at this point we do not recommend New PP for inexperienced users." For two reasons: - Experience does not help to cope with NewPP's unsoundness. I would simply not use it for production. For education and alike, it makes sense to use it. (It is difficult anyway to enforce the policy "don't use NewPP" in a class of students.) - ML has been unsound as well. 3) On Mathematical Notation / Sets: I have some feedback on how you introduce the various operators. I focus on the example of subset (\subseteq), but it applies to other definitions as well. Here is the "definition": S \subseteq T \triangleq \forall e\qdot e \in S \limp e \in T There is some room for interpretation what this actually means; here is what I understood: - It is not entirely clear whether S and T range over only well-defined or also over ill-defined values. I assume the latter. For, otherwise the statement L(S \box T) \triangleq L(S) \land L(T) would be pointless. - Then it is not entirely clear what the \triangleq means. A logic of partial functions has many notions of equality. I assume that A \triangleq B means that A is true/false/ill-defined iff B is true/false/ill-defined, respectively. This emphasizes that the left- and right-hand side of a definition are interchangeable. With this in mind, I spotted some problems: - Did you introduce "\in"? I could not find it. I admit, it is not possible to define "\in". But maybe you should say at some point what you take as granted and what you define on your own. That prevents readers from searching for definitions that do not exist. - The left- and right-hand side are actually not interchangeable. For, if S is the empty set and T ill-defined, then the lhs is ill-defined and the rhs is true. One may go one step further: the two equalities S \subseteq T \triangleq \forall e\qdot e \in S \limp e \in T and L(S \box T) \triangleq L(S) \land L(T) imply L(\forall e\qdot e \in S \limp e \in T) \triangleq L(S) \land L(T), which is certainly not the case. - Actually you have two kinds of variables and two kinds of equalities in the handbook. This makes it difficult to infer what is actually meant. I would make the difference between the two kinds of variables syntactically visible, and explain the semantical difference between the two kinds of variables/equalities up front. I believe that almost every reader of the handbook has already seen the subset relation and will find the equation S \subseteq T \triangleq \forall e\qdot e \in S \limp e \in T rather obvious. So he will not learn anything from reading this definition. Instead of emphasizing what the reader already knows, the handbook should point out how Event-B's operators deviate from the reader's intuition. 4) Some miscellaneous comments: In Section 3.3 you refer to the Z reference manual. There was never an agreement how partial functions are handled in Z. I would therefore not try to understand Event-B from the Z reference manual. In Section 3.3.2 you say that \land and \lor are "principally commutative". It is not clear to me what that should mean. On some internal level, \land and \lor are indeed commutative, but this is hardly evident to the user. I would therefore simply say that \land and \lor are not commutative. Best regards, Matthias |
From: Daniel P. <pl...@cs...> - 2011-11-28 14:40:39
|
Hello Matthias, On 28.11.2011 14:12, Matthias Schmalz wrote: > Hi Michael, > > Here is some feedback on the Rodin handbook. > > 1) Actually I have already used the email feedback feature. I asked for > a confirmation that my feedback has been received, but I never got a > confirmation. Apparently, there is a problem with the email feedback. we have received several feedback messages from you. The feedback is collected in a spreadsheet first and not all messages are attended to yet. I'm sorry if you might had the impression that we do not read the feedback. First, thank you for your feedback. This is exactly the kind of feedback I hoped for because I'm a little bit unsure regarding some topics of the reference section. I still have some questions about what you said about section 3: > 2) Proving / Provers: [...] > 3) On Mathematical Notation / Sets: > > I have some feedback on how you introduce the various operators. > I focus on the example of subset (\subseteq), but it applies to other > definitions as well. Here is the "definition": > > S \subseteq T \triangleq \forall e\qdot e \in S \limp e \in T > > There is some room for interpretation what this actually means; here is > what I understood: > - It is not entirely clear whether S and T range over only well-defined > or also over ill-defined values. I assume the latter. For, otherwise the > statement L(S \box T) \triangleq L(S) \land L(T) would be pointless. My intention was this: Under the assumption that the predicate is well-defined (as defined by the statement "L(S \ T) <: L(S) & L(T)"), "S <: T" is logically equivalent to "!e. e:S => e:T". I think in this context "L(S<:T) == L(S) & L(T)" is not pointless, because it just defines under which conditions the equivalence holds. > - Then it is not entirely clear what the \triangleq means. A logic of > partial functions has many notions of equality. I assume that A > \triangleq B means that A is true/false/ill-defined iff B is > true/false/ill-defined, respectively. This emphasizes that the left- and > right-hand side of a definition are interchangeable. I agree with you here. There is currently no definition of the operator in the handbook yet. My understanding is that A \triangleeq B means A is true/false iff B is true/false. As said above, the ill-defined case is ruled-out by the WD-condition. > With this in mind, I spotted some problems: > > - Did you introduce "\in"? I could not find it. I admit, it is not > possible to define "\in". But maybe you should say at some point what > you take as granted and what you define on your own. That prevents > readers from searching for definitions that do not exist. Yes, \in is defined in 3.3.2. Somewhat arbitrary, maybe it fits better into the sets section. > - The left- and right-hand side are actually not interchangeable. For, > if S is the empty set and T ill-defined, then the lhs is ill-defined and > the rhs is true. > One may go one step further: the two equalities > S \subseteq T \triangleq \forall e\qdot e \in S \limp e \in T > and > L(S \box T) \triangleq L(S) \land L(T) > imply > L(\forall e\qdot e \in S \limp e \in T) \triangleq L(S) \land L(T), > which is certainly not the case. But is this still the case if we assume S and T as well-defined? Or am I too naive here? > - Actually you have two kinds of variables and two kinds of equalities > in the handbook. This makes it difficult to infer what is actually > meant. I would make the difference between the two kinds of variables > syntactically visible, and explain the semantical difference between the > two kinds of variables/equalities up front. With two kinds of variables you mean a) a variable as a placeholder for an arbitrary expression and b) an Event-B identifier? I'm not sure what you do mean by the second equality? Do you mean statements like: "S \/ T = { x | x:S or x:T }"? In that case, does that really leads to any confusion? > I believe that almost every reader of the handbook has already seen the > subset relation and will find the equation > S \subseteq T \triangleq \forall e\qdot e \in S \limp e \in T > rather obvious. So he will not learn anything from reading this > definition. Instead of emphasizing what the reader already knows, the > handbook should point out how Event-B's operators deviate from the > reader's intuition. I do not agree fully here. For most (if not all) it is obvious. But where do we draw the line? Using prose everywhere just to avoid a formal notion would make the reference much more clumsy to read. > 4) Some miscellaneous comments: > > In Section 3.3 you refer to the Z reference manual. There was never an > agreement how partial functions are handled in Z. I would therefore not > try to understand Event-B from the Z reference manual. I agree. But the note is a reference for handbook writers as an example for a handbook for a mathematical notion, not for Z's foundations. The note will be removed before the final release. > In Section 3.3.2 you say that \land and \lor are "principally > commutative". It is not clear to me what that should mean. On some > internal level, \land and \lor are indeed commutative, but this is > hardly evident to the user. I would therefore simply say that \land and > \lor are not commutative. I agree. Again, thank you very much, Matthias. I'll work on the reference section and on incorporating the feedback this week. So most probably I will come back to you with several questions. :) Best regards Daniel |