Re: Preconditions /effects vs Preconditions/Postconditions

Walden, Charlie, all,

The terms "postcondition" and "effect" are not used consistently
within the computer science literature.  (Neither is the term
"condition", for that matter, which appears to be conflated with
"well-formed formula" in some of the email exchangtes.)

While the distinction you make below may be a reasonable one, I don't
think it reflects the use of *DAML-S* "effects" and *WS Choreography*
"postconditions".  The DAML-S Coalition will (I hope) discuss
this offline on Wednsday and come up with a response to Monika Solaki's
original question, which was to distinguish between these two uses of the
terms.

Regards,
Sheila McIlraith

On Mon, 15 Sep 2003, Walden Mathews wrote:

>
> How about this:
>
> The post-condition of a (successful) credit card transaction
> is that your loan balance is increased and your available credit
> is decreased, both by the transaction amount.
>
> (An invariant on the account state is that current balance
> plus available credit always = credit limit, but that's a little
> outside the scope here.)
>
> The effect of a (successful) credit card transaction is the
> existence of a new transaction identifier, which is handed to
> you as an outcome of the operation.
>
> Failure states are not part of the post-condition or effect
> landscape.  In other words pre- and post-states are part of
> the model of successful operation.
>
> How does that fly?
>
> Walden Mathews
>
>
> ----- Original Message -----
> From: "Charlie Abela" <abcharl@keyworld.net>
> To: "Li, Yinsheng" <Yinsheng.Li@nrc-cnrc.gc.ca>
> Cc: <www-ws@w3.org>
> Sent: Monday, September 15, 2003 1:04 PM
> Subject: 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.
> >
>
>
>

==============================================================================

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

Received on Monday, 15 September 2003 15:03:34 UTC