Re: Preconditions /effects vs Preconditions/Postconditions

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

Received on Monday, 15 September 2003 14:42:42 UTC