RE: Preconditions /effects vs Preconditions/Postconditions

IMHO, the distinction between the post-condition and effect is not a
clear-cut distinctionme definitions that I found for "post-condition" over the web:

i. The post condition is a statement of what the world should look like
after an operation. For instance if we define the operation square on a
number the post-condition would be of the form result = this * this (where
result is the output and this is the object on which the operation was
invoked). The post condition is a useful way of saying what we do, without
saying how we do it, separating interface from implementation.
ii. Post Condition: State of the system after executing the operation.
iii. A post-condition specifies some facts about the world which can be
expected to be valid after the service operation has finished its execution
regularly.

As for the defined example I'd say that the distinction could become clearer
if:

Post-condition: credit card billed/not billed
Effect: transaction successful/failed

Charlie

-------------------------------------------------
Charlie Abela
Research Student,
Dept. of Computer Science and AI
University of Malta,
MSD06. Malta
Web: http://www.semantech.org
Email: abcharl@keyworld.net

-----Original Message-----



All email is scanned by Keyworld against known Viruses. This service is offered to all Keyworld subscribers and hosted domains and does not carry any warranty. You are advised to protect your PC with updated antivirus software at all times.

Forwarded message 1

  • From: www-ws-request@w3.org <www-ws-request@w3.org> 
Yinsheng
Sent: Monday, September 15, 2003 6:17 PM

Forwarded message 2

  • Subject: RE: Preconditions /effects vs Preconditions/Postconditions
  • To: 'Michael Kifer'
  • Cc: 'www-ws@w3.org' 
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 13:02:50 UTC