RE: Proposal for CR108

Jonathan,

I think our assertions should be easy for developers to understand, and 
they should be "atomic" in the sense that they should test a single 
condition.

The counter-example to this is the errors you can get from an XSD 
validator. They can sometimes force you to read the XSD spec for days.

The way you phrase the first two is good. I'd phrase the last two as:

-          If the local name is ?infault? then the message exchange 
pattern MUST support at least one fault in the "In" direction
-          If the local name is ?outfault? then the message exchange 
pattern MUST support at least one fault in the "Out" direction

This rewording delegates the condition to the MEP. It allows for other 
fault propagation rules.

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



"Jonathan Marsh" <jonathan@wso2.com> 
Sent by: www-ws-desc-request@w3.org
12/21/2006 05:20 PM

To
Arthur Ryman/Toronto/IBM@IBMCA, "'Roberto Chinnici'" 
<Roberto.Chinnici@Sun.COM>
cc
<www-ws-desc@w3.org>, <www-ws-desc-request@w3.org>
Subject
RE: Proposal for CR108






Per this morning?s call, CR108 is closed, but Arthur?s suggestion will 
become a new issue.
 
AIUI, he is proposing something along the lines of these four new 
assertions, which while they may be (I?m still not sure) strictly 
redundant with the existing assertions, would provide more intelligible 
error messages to users:
 
Add to 2.5.3:
-          If the local name is ?input? then the message exchange pattern 
MUST have at least one placeholder message with direction ?In?.
-          If the local name is ?output? then the message exchange pattern 
MUST have at least one placeholder message with direction ?Out?.
-          If the local name is ?infault? then the message exchange 
pattern MUST either have at least one placeholder message with direction 
?In? and use the Fault Replaces Message propagation rule, or have no 
placeholder message with direction ?Out? and use the Message Triggers 
Fault propagation rule.
-          If the local name is ?outfault? then the message exchange 
pattern MUST either have at least one placeholder message with direction 
?In? and use the Message Triggers Fault propagation rule, or have at least 
one placeholder message with direction ?Out? and use the Fault Replaces 
Message propagation rule.
 
However, I?m not at all sure the last two are 1) correctly stated, 2) 
don?t overconstrain the development of extended MEPs, or 3) any less 
confusing then what we?ve got already.
 
Jonathan Marsh - http://www.wso2.com - 
http://auburnmarshes.spaces.live.com
 

From: www-ws-desc-request@w3.org [mailto:www-ws-desc-request@w3.org] On 
Behalf Of Arthur Ryman
Sent: Wednesday, December 20, 2006 6:39 PM
To: Roberto Chinnici
Cc: www-ws-desc@w3.org; www-ws-desc-request@w3.org
Subject: 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