RE: Preconditions /effects vs Preconditions/Postconditions

Hi Michael,

Could the example below consist with your statements? If so, we may have a
better understanding.

For a payment transaction,
Precondition: Credit card is fine
Input: Account and amount
Output: Approved/Rejected 
Postcondition: Client doesn't regret  
Effect: Transaction successful/Failed 

Regards,
Yinsheng Li


> -----Original Message-----
> From: Michael Kifer [mailto:kifer@cs.stonybrook.edu]
> Sent: Monday, September 15, 2003 10:44 AM
> To: David Martin
> Cc: Monika Solanki; www-ws@w3.org
> Subject: Re: Preconditions /effects vs Preconditions/Postconditions 
> 
> 
> 
> 
> There is a clear distinction between effects and postconditions.
> An effect is what the action *does*.
> A postcondition is a constraint that says what must hold 
> after the action
> executed or else the action should be aborted and its effects 
> undone. This
> constraint represented by the postcondition can be partial.
> 
> The difference is especially obvious when the theory has rules.
> For instance, suppose the current state has a rule and a 
> bunch of facts as
> shown below:
> 
> p(X) :- r(X,Y), q(Y).
> r(a,b).
> r(c,d).
> q(d).
> 
> A postcondition can be 
> 
> not p(c).
> 
> If the action produces the effect of insertion q(b) then the 
> constraint
> (postcondition) is satisfied and everything is fine.
> If the action inserts q(d) then, in the resulting state, p(c) becomes
> true and the postcondition becomes false. Therefore, the action
> should not be allowed to succeed.
> 
> 
> 	regards
> 	  --michael  
> 
> > 
> > Hi Monika -
> > 
> > I believe you have been saying that a "postcondition" in 
> DAML-S (if that 
> > term were used) would be the same as the condition of a conditional 
> > effect.  I guess, since we don't normally talk about 
> "postconditions" in 
> > DAMl-S documentation, there's no precise answer.  But I 
> tend to think of 
> > it differently than (I think) you've been saying.  more below ...
> > 
> > Monika Solanki wrote:
> > 
> > 
> > > Short reply for now.
> > > 
> > > I guess, we all are talking about the same thing. The 
> difference is 
> > > maybe only in the way we put it across. Post condition is 
> indeed the 
> > > condition which is true after service execution. However, in the 
> > > terminology that we use in DAML-S, an "Effect" may be  
> produced  under 
> > > certian condition and this condition is true only after service 
> > > execution, 
> > 
> > 
> > If you are talking about conditions of conditional effects, 
> it  doesn't 
> > seem quite accurate to say they are true only after service 
> execution. 
> > At least for some such conditions  they may also be true 
> before service 
> > execution.  For example, "book in stock" might certainly be 
> true (or 
> > false) both before service execution and after.
> > 
> > therefore this condition is the "Post condition".
> > 
> > Actually, I tend to think of "postcondition" and "effect" 
> as synonymous. 
> >    So then, in my mind at least, a postcondition would not 
> be the same 
> > as the condition part of a conditional effect; rather it 
> would be the 
> > same as the effect part.
> > 
> > I can't say for sure whether others in the DAML-S Coalition 
> hold the 
> > same view on this as me, but I think most probably do.
> > 
> > Regards,
> > -- David
> > 
> > Quoting
> > > from WSMF document:
> > > 
> > > The pre-condition is the condition that has to be true
> > > for the input in order for the web service to be able to 
> successfully 
> > > execute it. The postcondition
> > > is the condition that holds once the complex service has 
> been executed
> > > successfully, i.e., it defines constraints on its output.
> > > 
> > > 
> > > Sheshagiri, Mithun wrote:
> > > 
> > >>  
> > >>
> > >>     -----Original Message-----
> > >>     *From:* Monika Solanki [mailto:monika@dmu.ac.uk]
> > >>     *Sent:* Friday, September 12, 2003 6:18 PM
> > >>     *To:* Sheshagiri, Mithun
> > >>     *Cc:* 'Sheila McIlraith'; www-ws@w3.org
> > >>     *Subject:* Re: Preconditions /effects vs 
> Preconditions/Postconditions
> > >>
> > >>
> > >>
> > >>     Sheshagiri, Mithun wrote:
> > >>
> > >>>I might be be wrong but I think Monika and Sheila are 
> talking about two
> > >>>different conditions.
> > >>>
> > >>>Monika is talking about Effect of execution being a 
> condition and this she
> > >>>terms as postcondition. 
> > >>>
> > >>     :-) .. Incidentally, by "Postcondition" , I mean 
> precisely, the
> > >>     conditions under which the "effect" is produced and 
> which is alos
> > >>     a subclass of ceCondition (which is also what Sheila 
> is referring
> > >>     to), and not "the effect of execution being a condition".
> > >>     [Sheshagiri, Mithun] 
> > >>      
> > >>     I was under the impression that postcondition would be
> > >>     something that holds after the service is executed.
> > >>
> > >>     AtomicProces: BuyBook
> > >>     input: bookName
> > >>     precondition: validUser
> > >>     effect: points to disjointUnionOf(BookShippedEffect,
> > >>     BookWillBeShippedEffect)
> > >>     (BookShippedEffect, BookWillBeShippedEffect ) subClassOf
> > >>     ConditionalEffect
> > >>     BookShippedEffect
> > >>              +------ceEffect BookShipped 
> > >>              +------ceCondition BookImmAvail 
> > >>     BookWillBeShippedEffect
> > >>              +-------ceEffect BookWillBeShipped
> > >>              +-------ceCondition ¬BookImmAvail
> > >>      
> > >>     BookImmAvail determines the effect so is it correct 
> to call it
> > >>     a postcondition?
> > >>
> > >>     On the other hand,
> > >>     The effect of executing an AtomicProcess might be 
> the assertion of
> > >>     a condition. I thought this would be a postcondition
> > >>      
> > >>     AtomicProcess: ValidateCC
> > >>     input: CCname, CCnum, CCexpiry
> > >>     effect: points disjointUnionOf(ValidEffect, InValidEffect)
> > >>     (ValidEffect, InValidEffect) subClassOf ConditionalEffect
> > >>     ValidEffect
> > >>              +------ceEffect Valid
> > >>              +------ceCondition CreditApproved
> > >>     InValidEffect
> > >>              +-------ceEffect InValid
> > >>              +-------ceCondition ¬CreditApproved
> > >>     ValidP /sameValues/ Valid 
> > >>      
> > >>     Now  Valid and ValidP could be subClassOf 
> process.owl#Condition
> > >>     and Valid is this case, IMHO,  is a postcondition. And since
> > >>     ceEffect can point to owl:Thing, this is permitted.
> > >>      
> > >>     phew! I need a program that generates names for my 
> classes and
> > >>     properties.
> > >>      
> > >>
> > >>     --Monika
> > >>
> > >>>(ceEffect points to a concept which is a subclassof
> > >>>process:#Condition. And Sheila is talking about the 
> condition being pointed
> > >>>by ceCondition which decides the effect.
> > >>>
> > >>>mithun 
> > >>>
> > >>>  
> > >>>
> > >>>>-----Original Message-----
> > >>>>From: Sheila McIlraith [mailto:sam@ksl.Stanford.EDU] 
> > >>>>Sent: Thursday, September 11, 2003 5:45 PM
> > >>>>To: Monika Solanki
> > >>>>Cc: www-ws@w3.org
> > >>>>Subject: Re: Preconditions /effects vs 
> Preconditions/Postconditions
> > >>>>
> > >>>>
> >>>>
> > >>>>
> > >>>>
> > >>>>Monika,
> > >>>>
> > >>>>In DAML-S we are able to express conditional effects.  These 
> > >>>>are the side effects of a web service, as contrasted with its 
> > >>>>output. E.g.,  AcmeBookSeller Web Service:
> > >>>>  *output* is purchase receipt
> > >>>>  *conditionalEffect* is comprised of a *condition* and 
> an *effect*
> > >>>>    the *effect* is that the book is sent to the customer,
> > >>>>    under the *condition* that the book is in stock.
> > >>>>
> > >>>>Side effects of services are critical to encode for the 
> > >>>>purposes of automated WS composition, where such effects must 
> > >>>>be considered in composing and executing services.  
> > >>>>(Something we humans do all the time.)
> > >>>>
> > >>>>As to how this relates to the wschor document you were 
> > >>>>reading, it would be helpful to have the citation, but 
> > >>>>without seeing it, here is a general answer.  In the AI 
> > >>>>planning literature the term "effect" is often used 
> > >>>>synonymously with the term "postcondition".  It is used 
> > >>>>generically to captures the notion of effects which are 
> > >>>>either conditional (i.e., conditional effects) or unconditional.
> > >>>>
> > >>>>I'm guessing that ws-chor's notion of "postcondition" is used 
> > >>>>in this context.  It is possible that they have done away 
> > >>>>with the notion of condition in their "postcondition", 
> > >>>>because this is simpler, but I would argue, is not 
> > >>>>sufficiently expressive to capture the true side effects of 
> > >>>>web services.
> > >>>>
> > >>>>As for what we need for WS composition, we need both the 
> > >>>>*effect* and the *condition*, but the *effect* is the 
> key notion.
> > >>>>
> > >>>>Regards,
> > >>>>Sheila McIlraith
> > >>>>
> > >>>>
> > >>>>On Thu, 11 Sep 2003, Monika Solanki wrote:
> > >>>>
> > >>>>    
> > >>>>
> > >>>>>In DAML-S we have Preconditions and Effects(Conditions 
> and Effect).
> > >>>>>
> > >>>>>BPEL4WS does not have the notion of Preconditions and 
> > >>>>>      
> > >>>>>
> > >>>>Postconditions( 
> > >>>>    
> > >>>>
> > >>>>>to the best of my knowledge). However the ws-chor group  
> > >>>>>      
> > >>>>>
> > >>>>have defined 
> > >>>>    
> > >>>>
> > >>>>>Precondition and Postcondition for the use cases in their 
> > >>>>>      
> > >>>>>
> > >>>>requirement 
> > >>>>    
> > >>>>
> > >>>>>document.
> > >>>>>
> > >>>>>I am wondering if the semantics of the "Conditions" for 
> > >>>>>      
> > >>>>>
> > >>>>"Effects" as 
> > >>>>    
> > >>>>
> > >>>>>defined in DAML-S are different from "Post conditions" in 
> > >>>>>      
> > >>>>>
> > >>>>ws-chor doc, 
> > >>>>    
> > >>>>
> > >>>>>as  what we are really interested in is the condition 
> itself.  What 
> > >>>>>would be lost (just for the sake of argument) if we 
> were to discard 
> > >>>>>the notion of "effect" and retain only the condition part 
> > >>>>>      
> > >>>>>
> > >>>>of "Effect" 
> > >>>>    
> > >>>>
> > >>>>>i.e if I may call it,  "Post condition". I say this 
> because I feel 
> > >>>>>that in some way the effect part gets reflected in the 
> > >>>>>      
> > >>>>>
> > >>>>output. Maybe 
> > >>>>    
> > >>>>
> > >>>>>"Effect" makes it more explicit. I guess even for service 
> > >>>>>      
> > >>>>>
> > >>>>composition, 
> > >>>>    
> > >>>>
> > >>>>>what we are really interested in apart from input 
> -output is the 
> > >>>>>conditions that are captured in Preconditions and 
> Effects. I guess 
> > >>>>>what I am really trying to say is can we simplfy the notion of 
> > >>>>>Conditional effects by attributing it as "post 
> condition" without 
> > >>>>>compromising anything that is not covered in any other 
> property 
> > >>>>>parameter.
> > >>>>>
> > >>>>>Any comments / thoughts well appreciated
> > >>>>>
> > >>>>>Thanks,
> > >>>>>
> > >>>>>Monika
> > >>>>>
> > >>>>>--
> > >>>>>**>><<**>><<**>><<**>><<**>><<**>><<**>><<**
> > >>>>>Monika Solanki
> > >>>>>Software Technology Research Laboratory(STRL)
> > >>>>>De Montfort University
> > >>>>>Hawthorn building, H00.18
> > >>>>>The Gateway
> > >>>>>Leicester LE1 9BH, UK
> > >>>>>
> > >>>>>phone: +44 (0)116 250 6170 intern: 6170
> > >>>>>email: monika@dmu.ac.uk
> > >>>>>web: http://www.cse.dmu.ac.uk/~monika
> > >>>>>**>><<**>><<**>><<**>><<**>><<**>><<**>><<**
> > >>>>>
> > >>>>>
> > >>>>>      
> > >>>>>
> > >>>>==============================================================
> > >>>>================
> > >>>>
> > >>>>*** Moving to Dept. Computer Science, University of Toronto ***
> > >>>>
> > >>>>Sheila McIlraith, PhD                 Phone: 650-723-7932
> > >>>>Senior Research Scientist             Fax:  650-725-5850
> > >>>>Knowledge Systems Lab
> > >>>>Department of Computer Science
> > >>>>Gates Sciences Building, 2A-248       
> > >>>>http://www.ksl.stanford.edu/people/sam
> > >>>>Stanford University    
> > >>>>               E-mail: sam-at-ksl-dot-stanford-dot-edu
> > >>>>Stanford, CA 94305-9020
> > >>>>
> > >>>>
> > >>>>
> > >>>>
> > >>>>
> > >>>>    
> > >>>>
> > >>>
> > >>>  
> > >>>
> > >>
> > >>     -- 
> > >>     **>><<**>><<**>><<**>><<**>><<**>><<**>><<**
> > >>     Monika Solanki
> > >>     Software Technology Research Laboratory(STRL)
> > >>     De Montfort University
> > >>     Hawthorn building, H00.18
> > >>     The Gateway
> > >>     Leicester LE1 9BH, UK
> > >>
> > >>     phone: +44 (0)116 250 6170 intern: 6170
> > >>     email: monika@dmu.ac.uk
> > >>     web: http://www.cse.dmu.ac.uk/~monika
> > >>     **>><<**>><<**>><<**>><<**>><<**>><<**>><<**
> > >>
> > > 
> > > -- 
> > > **>><<**>><<**>><<**>><<**>><<**>><<**>><<**
> > > Monika Solanki
> > > Software Technology Research Laboratory(STRL)
> > > De Montfort University
> > > Hawthorn building, H00.18
> > > The Gateway
> > > Leicester LE1 9BH, UK
> > > 
> > > phone: +44 (0)116 250 6170 intern: 6170
> > > email: monika@dmu.ac.uk
> > > web: http://www.cse.dmu.ac.uk/~monika
> > > **>><<**>><<**>><<**>><<**>><<**>><<**>><<**
> > > 
> > 
> > 
> > 
> 
>

Received on Monday, 15 September 2003 12:16:52 UTC