Discussion on Modelling Effects

Dear all, 

I would like to start a discussion about what kind of information pre-
and postconditions need to provide. 

Since the approach followed by OWL-S and WSMO is to use an axiomatic
semantics we should provide a set of Hoare-triples {P}p{Q} for each
process. Preconditions "declare" the variables and provide conditions to
call the process. But what are the effects? Here, I suppose, we should
model all things that a process changes. For a process, where I buy
something, this usually includes the balance of my account as well as
the fact, that something will be delivered. Thus we need be able to
express, that things change, although we did not pass them in as a
parameter (my account), and we need a concept of time (since things will
be delivered in the future). 

I would think that we might have a precondition 

{Creditcard(X) /\ X.account.balance>200 /\ Book(Y) /\ Buyer(Z)}

where the value of functional roles (attributes) was written as in OO
languages by a dot. An effect might look like

{[X.account.balance]after = [X.account.balance]before - 200 /\
[Y.owner]after=Z}

Here I indicated the states by "[*]after" and "[*]before". 

Are there any publications on these issues or any further suggestions?

Regards, 

Jan Ortmann

Received on Thursday, 8 June 2006 21:38:39 UTC