On 28.11.2011 14:12, Matthias Schmalz wrote:

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.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.

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.

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.- 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.

Yes, \in is defined in 3.3.2. Somewhat arbitrary, maybe it fits better into the sets section.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.

But is this still the case if we assume S and T as well-defined? Or am I too naive here?- 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.

With two kinds of variables you mean- 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.

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 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.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 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.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.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.

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