Re: [wsbpel] Need for Formalism

[Ron Ten-Hove <Ronald.Ten-Hove@Sun.COM>]

An excellent idea. Formalism will make our task as a committee easier. 
Trying to instill rigor, and remove ambiguity, from standard English 
results in virtually impenetrable prose. Formalism will allow us to be 
clearer, more easily reason about what we have described, and spend a 
lot less time debating the exact meaning of inexact English terms.

-Ron

Sid Askary wrote:

> I would like to pose the need for a ”formalism” to the group.  I think 
> we need it.  Here are some of my thoughts.  Let me know what you think.
>
> When developing a programming language (be it declarative, as in the 
> case of BPEL), there is generally a computation model (reasoned 
> mathematically – as is the case with process calculi) followed by 
> syntax and semantics.
>
> The syntax will usually be accompanied by one or more of the three 
> commonly known complementary formal approaches:
>
> 1)  Denotational semantics: -  Used mainly for requirements, 
> specification correctness, etc.
> -  Concerned with effects - observable behavior (and property) after 
> execution.
>
> 2)  Algebriac Semantics:
> -  Used mainly to reason about the language specification.
> -  Concerned with partial correctness – formulas for pre and post 
> condition states.
>
> 3)  Operational Semantics:
> -  Used mainly for guidelines on implementation.
> -  Concerned with how to execute a program using atomic steps and 
> transition rules.
>
> The above methods are neither always present in a language 
> presentation, nor are they complete.  For instance, “Total 
> correctness” proofs such as deadlocks, abnormal termination, etc. are 
> often ignored.  Nevertheless, they help to reinforce the soundness of 
> the proofs (or claims) by multiple means.
>
> The issue of formalism becomes even more critical when a language is 
> being debated in the context of a standard organization.  And in the 
> case of BPEL specification, although there is a notion of “operational 
> semantics” (albeit not formalized), there are also “distributed”, 
> “concurrent” and “asynchronous” properties that are not formalized – 
> (“intent” and “goals” notwithstanding, as I look forward to reading 
> that upcoming document from the original authors).  Since the BPEL 
> specification is a combination of XLANG and WSPL, what is the combined 
> computational model?
>
> To relegate this question to practical domain is not sufficient.  It 
> is often the case that in practice, such problems are tackled 
> empirically in execution environment where common programming 
> languages (and/or platforms) can simultaneously mask some deficiencies 
> AND highlight others in the specification.  Furthermore, while they 
> may focus on common to perform process/workflow patterns, the 
> implementations do not reflect the causal relationship for 
> stratification of specification as it pertains to certain aspects 
> (i.e. reliance on certain protocols, security, choice of methodology 
> for extraction of expressions, etc.).
>
> Therefore, two additional semantics plus a computational model is 
> needed in order to fully reason about the specification and discuss 
> provability, completeness, liveliness and other relevant properties.  
> I imagine that the original authors have some or all of these 
> constructs and I only ask that they be shared with the group.
>
> Regards,
> Sid Askary
>
>
>
>
> ---------------------------------------------------------------------
> To unsubscribe, e-mail: wsbpel-unsubscribe@lists.oasis-open.org
> For additional commands, e-mail: wsbpel-help@lists.oasis-open.org
>