Re: Proposal for CR108

+1

Given MEP extensibility, and the possibility of alternative fault propagation strategies, these modifications strike me as 'cleaner' and more comprehensive.  I also agree with Arthur and Jonathan on the language for the other assertions.

Amy!
On Tue, 2 Jan 2007 10:40:57 -0500
Arthur Ryman <ryman@ca.ibm.com> wrote:

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


-- 
Amelia A. Lewis
Senior Architect
TIBCO/Extensibility, Inc.
alewis@tibco.com

Received on Tuesday, 2 January 2007 16:11:02 UTC