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