RE: Discussion on Modelling Effects

Jan,

I've used pre and post conditions in the OO context in a number of
projects, but with the focus on providing run-time checking (either by a
user to check if a method will work on the available data, by the
"object" to check pre and post-conditions and produce an exception if
constraints are violated, or by a user after a result has been returned
to check the validity of the result/method that produced it (sort of an
"executable" exception description mechanism).  For service pre/post
conditions, are these distinctions likely to be valid/useful?

In the context of services, however, one of the most useful aspects
could possibly be to clarify the meaning of operations, by describing
the relationship between the inputs and outputs (particularly complex
ones, allowing for elements of input arrays to be related to elements of
output arrays etc).  Is this "in scope"?

Regards,

Paul  

-----Original Message-----
From: public-sws-ig-request@w3.org [mailto:public-sws-ig-request@w3.org]
On Behalf Of Jan Ortmann
Sent: Friday, 9 June 2006 7:36 AM
To: public-sws-ig@w3.org
Subject: 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 Tuesday, 13 June 2006 01:47:52 UTC