Re: Preconditions /effects vs Preconditions/Postconditions

>>>>> "JL" == Message from Jeff Lansing <<jeff@polexis.com> > writes:

    JL> 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.
    >> 
    >> 
    >> 
    JL> If post-conditions are conditions, then there are 2 post-conditions 
    JL> here, which could be stated as:

    JL> 1) the increase in the loan balance is equal to the transaction amount
    JL> 2) the decrease in the available credit is equal to the transaction amount.

    JL> (and which could be conjoined into a single post-condition, if you prefer).

    JL> There are also two effects:

    JL> a) the loan balance has been increased (by the transaction amount, as it 
    JL> happens)
    JL> b) the available credit has been decreased (also by the transaction 
    JL> amount, as it happens).


The two things that you have specified are neither postconditions nor
preconditions.

A precondition is a constraint on the state of the database that exists
before the execution of an action.
A postcondition is a constraint on the state that exists right after the
execution of an action.
(And, again, the effect is the actual change that the action does to the
database state. By the way, by "state" I mean the logical theory that
describes the situation. It can include not only facts but other formulas
as well. But in most practical cases people probably view the database as a
bunch of facts.)

The conditions that you have given above are sometimes called "dynamic
constraints on action execution", but I don't think there is an agreed
upon term for this, such as  postcondition/precondition mentioned above.

The above two constraints are constraints on the change performed by an
action -- it involves both the state before the execution and the state after.
Such constraints are pretty common (e.g., no transaction can increase
salary by more than 5%), but they are neither pre nor post conditions.

Note that if you know what an action does then it might be possible to
check such dynamic constraints before executing the action. This, however,
doesn't make this constraint into a precondition. You are still reasoning
about both states: the before- and after-states. In this case,
you are just able to perform the reasoning without actually executing the
action.

Hope these explanations help.


	--michael

Received on Monday, 15 September 2003 20:03:09 UTC