Re: Proposal for CR108

Roberto,

Thx for the analysis. 

Amy rightly pointed our that the same situation occurs with 
MessageLabel-0004 and MessageLabel-0012.

I was assuming that these assertions applied to the case where there was 
at least one message placeholder with a given direction and that they were 
defining when the messageLabel was required. Here is my analysis

Let P = The messageLabel AII is Present.
Let Q = The MEP has a unique placeholder message with direction equal to 
the message direction.

ML06 = If not(Q) then P.
ML14 = If not(P) then Q.

Both of these propositions are equivalent to the symmetrical statement (P 
or Q), which translates to:

The messageLabel AII MUST be present OR the MEP MUST have a unique message 
placeholder with direction equal to the message direction.

However, we have not in fact ensured that there is at least one 
placeholder message in the given direction, that my translation is wrong 
since in that case

not(Q) = The MEP has either zero OR more than one placeholder message in 
the given direction.

I propose the following resolution:

In 2.5.3 Mapping Interface Message Reference's XML Representation to 
Component Properties add the following assertion:

If the local name is input then the MEP MUST have at least one placeholder 
message with direction = in.
If the local name is output the the MEP MUST have at least one placeholder 
message with direction = out.

I agree that we can drop MessageLabel-0004 and keep MessageLabel-0012.

Similarly, fix up

2.10.3 Mapping Binding Message Reference's XML Representation to Component 
Properties

the same way.

We probably have to fix up the Interface Fault Reference and Binding Fault 
Reference the same way.

Arthur Ryman,
IBM Software Group, Rational Division

blog: http://ryman.eclipsedevelopersjournal.com/
phone: +1-905-413-3077, TL 969-3077
assistant: +1-905-413-2411, TL 969-2411
fax: +1-905-413-4920, TL 969-4920
mobile: +1-416-939-5063, text: 4169395063@fido.ca



Roberto Chinnici <Roberto.Chinnici@Sun.COM> 
Sent by: www-ws-desc-request@w3.org
12/19/2006 06:20 PM

To
www-ws-desc@w3.org
cc

Subject
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