Proposal for CR108

With respect to CR108, I set out to prove that MessageLabel-0006 
(henceforth ML06 for brevity) and MessageLabel-0014 (ML14) are 
equivalent and discovered that they are not.

So now I'm in agreement with Amy on this point and I have a proposal to 
close CR108. But before doing that, I'd like to establish that ML06 and 
ML14 are not equivalent.

------ PART 1. ML14 => ML06 ------

I'm going to show that ML14 implies ML06 (I use "=>" for logical 
implication).

Let's consider the two assertions:

ML06: The messageLabel attribute information item  of a
binding message reference element information item MUST be present if
the message exchange pattern has more than one placeholder message with
{direction} equal to the message direction.

ML14:  If the messageLabel attribute information item  of a
binding message reference element information item is absent then there
MUST be a unique placeholder message with {direction} equal to the
message direction.

Assume <<the message exchange pattern has more than one placeholder
message with {direction} equal to the message direction>>, i.e. the
antecedent of ML06. (#1#)

Now let's assume that the consequent of ML06 is false, i.e. that <<the
messageLabel attribute information item  of a binding message reference
element information item is absent>> (#2#) and derive a contradiction 
from it, (#1#) and ML14.

Applying modus ponens to (#2#) and ML14, we obtain <<there MUST be a 
unique  placeholder message with {direction} equal to the message 
direction>>. This is inconsistent with (#1#).

Consequently, ML14 => ML06.

------ PART 2. ML06 =/=> ML14 ------

Initially I thought that the two were equivalent, but they aren't.
Here's a counterexample that proves that ML06 does not imply ML14.

Consider a binding operation

<operation ref="tns:foo"> (#3#)
     <input />
     <output />
</operation>

whose corresponding interface operation is

<operation name="foo" pattern="myNs:pattern1">
     <output />
</operation>

such that the nyNs:pattern1 MEP (#4#) has no input messages.

You would expect this to be an error, but if you only assume ML06 but 
not ML14, you can't prove it. Why? Because the antecedent of ML06 says 
"if the message exchange pattern has more than one placeholder message 
with {direction} equal to the message direction" and the MEP (#4#) 
doesn't satisfy it (zero is not "more than one").

ML14 catches this case because the MEP (#4#) does not satisfy its 
consequent: <<there MUST be a unique placeholder message with 
{direction} equal to the message direction>> (there isn't one), thus 
making the component model is invalid. So ML06 =/=> ML14.

------ PART 3. PROPOSAL ------

Given that ML14 => ML06, we propose to remove ML06 from the spec as 
redundant.

We should then close CR108 with no further action, indicating that the 
question it raised ("are ML06 and ML14 equivalent?") can be answered 
negatively by the counterexample in part 2 of this message.

Thanks,
Roberto

Received on Tuesday, 19 December 2006 23:59:04 UTC