Seyed H Haeri

Sibylle Schupp
email: schupp@tu-harburg.de

Reusable Components for Lightweight Mechanisation of Programming Languages

Implementing Programming Languages (PLs) has always been a challenge for various reasons. One reason is the excess of routine tasks to be redone on every implementation cycle. This is despite the remarkable fraction of syntax and semantics usually shared between successive cycles. In this paper, we present a component-based approach to avoid reimplementation of shared PL fractions. We provide two sets of reusable components; one for syntax implementation and another for semantics. Our syntax and semantics components correspond to syntactic categories and semantics rules of a PL specification, respectively. We show how, in addition to their service to reusability in syntax and semantics, our components can cater reusable implementation of PL analyses. Our current level of experimentation suggests that this approach is applicable wherever the following two features are available or can be simulated: Type Constraints and Multiple Inheritance. Implementing a PL using our approach, however, requires some modest programming discipline that we will explain throughout the text.

Introduction

Mechanisation of a PL is implementing it for the purpose of experimentally studying its characteristics and conduct. One interacts with the mechanisation to discover otherwise inapparent facts or flaws in action. PL mechanisation, however, can become very involved using traditional formal proof systems. Various other frameworks have, therefore, been crafted to help lightweight mechanisation. Different frameworks focus on facilitating different mechanisation tasks.

Mechanisation often enjoys cycles. Repeating implementation upon each cycle can form a considerable burden against mechanisation, especially because consecutive cycles often share a sizeable fraction of their syntax, only differ in few semantic rules, and, rarely add new analyses. Modularity becomes vital in that, upon extension, existing modules ought to be readily reusable.

As such, component-based mechanisation can provide even more reusability by facilitating implementation sharing for individual PL constructs. For example, it is not uncommon for different PLs to be extended using similar constructs (in the syntax or semantics). Component-based mechanisation cancels the need for reimplementing such constructs. In addition, our above interpretation of modularity comes as a side product in that PL modules already composed of components need not to be touched upon the addition of new components.

In this paper, we implement language-independent components for syntactic categories to obtain syntax code reuse. We also offer a collection of semanticslenient derivation rules that are individually executable. These form our highly flexible components that cater various sorts of semantics code reuse upon composition. A particularly interesting consequence of the flexibility in our syntax and semantics components is analysis code reuse. These components elevate the programming level of mechanisation; they encourage coding in terms of themselves (as opposed to exact type constructors), viz. , addition of new type constructors imposes no recompilation on existing code. (C.f. Expression Problem [START_REF] Wadler | The Expression Problem, Java Genericity Mailing List[END_REF].)

Whilst our use of multiple inheritance caters easy extension of mechanisation, type constraints help the compiler outlaw reuse of mechanisation when conceptually inapplicable. Our approach is applicable independent of the formalism used for specification. Yet, a modest programming discipline is required for enjoying our reusability. Most of the burden is, however, on the Language Definitional Framework (LDF). Our approach indeed minimises the PL implementer's effort when an extensive set of our components is available through the LDF.

We choose to embed our approach in Scala for its unique combination of built-in features that suit mechanisation [START_REF] Odersky | Scalable Component Abstractions[END_REF]. Both multiple inheritance and type constraints have special flavours in Scala that are not shared universally amongst languages. However, we do not make use of those specialities. Hence, the applicability of our approach is deemed to only be subject to the availability of multiple inheritance and type constraints.

We start by reviewing the related literature in Section 2. In Section 3, we provide a minimal explanation of the Scala features we use. We exemplify our approach using five systems for lazy evaluation that we briefly present in Section 4. Next, in Section 5, we demonstrate our components for both syntax and semantics mechanisation. As an interesting extra consequence of our particular design of components, Section 6 shows how analysis mechanisation reuse is gained. Concluding remarks and discussion on future work come in Section 7. 1

Related Work

Funcons of PLanCompS [START_REF] Johnstone | An Agile Approach to Language Modelling and Development[END_REF] are composable components for PL mechanisation each of which with a universally unique semantics. Funcons are similar to our syntax components except that, due to our decoupling of syntax and semantics, our components can have multiple pieces of semantics. On the other hand, a funcon's semantics is provided using Modular SOS [START_REF]Modular Structural Operational Semantics[END_REF] and Action Semantics [START_REF] Mosses | Theory and Practice of Action Semantics[END_REF], whilst we do not demand any particular formalism. The GLoo mini parsers enable scope-controlled extensions to its language by desugaring the extended syntax into core GLoo [START_REF] Lumpe | Growing a Language: The GLoo Perspective, Soft. Composition[END_REF]. SugarHaskell [START_REF] Erdweg | Layout-sensitive Language Extensibility with SugarHaskell[END_REF] provides similar facilities, but in a layout-sensitive fashion and for Haskell. Polyglot [START_REF] Nystrom | Polyglot: An Extensible Compiler Framework for Java[END_REF] users can extend a PL compiler (including that of Polyglot itself) by providing (one or more) compiler passes that rewrite the original AST into a Java one. The difference between the last three works and ours is that we do not specifically target PL specification through syntactic desugaring. Our semantics components can be used with or without a core semantics, and, are not restricted to any particular formalism.

Two important ingredients of our approach are type constraints and multiple inheritance. Kiama [START_REF] Sloane | Lightweight Language Processing in Kiama[END_REF] is an LDF that is embedded in Scala. Hence, Kiama does already have all the language support required by our approach. Maude [START_REF] Clavel | The Maude 2.0 System, Rewriting Techs & App[END_REF], K [START_REF] Florin S ¸erbȃnut ¸ȃ | The K Primer (version 2.5)[END_REF], MMT [START_REF] Chalub | Maude MSOS Tool[END_REF], Redex [START_REF] Felleisen | Semantics Engineering with PLT Redex[END_REF], Liga [START_REF] Kastens | Modularity and Reusability in Attribute Grammars[END_REF], Silver [START_REF] Van Wyk | Silver: an Extensible Attribute Grammar System[END_REF], Rascal [START_REF] Klint | EASY Meta-programming with Rascal[END_REF], UUAG [START_REF] Dijkstra | The Architecture of the Utrecht Haskell Compiler[END_REF], JastAdd [START_REF] Ekman | The JastAdd Extensible Java Compiler[END_REF], and Spoofax [START_REF] Kats | The Spoofax Language Workbench: Rules for Declarative Specification of Languages and IDEs[END_REF] are LDFs that ship with their own DSL as the meta-level PL. Maude is the only such LDF with support for both multiple inheritance and type constraints. JastAdd, UUAG, and Rascal each only provide built-in support for half the language features that our approach requires. Only a runtime simulation of our approach is possible in K, Redex, Liga, Spoofax, and Silver.

Finally, Axelsson [START_REF] Axelsson | A Generic Abstract Syntax Model for Embedded Languages[END_REF] and Bahr [START_REF] Bahr | Parametric Compositional Data Types[END_REF] provide Haskell libraries to improve different aspects of embedded DSL mechanisation. They both build on Swierstra's data types à la carte [START_REF] Swierstra | Data Types à la Carte[END_REF] and proceed by offering a new abstract syntax model.

Scala Syntax

This section introduces the parts of Scala syntax that we use in this paper. The method apply (line 1) tells Scala to expand calls like O(1) to O.apply [START_REF] Abramsky | Full Abstraction in the Lazy Lambda Calculus[END_REF]. The nested types NT1 and NT2 of the class C0 (line 2) can be referred to as C0#NT1 and C0#NT2, respectively. This contrasts with Scala's dot notation for referring to members of a package. We say that C0 binds NT1 to Int. The nested type NT2 is abstract in that C0 itself does not bind it. Class C1 is parametrised over type T (line 3). Likewise, method m is parametrised over type U (line 4). The type parameter T1 of C2 is constrained by an upper bound type T2 (line 6). As a result, one can only instantiate C2 with types which inherit from T2. The types to instantiate C3 with need to also have a nested type NT (line 7). One can also place constraints on nested types of type parameters. The plus used before type parameter T in line 8 implies that when T1 is a subtype of T2, C4[T1] is considered a subtype of C4[T2]. Use of underscore in line 9 indicates that one can instantiate C5 with any type that inherits from C2[T'], for some type T'. Type parameters can be more than one, in which case they are separated using commas. Multiple nested types demanded by an upper bound are to be put on separate lines, or, separated using semicolons. Class C6 places two upper bound constraints on its type parameter T (line 10). Namely, the type parameter T has to inherit from both C0 and C2[T]. (Note that T itself is used in its own latter upper bound.) Traits are like abstract classes, but can be multiply inherited.

The Implemented Family of Operational Semantics

Five systems in the family of lazy evaluation are: Abramsky and Ong [START_REF] Abramsky | Full Abstraction in the Lazy Lambda Calculus[END_REF], Launchbury [START_REF] Launchbury | A Natural Semantics for Lazy Evaluation[END_REF], Sinot [START_REF] Sinot | Complete Laziness: a Natural Semantics[END_REF], van Eekelen and de Mol [START_REF] Van Eekelen | Reflections on Type Theory, λ-Calculus, and the Mind[END_REF], and Haeri [START_REF] Haeri | Observational Equivalence and a New Operational Semantics for Lazy Evaluation with Selective Strictness[END_REF]. We will be referring to these as L 0 , L 1 , L 2 , S 1 , and S 2 , respectively. 2 Moreover, we will refer to the syntax of a family member as a member syntax, and, to its semantics as a member semantics. Section 4.1 provides an overview of the family syntax. Section 4.2 exhibits only the parts of family semantics that we refer to in this paper. The reader may refer to the original papers for more explanation. The aim of this section is to give the reader enough understanding from the family so that they can follow our discussions. We chose these particular five systems because their good proximity makes demonstration easy. However, given the flexibility in our components, our approach is well applicable beyond just these five.

Syntax

Here, we briefly present the syntax of the implemented family. Notationally, our presentation is not exactly the same as the original ones. We unify the original notations and neglect the minor differences. Figure 1 shows the family syntax where e ranges over expressions, v ranges over values, and, x ranges over variables. The left half of the figure demonstrates the syntax common between L 0 , L 1 , S 1 , and S 2 . With the great degree of commonality between the four, we demonstrate them altogether in a single compact form to avoid repetition. Ticks show the constructors in each member syntax.

To the right, the top half shows complete L 2 syntax, which is a bit different from the previous four. Here, -→ x is a short form for

x 1 x 2 • • • x n where n ≥ 2.
In L 2 , the generalised identifier b ranges over ordinary variables and metavariables (Z( -→ x )). Function applications are likewise generalised. That is, application of functions is allowed to metavariables as well as variables. λ-abstractions are the only values at L 0 , L 1 , and S 1 . Whereas, in S 2 , let-surrounded λ-abstractions are also considered values, where let {x i =e i } n i=1 in λx.e is a syntactic sugar for λx.e when n = 0. In the L 2 syntax, successive applications of a variable to generalised identifiers (x b 1 • • • b n ) is also considered a value. We refer to this syntactic category as the variable-to-identifier-applications. In the entire family, subscripts do not impact the syntactic category, and, are allowed to be arbitrary. Here, rule labels are of the form (r) where r is the rule name and is the list of family members containing r in their semantics. Rules are of the form Γ : e ⇓ ∆ : v where capital Greek letters denote heaps. This rule form reads: Evaluation of e in Γ results in v and updates the bindings to ∆. We write Γ : e ⇓ Π ∆ : v to emphasise that Π is the derivation tree for Γ : e ⇓ ∆ : v. In L 1 's terminology, heaps are partial functions from variables to expressions. S 1 as well as S 2 inherit the same terminology. In the semantics of L 2 , however, the domain of heaps consists of the set of variables and metavariables. e[x/y] denotes capture-avoiding substitution of variable x in e by variable y. All the family members have a distinct-name convention, i.e., variable names are supposed to be distinct.

Semantics

(lam)L 1 ,S 1 ,L 2 Γ : λx.e ⇓ Γ : λx.e Γ : e ⇓ ∆ : v (var)L 1 ,S 1 ,S 2 ,L 2 (Γ, x → e) : x ⇓ (∆, x → v) : v Γ : e ⇓ ∆ : λy.e ∆ : e [x/y] ⇓ Θ : v (app)L 1 ,S 1 Γ : e x ⇓ Θ : v (Γ, xi → ei) n i=1 : e ⇓ ∆ : v (let)L 1 ,S 1 ,L 2 Γ : let {xi=ei} n i=1 in e ⇓ ∆ : v Γ : e1 ⇓ Θ : v1 Θ : e2 ⇓ ∆ : v2 (seq)S 1 ,S 2 Γ : e1 seq e2 ⇓ ∆ : v2

Components

Figure 3 gives a UML overview of our approach. At the top, elements of our approach for syntax mechanisation are illustrated, and, at the bottom, those of semantics. The left portions are class diagrams. The right portions are use cases for the left portion of the same row. We use a number of non-standard UML notations: The type Exp with which a LazyExp (top left portion) is instantiated has to inherit from LazyExp itself. There are similar constraints on the type parameter Exp of OpSem as well as Exp and OS of the apply method of Executable Rule (all in the bottom left portion). Abusing the UML notation, we draw generalisation arrows that extend from the right portions (use cases) to the respective left (class diagrams). For instance, L1OpSem inherits from OpSem. Finally, in the top row, we use a non-standard dashed arrow "ntb" to specify that an Expression Trait binds nested types to its type constructors. As an example, L1Exp binds its nested type Val to its type constructor Lam. (See the top right portion.) For reasons of improved correctness and reusability that we explain later, we need to check whether a PL syntax contains a certain syntactic category or not. Implementing a syntax using a typical algebraic datatype will, hence, not suffice. This is mainly because an ordinary algebraic datatype does not provide a mechanism for programmatically querying its type constructors. In Section 5.1 where our syntax components are presented, we employ nested types as an extra storage that make such programmatic queries possible. Our approach enjoys a design-by-contract flavour in that the names and duties of these nested types are dictated by the intermediate classes -at their design time. This flavour will also be available in Section 5.2, where our semantics components are introduced.

Syntax Components

In an embedded setting, mechanisation of a PL syntax typically involves embedding its abstract and concrete syntax, pretty-printing and the rest of debugging cosmetics, and sanity checks. One can of course perform the same task repeatedly for each member syntax. This entails a total of at least 24 type constructors for Figure 1 with a great amount of reimplementation in the above syntax mechanisation tasks. We instead mechanise a PL syntax in terms of our reusable components that serve as syntactic building blocks. Each of these components -called "intermediate classes" -corresponds to one and only one syntactic category. (See Intermediate Class in the top left portion of Figure 3.) An intermediate class implements its own part of an abstract syntax, pretty-printing, and sanity checks. This one-off implementation, then, is readily available to whatever PL syntax that contains the respective syntactic category, and, can be used off-the-shelf. For example, for Figure 1, we have implemented a total of 9 intermediate classes that correspond to variables (BaseVar), λ-abstractions (BaseLam), function applications (BaseApp), let-expressions (BaseLet), selective strictness (BaseSeq), metavariables (BaseMVar), generalised identifiers (BaseGenIdn), let-surrounded λ-abstractions (BaseVal), and variable-to-identifier-applications (BaseVarApp). On the other hand, we embed concrete syntax in terms of LazyExp -once and for all. LazyExp is our root of expressions for the entire family. (Compare with LazyExp in the top left portion of Figure 3.)

In Section 5.1.1, we first explain how to put our syntax components together to gain a complete syntax mechanisation. We, then, take a deeper look into some internals of our code which made this possible in Section 5.1.2.

Syntax Mechanisation When appropriate intermediate classes and

LazyExp are at hand, a simple discipline needs to be followed:

-A member syntax is mechanised using its own (algebraic data-) type. Such a type provides its extra storage using binding nested types to its respective type constructors. When a syntax is mechanised in such a fashion, we refer to its implementing datatype as an "expression trait." Furthermore, when a type constructor is bound in such a fashion, we say it is register ed (at the expression trait). To inherit the concrete syntax embedding, and to be of use to our semantics mechanisation utilities, an expression trait T always derives from LazyExp[T]. -Type constructors themselves need as well to specify which syntactic category they belong to. With their type parameters that will be explained later, we consider our intermediate classes only half-baked. We say that an intermediate class gets fully-baked for an expression trait T when a type constructor of T inherits from their instantiation for T. Note that the type of the latter parameter is not fixed. Instead, it is typed using the type parameter Exp (line 1). The upper bound on Exp makes BaseLet invariably available to every member syntax so long as Exp registers its BaseLetderived type constructor under the name Let. (Namely, L 0 is excluded.) Similar type constraints selectively determine the appropriate classes of syntax.

It remains to further expand on the role of LazyExp. In this section, we focus only on the syntactic parts of its role. Section 5.2 explains its role for semantics mechanisation. We implement all our concrete syntax embedding for LazyExponce and for all. When applicable, a member syntax reuses the same embedding through inheritance of its expression trait from LazyExp. The following table summarises our concrete syntax embedding: In each row, the code on the left gets automatically desugared into a piece of abstract syntax that represents the mathematical expression on the right. (T in line 2 is the corresponding expression trait of e.) code math 1 e("x1")...("xn")

((e x 1 ) • • • x n ) 2 \[T]("x1",...,"xn")(e) λx 1 • • • x n .e 3
let ("x1" -> e1,...,"xn" -> en) in e let {x i =e i } n i=1 in e 4 e1 seq e2 e 1 seq e 2 Note that the code in line 2 embeds a let-surrounded λ-abstraction in S 2 's syntax and ordinary λ-abstractions in other family members. Likewise, when e is a λ-abstraction, the code in line 3 embeds another λ-abstraction for S 2 's syntax, and, let-expressions otherwise. On the other hand, the embedding in line 4 is only applicable when a syntactic category is available for selective strictness. Again, the selectivity on the classes of syntax is enabled by type constraints.

As also explained further above, our convention is that an expression trait T must derive from LazyExp[T]. (See line 3 in Figure 4 for L1Exp, for example.) Given that T's type constructors inherit from it, they also inherit from LazyExp by transitivity of inheritance. Note how following our convention for expression traits makes them distinguishable from type constructors. The particular wiring used below for the type parameter Exp of LazyExp enforces the above convention. Section 5.2 contains an example where this convention comes handy.

Semantics Components

Similar to the case for syntax, it is perfectly possible to program each member semantics separately. That is a total of 23 rules for the entire family, and, with a great deal of code repetition. Instead, we implement a collection of 14 reusable and executable rules, which can be plugged into a PL semantics mechanisation. Our design ships another artefact as well: OpSem is our root operational semantics class. This is an abstract base class with a method for distributing the semantics evaluation between executable rules. Yet, OpSem is flexible on its input/output to the extent that it allows several semantics mechanisations for a single syntax. In this paper, we only demonstrate the idea for rules which document the entire semantics evaluation, if successful. However, one can easily configure OpSem for rules which, for instance, merely work with the PL objects involved in the semantics specification. Although we only demonstrate mechanisation for operational semantics, we have no evidence to doubt the applicability of our approach to other formalisms. After all, it only amounts for the semantic rules to be implemented like our executable rules.

In Section 5.2.1, we first explain how to combine our components to mechanise a PL semantics. A closer look into our components themselves is then provided in Section 5.2.2. Whilst the latter section targets LDF implementers more, the former one is more useful to the LDF users.

Semantics Mechanisation

Assuming the availability of our components, the following programming discipline needs to be followed for semantics mechanisation: A member semantics is implemented as a stand-alone object that derives from OpSem[T], where T is the expression trait of the corresponding member syntax. This object needs to implement a method proofsearch which distributes evaluation between pertaining executable rules. In such a case, we say the member semantics plugs its appropriate executable rules. For example, for L 1 's semantics, the method proofsearch in Figure 5 takes a heap along with an expression (line 5), and, produces a derivation tree, when successful: Here, the plugged executable rules are HBLamRule, HBAppRuleLam, HBVarRule, and HBLetRuleLam (lines 6 to 9, respectively) that we schematically depicted in Figure 3. (In our naming convention, prefix HB indicates a heap-based system. That includes all the family members in this paper except L 0 .) What comes after the executable rule names in square brackets is to guide Scala's type deduction. HBNode is the root of our hierarchy for nodes in the heap-based derivation trees. Each node class encapsulates relevant compile time/runtime sanity checks that make it easier to enforce correctness of the executable rules. Armed with such correctness enforcement mechanisms, the compiler would have stopped us, for any of the four cases, had we plugged in a rule which is incompatible with the respective characteristics of either L 1 's syntax or semantics.

Technicality

Implementing a rule in a way that is not exclusively useful to a particular PL entails parameterising it over both the syntax and semantics. And, indeed the type parameters of our executable rules characterise both the syntax and semantics they expect. Our rules can be plugged into any semantics so long as their characteristic expectations hold. A compile error will be emitted otherwise. For example, below is our (let) L1,S1,L2 implementation: The type parameters Exp and OS above (lines 2 and 4) signify the expression trait and the operational semantics, respectively. However, not every rule in Figure 2 is a part of every member semantics. For example, this (let) rule is only a part of the L 1 , S 1 , and L 2 semantics. The constraint type Val <: BaseLam[Exp] (line 2) rules out S 2 . This constraint enforces on Exp the availability of a nested type Val that binds to a class derived from BaseLam, i.e., that λ-abstractions is a value type of the syntax. (See Figure 1.) OS <: OpSem [Exp] states that OS must be an operational semantics type over the expression type Exp. (More on OpSem shortly.) The constraint type Conf = HBConf[Exp] (line 4) on OS states that it inputs a pair of heap and expression. Similarly, type Node = HBNode[Exp] (line 5) specifies that OS outputs a heap-based derivation tree. These constraints rule out the semantics of L 0 too, making HBLetRuleLam only applicable to the right family members. Lastly, note how the treatment of type parameters enables opsem to take a continuation-passing style role for handling "the rest of the evaluation" -again, only for the correct family members.

Here is a recap on the remaining points: The constraint type Let <: BaseLet[Exp] (line 3) ensures that Exp registers its BaseLet-derived constructor under the name Let. Furthermore, lexp (in line 6) is required to be an instance of both Exp and this registered type. In other words, lexp needs to be constructed using a type constructor of Exp that corresponds to let-expressions. Recall also that, as seen at the end of Section 5.1, the constraint Exp <: LazyExp[Exp] (line 1) ensures that Exp is an expression trait. HBLetNodeLam inherits from HBNode to be the node for let-expressions where λ-abstractions are a value type.

It remains to consider our OpSem trait: For each operational semantics, proofsearch inputs the initial configuration, and, produces the derivation tree according to the rules of the semantics. The ab-stract type Conf represents the type signature of the input (line 2). Likewise, the abstract type Node is the derivation tree type an operational semantics outputs (line 3). The type ProofTree is our generic ADT for derivation trees.

Case Study: Analysis Code Reuse

Like the case of syntax and semantics, one should be able to reuse the code for analyses implemented over previous mechanisation cycles -but, only when they are still conceptually applicable. We address that need based on two facts: Fact 1. Old code that is implemented in terms of the root of a hierarchy works for new classes that derive from the root. Fact 2. Code that constraints its type parameters can employ the compiler to prevent its use for wrong types.

Information gathering over derivation tree traversals is the essence of many analyses. A crude idea can, thus, be implementing all the analyses over a single generic tree type. However, such a tree is unaware of the types its nodes contain. One would rather make all the derivation tree types inherit from such a generic type. This way, old code which operates on the generic type can remain intact over the addition of new derivation types. (C.f. Fact 1.) More precision can also be gained by giving this hierarchy extra intermediate nodes. On the other hand, by constraining the type parameters of analysis implementations, one can avoid their wrong application. Constraints can enforce applicability of an analysis to all derivation trees that say derive from a certain base. (C.f. Fact 2.) We call the process of organising derivation tree types in a hierarchy and implementing analyses in terms of the suitable hierarchy node "multi-levelling analyses."

Our hierarchy of derivation trees is rooted in ProofTree (seen first in Section 5.2). ProofTree has a minimal understanding of what it contains. All it knows is that a set of premisses leads to a conclusion using a rule label. HBNode and HLNode extend ProofTree for heap-based nodes and the heap-less ones, respectively. Nodes which represent derivation in the L 0 operational semantics are instances of HLNode. All other nodes are of type HBNode. Both HBNode and HLNode provide more specific information. For example, the former also knows that its conclusion is always a 4-tuple for the Γ : e ⇓ ∆ : v scheme. Further down in the hierarchy come nodes that correspond to semantics rules, and hence, executable rules. These latter nodes know the syntactic category of their e in the above scheme. For instance, HBVarNode that corresponds to (var) L1,S1,S2,L2 knows that it works on variables. At the same level are types for the derivation trees of the individual family members. L1Node, for instance, is that of L 1 . Obviously, L1Node has more specific information at hand, e.g., the exact type of expressions/heaps it works with.

Generally, analyses remain invariably useful over several mechanisation cycles so long as they are implemented in terms of the right level at the derivation tree hierarchy. Most of what makes such a hierarchical craft of derivation trees helpful stems from the high degree of flexibility in executable rules. The apply methods of the executable rules presented in this paper all have HBNode return types. However, it is trivial to configure executable rules otherwise and still enjoy them as reusable components for semantics mechanisation. We also gain other sorts of analysis reusability from the high degree of reusability in intermediate classes. For example, an analysis which deals with evaluation of a particular syntactic category can remain intact over consecutive mechanisation cycles even though the actual type constructors involved vary across the cycles. We will not demonstrate reusability of this latter sort in this paper.

As a first example, consider an analysis the right level for in our hierarchy is ProofTree: Counting the number of rules used over a derivation. This analysis does not need any knowledge about the types involved over the proof search. It is a simple folding action over the premisses (line 2) with axioms as the basis of induction (line 1). An occasion where this counting might be useful is comparing the cost of designated computations across different semantics which are known to be observationally equivalent.

Our second example is on the analyses in Definition 1, which play a central role in the observational equivalence theorems on S 2 [START_REF] Haeri | Observational Equivalence and a New Operational Semantics for Lazy Evaluation with Selective Strictness[END_REF]:

Definition 1. Suppose Γ : e ⇓ Π ∆ : v. Define diff (Π) = {x ∈ dom(Γ ) | Γ (x) = ∆(x)}. Call x atomic in Γ when there exist ∆ x , v x , and Π x such that Γ : x ⇓ Πx ∆ x : v x and diff (Π x ) = {x}.
In fact, as opposed to only S 2 , diff and atomic are analyses applicable to any heap-based semantics. Here is how we employ that observation: Notice that atomic characterises the syntax and semantics it is applicable to through the constraints on the type parameters (lines 6-8). Consequently, it remains applicable upon extensions of mechanisation so long as the characteristics remain intact. Thanks to our multi-levelling, in the implementation of diff, types are all correctly identified by the compiler. We would have not had such a pleasure, had we implemented it on ProofTree, which is oblivious of the types inside it. This static safety becomes clearer in the next example where we examine order of evaluation of variables for any heap-based semantics: EvalList produces the list of evaluated variables in order. Due to space restrictions, we only report how the above single implementation of EvalList remains applicable upon extending mechanisation of L 1 to S 2 . Let heap Γ = {id → λt.t, y → (λt 1 t 2 .t 1 ) id x, x → (λt 1 t 2 .t 2 ) id} be represented by g. For L 1 , EvalList(g <::> "y") produces List(y), whilst List(x, y) is produced by EvalList(g <::> ("x" seq "y")) for S 2 . 4Due to multi-levelling, Scala precisely infers the types for pi, xvar, g, and d. There is no need for runtime casting. To get multi-levelling, we identified that this analysis is applicable to any heap-based derivation tree on expression traits with a syntactic category for variables. We enforced that by making EvalList applicable to any such tree through placing the type constraints at line 2. It is exactly this constraint that creates a flow of type information that automates type inference of the above variables. In the absence of that type information in scope, one has to manually set variable types and/or even resort to runtime casting to calm the type system.

Conclusion and Future Work

In this paper, we present our components for syntax and semantics mechanisation. As a driving example, we use five systems for lazy evaluation to show how these components can serve reusability in the mechanisation of PL syntax, semantics, and analysis. We also discuss the internals of our components and how, using type constraints and multiple inheritance, they are engineered for this particular sort of code reuse.

Using our components imposes some modest programming discipline. A PL implementer's part of this discipline is indeed minimal. And, yet, the effort to suit the reusability is incomparably smaller than reimplementation: For syntax, this effort amounts to simply deriving from an extra base class (i.e., intermediate classes for each type constructor) and binding the type constructors under some fixed nested type of the expression trait (Figure 4). For semantics, it takes deriving from an abstract base class (e.g., OpSem) and implementing a method (like proofsearch) that merely distributes the evaluation task between the appropriate executable rules (Figure 5).

Shipping our components is certainly a new burden on LDFs. Implementing our components can sometimes become clunky. This is mainly because, working with constrained type parameters as opposed to exact types makes some extra indirection inevitable. The burden on LDFs magnifies are they to ship an exhaustive set of our components which the PL implementer can freely mix-and-match; that is, after all, likely to take several rounds of refactoring on its way.

Whether or not our approach will scale is a topic for further research. One might also study the classes of extensions in terms of the refactoring they dictate. For example, having had implemented our approach for the other four family members, addition of L 2 dictated some refactoring to our codebase. Regarding further extensions, the effort might vary: For example, adding integer arithmetic as sketched in the L 1 's original paper [START_REF] Launchbury | A Natural Semantics for Lazy Evaluation[END_REF] is routine. Addition of Eden's strict function application [START_REF] Loogen | Parallel Functional Programming in Eden[END_REF] would also be relatively easy. However, we anticipate that adding the lazy evaluation material of Danvy et al. [START_REF] Danvy | On inter-deriving small-step and big-step semantics: A case study for storeless call-by-need evaluation[END_REF] needs refactoring.

Our components enjoy composability, but, are not atomic. That is, whilst it is trivial to compose our components to acquire new ones, not every semantic rule can be composed out of existing ones. For example, the subtle difference between (app) L1,S1,L2 and the function application rule of S 2 means that neither can be implemented in terms of another. The study of atomic support for implementing our components is yet another future work.

  object O {def apply(n: Int) = ...} class C0 {type NT1 = Int; type NT2} class C1[T] { def m[U]: Int -> Int = ... } class C2[T1 <: T2] class C3[T1 <: T2{type NT}] class C4[+T] class C5[T <: C2[_]] class C6[T <: C0 with C2[T]]

L0Fig. 1 .

 1 Fig. 1. Syntax for All the Family Members

L1=

  Launchbury, S1= van Eekelen and de Mol, S2= Haeri, L2= Sinot

Fig. 2 .

 2 Fig. 2. Selected Parts of the Family Semantics

Figure 2

 2 Figure2shows selected parts of the family semantics. Here, rule labels are of the form (r) where r is the rule name and is the list of family members containing r in their semantics. Rules are of the form Γ : e ⇓ ∆ : v where capital Greek letters denote heaps. This rule form reads: Evaluation of e in Γ results in v and updates the bindings to ∆. We write Γ : e ⇓ Π ∆ : v to emphasise that Π is the derivation tree for Γ : e ⇓ ∆ : v. In L 1 's terminology, heaps are partial functions from variables to expressions. S 1 as well as S 2 inherit the same terminology. In the semantics of L 2 , however, the domain of heaps consists of the set of variables and metavariables. e[x/y] denotes capture-avoiding substitution of variable x in e by variable y. All the family members have a distinct-name convention, i.e., variable names are supposed to be distinct.

Fig. 3 .

 3 Fig. 3. Architecture of our Approach

Figure 4 Fig. 4 .

 44 Figure 4 exemplifies our discipline for L 1 . Scala uses normal inheritance as a simple facility for extensible algebraic datatypes. Accordingly, Var, Lam, App, and Let (lines 11-14) are type constructors of L1Exp. They are fully-baked for L 1 's

1 trait

 1 LazyExp[+Exp <: LazyExp[Exp]] {...}

Fig. 5 .

 5 Fig. 5. Implementing the L1 Operational Semantics in Isolation

  object HBLetRuleLam { def apply[Exp <: LazyExp[Exp]{type Val <: BaseLam[Exp] type Let <: BaseLet[Exp]}, OS <: OpSem[Exp]{type Conf = HBConf[Exp] type Node = HBNode[Exp]}] (g: Heap[Exp], lexp: Exp#Let with Exp) (implicit opsem: OS): HBNode[Exp] = { val (e, bs) = (lexp.e, lexp.bs) val pi = opsem.proofsearch(g ++ bs, e) val (d, z) = (pi.g2, pi.e2) new HBLetNodeLam[Exp](pi, g, lexp, d, z) } }

  def rulecount(p: ProofTree): Int = if (p.prems.isEmpty) 1 else (0 /: p.prems) (_ + rulecount(_))

3

 3

  object diff { def apply[Exp <: LazyExp[Exp]](pi: HBNode[Exp]): Set[Idn] = for(x <-pi.g.dom; if(pi.g(x) != pi.d(x))) yield x }//diff(pi) = {x ∈ dom(pi.g) | pi.g(x) != pi.d(x)} object atomic { def apply[Exp <: LazyExp[Exp]{type Var <: BaseVar}, OS <: OpSem[Exp]{type Conf = HBConf[Exp] type Node = HBNode[Exp]}] (g: Heap[Exp], x: Idn)//x is atomic in g when... (implicit opsem: OS, variabliser: Idn => Exp with Exp#Var): Boolean = diff(opsem.proofsearch(g, x)) == Set(x)//... diff(pix) == {x}, }//where pix = opsem.proofsearch(g, x).

  object EvalList { def apply[Exp <: LazyExp[Exp]{type Var <: BaseVar}] (hbn: HBNode[Exp]): List[Idn] = hbn match { case HBVarNode(pi, g, xvar, d, _) => {//(var)L 1 ,S 1 ,S 2 ,L 2 in Fig. 2: val prev = EvalList(pi)//what gets evaluated in the premisses... val x = xvar.name if(g(x) != d(x)) (prev:::List(x)) else prev }//... plus x itself when g(x) != d(x). case _ => //Otherwise: union what is evaluated in the premisses. (for(p <-hbn.ps) yield EvalList(p)).toList.flatten }//Note: hbn.ps == premisses of hbn }

online source code available at http://www.sts.tuhh.de/~hossein/compatibility.

variabliser is our implementation detail in charge of reifying an identifier into an expression of the right type (i.e., a variable).

g <::> e abbreviates os.proofsearch(g, e) when os is an implicit in scope.


Peter H Wong
email: peter.wong@fredhopper.com

Peter Y H Wong

Compositional Development of BPMN

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Modelling of business processes and workflows is an important area in software engineering. Business Process Modelling Notation (BPMN) [START_REF] Omg | Business Process Modeling Notation[END_REF] allows developers to take a process-oriented approach to modelling of systems. There are currently over seventy implementations of the notation, but the notation specification does not have a formal behavioural semantics, which we believe to be crucial in behavioural specification and verification activities. Previously a process semantics [START_REF] Wong | A Process Semantics for BPMN[END_REF] has been given for a large subset of BPMN in the language of Communicating Sequential Processes (CSP) [START_REF] Roscoe | The Theory and Practice of Concurrency[END_REF]. This semantics maps BPMN diagrams to finite state CSP processes. Using this semantics, the behaviour expressed in BPMN can be formally verified and BPMN diagrams can be behaviourally compared. Verification and comparison are expressed as CSP traces and failures refinements. Refinements of finite state CSP processes can be automatically verified using a model checker like FDR [START_REF]Formal Systems (Europe) Ltd. Failures-Divergences Refinement, FDR2 User Manual[END_REF].

Monotonicity and Refinement

One major problem of verifying concurrent systems by model checking is potential state explosion. To alleviate this one can exploit compositionality. Our constribution is to introduce a comprehensive set of operations to incrementally construct BPMN diagrams. We provide these operations with a CSP semantics, and characterise the conditions under which the operations are monotonic with respect to CSP refinements. These operations are partitioned into the following categories: sequential composition, split, join, iteration, exception and collaboration.

The combination of monotonicity and refinement allows one to construct and verify behavioural correctness of large complex systems compositionally. Informally, for any two BPMN diagrams C and D, D C denotes C is a refinement of D. We let f (.) be an operation over BPMN diagrams. If f (.) is monotonic with respect to the refinement, then by construction f (D) f (C ) ⇔ D C for all BPMN diagrams C and D. As a result we can incrementally increase the complexity of C and D using the proposed operations without needing further verification.

Moreover, monotonic operations preserve refinement-closed properties. A relation ⊕ is refinement-closed if and only if for all BPMN diagrams P and Q such that if P ⊕ Q, then it is the case that P ⊕ Q for all P P and Q Q . One important refinement-closed property is the behavioural compatibility, compatible, between BPMN pools [START_REF] Wong | Formalisations and Applications of Business Process Modelling Notation[END_REF][START_REF] Wong | Property Specifications for Workflow Modelling[END_REF]. Given two BPMN pools P and Q, compatible(P , Q) if and only if P and Q are deadlock free and that their collaboration is deadlock free. If we let f (.) be a monotonic operation over BPMN diagrams and compatible(f (C ), f (D)), then by construction compatible(f (C ), f (D )) for all C and D such that C C and D D . As a result we may use the proposed operations to perform independent development while maintaining any refinement-closed properties.

Structure

This paper begins with a brief introduction to Z and CSP in Section 2, and then an overview of the abstract syntax of BPMN in Z and its behavioural semantics in Section 3. Our contribution starts in Section 4: in this section we introduce a set of operations to construct BPMN diagrams and provide them with a CSP semantics. Using this semantics, we characterise the conditions under which these operations are monotonic with respect to CSP refinements. We conclude this paper with a discussion on related work and a summary.

Preliminaries

Z The Z notation [START_REF] Woodcock | Using Z: Specification, Proof and Refinement[END_REF] is a language for state-based specification. It is based on typed set theory with a structuring mechanism: the schema. We write some schema N to make declaration d that satisfies constraint p as

N = [d | p].
Z provides a syntax for set expressions, predicates and definitions. Types can either be basic types, maximal sets within the specification, each defined by simply declaring its name [Type], or be free types, introduced by identifying each of the distinct members, introducing each element by name Type ::= E 0 | ... | En . By using an axiomatic definition we can introduce a new symbol x , an element of S , satisfying constraint p.

x : S p CSP In CSP [START_REF] Roscoe | The Theory and Practice of Concurrency[END_REF], a process is a pattern of behaviour, denoted by events. Below is the syntax of the subset of CSP used in this paper.

P , Q ::= P ||| Q | P |[ A ]| Q | P |[ A | B ]| Q | P 2 Q | P Q | P o 9 Q | e → P | Skip | Stop
Given processes P and Q, P ||| Q denotes the interleaving of P and Q; P |[ A ]| Q denotes the partial interleaving of P and Q synchronising events in set A; P |[ A | B ]| Q denotes parallel composition, in which P and Q can evolve independently performing events from A and B respectively but synchronise on events in their intersection A ∩ B ; we write i :

I • A(i) • P (i)
to denote an indexed parallel combination of processes P (i) for i ranging over I . P 2 Q denotes the external choice between P and Q; P Q denotes the internal choice between P or Q;

P o 9 Q denotes the sequential composition of P and Q; e → P denotes a process that is capable of performing event e, and then behaves as P . The process Stop is a deadlocked process and the process Skip is a successful termination. One of CSP's semantic models is the stable failures (F) The stable failures model records the failures of processes. We write traces(P ) and failures(P ) to denote the traces and the failures of process P . A failure is a pair (s, X ) ∈ failures(P ) where s ∈ traces(P ) is the trace of P and X is the set of events of P refuses to do after s. CSP semantics admit refinement orderings such as the stable failures refinement P F Q ⇔ traces(P ) ⊇ traces(Q) ∧ failures(P ) ⊇ failures(Q). Refinement under the stable failures model allows assertions about a system's safety and availability properties.

Formalising BPMN

A BPMN diagram is made up of a collection of BPMN elements. Elements can either be events, tasks, subprocesses or control gateways. Elements are grouped in pools. A pool represents a participant in a business process; a participant may be an entity such as a company. Elements in a pool are connected by sequence flows to depict their flow of control in the pool, A BPMN diagram is a collection of pools in which elements between pools may be connected by message flows to depict the flow of messages between pools.

As a running example we consider the BPMN diagram shown in Fig. 1. The diagram describes the business process of an online shop promoting a sale. Specifically, it is a business collaboration between an online shop and a customer, depicted by two pools. The online shop business process begins by sending a message to the customer about a sale offer. This is modelled as a message flow from the task named Send Offer to the message event. The business process then waits until it receives either a confirmation or a decline from the customer. This decision waiting is modelled using the event-based exclusive-or gateway from the Send Offer task to the tasks Receive Confirmation and Receive Decline. If a decline is received, the online shop business process ends. If a confirmation is received, the online shop receives payment from the customer, sends the invoice and dispatches the goods to her. The customer's business process begins by receiving a message from the online shop about a certain promotion item. She may either accept or decline the offer. The decision is modelled using the databased exclusive-or gateway from the message event to the tasks Decline Offer and Accept Offer. If she decides to accept the offer, she sends payment to the shop, modelled by task Send Payment, then waits for her offer. This is modelled as a subprocess Receive Offer consisting of two tasks: The task Receive Goods models the receiving of goods, while Receive Invoice models the receiving of the invoice. Note these activities may happen in either order and this is modelled using a parallel gateway to both tasks. If she declines the offer, the business process ends.

We now give an overview of BPMN's abstract syntax in Z and its semantics in CSP. For brevity, we highlight only the most important aspects of the syntax and semantics. The complete formalisation of the syntax and semantics can be found in the author's thesis [START_REF] Wong | Formalisations and Applications of Business Process Modelling Notation[END_REF]Chapters 4,[START_REF] Istoan | Defining Composition Operators for BPMN[END_REF].

In the abstract syntax we let basic types Sflow and Mflow be types of sequence flows and message flows, and TaskName be the type of task names; we use the free type We define schema Pool = [proc : F 1 Element] to record individual pools, it defines component proc to record a non-empty finite set of BPMN elements contained in a pool; note that for brevity we have omitted the specification of predicate constraints on that component. We define InitPool = [proc : F 1 Element | proc = {se, ee}] to be the initial state of Pool , where se is a start event and ee is an end event such that (atom ∼ se).ou = (atom ∼ ee).in. We also specify the structure of a BPMN diagram using the schema We define the semantic function bToc that takes a BPMN diagram and returns a CSP process that models communications between elements in that diagram. We present the semantic definition in a bottom up manner, starting with individual BPMN elements.

We first define function aToc to model atomic elements, that is, events, tasks and gateways. The function defines the behaviour of the elements by sequentially composing the processes that model the element's incoming sequence flows and message flows, the element's type and the element's outgoing sequence flows and message flows. Note that other than start and end events, aToc models other atomic elements as recursive processes.

aToc : Element → CSP Our semantics models the communications between elements as a parallel combination of processes, each modelling the behaviour of an element. Our semantics ensures that upon an end event being triggered, the containing BPMN process may terminate if its contained elements can also terminate. This is achieved by insisting that each end event performs a completion event, and that all other elements may synchronise on one of these completion events to terminate.

cp : (F Element × Element) → CSP
The function cp defines the execution of a BPMN element as follows: for an atomic element, cp applies function aToc, and for a compound element, cp applies function mToc; function mToc defines the sequential composition of these processes: the CSP process that models the incoming sequence flows of the compound element; the parallel composition of processes, each modelling an element contained in the compound element, and the CSP process that models the outgoing sequence flows of the element.

mToc : CSP × F Element × CSP → CSP
A BPMN diagram is modelled by semantic function bToc, which defines a parallel composition of processes, each modelling a BPMN pool in the diagram. A pool is modelled by function pToc, which defines a parallel composition of processes, each modelling elements in the pool.

pToc : Pool → CSP bToc : Diagram → CSP
This semantic function induces an equivalence relationship on the behaviour of BPMN diagrams. Two BPMN diagrams are equivalent when each failuresrefines the other. The notion of equivalence is formally defined as follows: Definition 1. Equivalence. Two BPMN diagrams P and Q are equivalent, denoted as

P ≡ BPMN Q if and only if bToc(Q) F bToc(P ) ∧ bToc(P ) F bToc(Q).
For example, we consider our online shop running example shown in Fig. 1. We define CSP process CP in Equation 1 to model the behaviour of the Customer BPMN pool, where αP denotes the alphabet of process P . The start event is identified by sCP while all other BPMN elements in the pool are identified by their incoming sequence flows.

EP = c.s13 → Skip 2 c.s4 → Skip P (sCP ) = (m.m1 → s.s1 → EP ) 2 EP P (s1) = (s.s1 → (s.s2 → Skip s.s3 → Skip) o 9 P (s1)) 2 EP P (s2) = (s.s2 → w .DO → m.m3 → s.s4 → P (s2)) 2 EP P (s3) = (s.s3 → w .AO → m.m2 → s.s5 → P (s3)) 2 EP P (s4) = (s.s4 → c.s4 → Skip) 2 c.s13 → Skip P (s5) = (s.s5 → w .SP → m.m4 → s.s6 → P (s4)) 2 EP P (s6) = (s.s6 → RO o 9 s.s13 → P (s6)) 2 EP P (s13) = (s.s13 → c.13 → Skip) 2 c.s4 → Skip CP = i : {sCP , s1, s2, s3, s4, s5, s6, s13} • αP (i) • P (i) (1)
For presentation purpose, we model sequence flows by prefixing 's.', message flows by 'm.' and completion events by 'c.'. We abbreviate each task name using the first letter of each word in its name. For example, the CSP event w .DO represents the work done of task Decline Offer, the process P (s6) models the behaviour of the Receive Offer subprocess; the definition of RO is defined in Equation 2.

FP = c.s12 → Skip P (sRO) = (s.s7 → FP ) 2 FP P (s7) = (s.s7 → (s.s8 → Skip ||| s.s9 → Skip) o 9 P (s7)) 2 FP P (s8) = ((s.s8 → Skip ||| m.m5 → Skip) o 9 w .RI → s.s4 → P (s8)) 2 FP P (s9) = ((s.s9 → Skip ||| m.m6 → Skip) o 9 w .RG → s.s11 → P (s9)) 2 FP P (s10) = ((s.s10 → Skip ||| s.s11 → Skip) o 9 s.s12 → P (s10)) 2 FP P (s12) = s.s12 → c.12 → Skip RO = i : {sRO, s7, s8, s9, s10, 12} • αP (i) • P (i) (2)
We may similarly define CSP process OS to model the behaviour of the OnlineShop BPMN pool. The CSP process CP |[ αCP | αOS ]| OS then models the interaction between the customer and the online shop business processes.

Constructing BPMN

Using Z we provide a comprehensive set of operations for constructing BPMN processes. Specifically these are operation schemas on the state schemas Pool and Diagram. These operations are partitioned into the following categories: sequential composition, split, join, iteration, exception and collaboration. Informally, sequential composition adds to a BPMN process an activity (a task or a subprocess); split adds a choice to two or more activities; join joins two or more activities via a join gateway; iteration adds a loop using a exclusive-or split and join gateway; exception adds exception flows to a activity, and collaboration connects two BPMN pools with a message flow. While these operations are not part of BPMN, we did not need to extend the existing syntax of BPMN for defining these operations. These operations are designed to provide the following benefits:

1. To provide operations to construct business processes. We have chosen a comprehensive set of operations for constructing business processes similar to those in structured programming [START_REF] Dahl | Structured programming[END_REF]; 2. To ensure the syntactic consistency of business processes by calculating the preconditions of the operations. Precondition calculations can be found in the author's thesis [11, Appendix B]; 3. To allow the compositional development of business processes. We provide a CSP semantics to these operations, and characterise the conditions under which these operations are monotonic with respect to CSP traces and failures refinements, and 4. To encourage formal tool support for constructing business processes. The behavioural of BPMN diagrams constructed using the provided operations admits verification such as automatic refinement checking. These operations can be implemented in a BPMN development environment that supports the semantic translation of BPMN to CSP 1 and the automated refinement checking via model checkers such as the FDR.

Syntax and Semantics

We describe four operations using the combination of Z and CSP; when describing operations, we refer to Fig. 2 for illustration purposes. Diagrams labelled with a number depict an operation's before state and diagrams with a letter depict an operation's after state. Operations whose after states are one of Digrams A and B assume Diagram 1 to be the before state; the operation whose after state is Diagram C assumes Diagram 2 to be the before state, and the operation whose after state is Diagram E assumes Diagram 3 to be the before state.

For reason of space, we mainly focus on semantic definitions of these operations and present the syntactic definition of sequential composition (SeqComp), while for the other operations, we present their type declaration. We also provide an informal description of these operations. We provide functions pf , ext, int and par to model prefixing, external choice, internal choice and interleaving. We provide functions type, in, ou, re and sd on BPMN elements to obtain their type, incoming and outgoing sequence flows, and incoming and outgoing message flows respectively. We provide functions sf , mf and fn to model sequence flow, message flow and completion as CSP events. Furthermore, we provide functions sflow , cnt, ends, eles and modify as follow: Fig. 2. Operations sflow (es) takes a set of elements es and returns all sequence flows of the elements in es; cnt(e) takes element e and recursively returns the set of elements contained in element e; ends(ps) takes a set of elements ps and returns a partial function that maps each incoming sequence flow of an end event to that event; nonsend (ps) takes a set of elements ps and returns a partial function that maps each incoming sequence flow of an element that is not a task or an intermediate event to that element, and modify(ps, ns, os) takes three sets of elements ps, ns and os and returns ps with elements of os contained in ps replaced with elements in ns.

SeqComp The schema SeqComp adds either a task, a subprocess, or an intermediate message event to a BPMN pool. It takes two elements new ? and end ?, and sequence flow from? as inputs and replaces the end event in the component proc that has incoming sequence flow from? with elements new ? and end ?. Schema SeqComp is illustrated by Diagrams 1 and A in Fig. 2, where the end event labelled E is specified by the expression ((ends proc) from?). The illustration shows how this operation replaces element E with element new ? and end ?. Specifically, new ? is either an intermediate message event (with no message flow) or an activity. That is, new ? has exactly one incoming and one outgoing sequence flow, and end ? is an end event. Furthermore, SeqComp includes Commons to ensure the following constraints: 1) no outgoing sequence flow of news as well as of elements contained in new ? must also be a sequence flow of any element contained the before state component proc; 2) from? is an incoming sequence flow of new ?, and 3) from? is also an incoming sequence flow of an end event contained in proc.

We let e denote the end event end (proc) from?. The semantics of new ? and end ? are provided by the processes P (new ?) = cp((proc \ {e}) ∪ {end ?}, new ?) and P (end ?) = cp(proc \ {e}, end ?) respectively. In general, unless otherwise specified, given a state Pool with component proc, we write P (i) to denote the process cp(proc, i), and define as(es) = {i : es • αP (i)} to return the alphabet of the process semantics of elements in es. The semantics of SeqComp is given by the following process, where OB = i : proc \ {e} • ((αP (i) \ {fn(e)}) ∪ fn(end ?)) • cp(proc ∪ {end ?}, i) and AB = as(proc \ {e}) ∪ {fn(end ?)}.

Split The schema Split adds either an exclusive or a parallel split gateway to a BPMN pool. The operation takes as inputs gateway new ?, a set of end events outs?, and sequence flow from?. Schema Split is illustrated by Diagrams 1 and B in Fig. 2, where the end event labelled E is specified by the expression ((ends proc) from?).

The illustration shows how the operation replaces E with element new ? and the set of elements outs?, which contains elements labelled F and G. We now consider the constraints specified by this operation in detail. Split includes constraints specified by Commons about new ?, from? and the before state Pool . It also specifies the following constraints on all input components: 1) new ? must be either an exclusive or a parallel split gateway; 2) outs? must be a non-empty set of end events, in which elements do not share incoming sequence flows; 3) incoming sequence flows of elements in outs? are not sequence flows of elements contained in proc of before state Pool , and 4) incoming sequence flows of elements in outs? are exactly the outgoing sequence flows of new ?.

We let e denote the end event end (proc) from?. The semantics of new ? is then defined as P (new ?) = cp((proc \ {e}) ∪ outs?, new ?), and the semantics of the set of elements outs? can be modelled by the parallel composition of processes QS = o : outs? • αQ(o) • Q(o), where each process Q(o) is defined as cp((proc \ {e}) ∪ outs?, o). The semantics of Splits is then given by the following process, The operation takes input components gateway gate? and end event end ?. Schema Join is illustrated by Diagrams 2 and C in Fig. 2, where the incoming sequence flows of E and F are the incoming sequence flows of gate?. The illustration shows how the operation replaces elements E and F with elements gate? and end ?. Here end ? is labelled G in the illustration. Specifically, Join defines the following constraints: 1) gate? is either an exclusive or a parallel join gateway; 2) end ? is an end event; 3) gate?'s incoming sequence flows are incoming sequence flows of some end events contained in either proc of the before state Pool , or one of the subprocesses contained in proc of the before state Pool ; 4) outgoing sequence flows of gate? are exactly the incoming sequence flows of end ?, and 5) incoming sequence flows of end ? are not sequence flows of elements contained in proc component of the before state Pool .

We let es = end (proc)(| in(gate?) | ), and the semantics of gate? and end ? are provided by P (gate?) = cp((proc \ es) ∪ {end ?}, gate?) and P (end ?) = cp(proc \ es, end ?) respectively. The semantics of Join is then given by the following process, Briefly, ConnectSplit specifies the constraints on the input exclusive split gateway, ConnectJoin specifies the constraints on the input exclusive join gateway, and Connect specifies the interdependent constraints on the two gateways.

Schema Loop is illustrated by Diagrams 3 and D in Fig. 2. Specificially, Loop performs a two-step operation: 1) replace the end event in the component proc that has incoming sequence flow from? with gateway split? and the end event end ?. The constraints of Loop ensure connect? is one of split?'s outgoing sequence flows, and 2) add a join gateway join? to the component proc. The constraints of Loop ensure that connect? and f 2? are incoming sequence flows of join? and t2? is the outgoing sequence flow of join?. The constraints also ensure that there is an element contained in the before state of proc that has f 2? as one of its incoming sequence flows and replaces this element's f 2? incoming sequence flow with t2?. This element is defined by the expression (µ p : proc | f 2? ∈ in(p) • p) and we let m denote this element.

We let e = end (proc) from?, and ps = (proc \ {e}) ∪ {end ?}. The semantics of split?, join? and end ? are provided by the processes P (split?) = cp(ps, split?), P (join?) = cp(ps, join?) and P (end ?) = cp(ps, end ?) respectively. We also let P (m ) = P (m)[fn(f 2?) ← fn(t2?)], which renames all occurrences of sf (f 2?) to sf (t2?) in P (m). The semantics of Loop is then given by the following process, where OB = i : proc \ {e, m} • ((αP (i) \ {fn(e)}) ∪ {fn(end ?)}) • cp(proc ∪ {end ?}, i).

Fig. 3. Construction of the customer business process

Example Here we describe how to construct the customer business process of our online shop example in Fig. 1. A step-by-step illustration of the business process construction is shown in Figure 3. The following describes the steps shown in the figure .   1. Start with a subprocess' initial state, containing a start and an end events (Step 1); 2. Add an exclusive split gateway using Split (Step 2); 3. Apply SeqComp four times to add three task elements and one subprocess element. The subprocess element is in an initial state, again containing a start and an end events (Steps 3, 4, 5, 6); 4. Apply Split to add an exclusive split gateway inside the subprocess element that was added in the previous step (Step 7); 5. Add two task elements inside the subprocess element using SeqComp two times (Steps 8, 9) and, 6. Join two end elements inside the subprocess element using Join (Step 10).

Analysis

The combination of monotonicity and refinements allows one to verify behavioural correctness of large complex systems incrementally. We would like to show that the operations considered in the previous section to be monotonic with respect to failures refinement ( F ). However, we observe that in general these operations are not monotonic. Consider the BPMN processes in Fig. 4. They are constructed by a combination of operations SeqComp, Split, Join and Loop. We let P 1, P 2, P 3 and P 4 denote the BPMN processes shown in Figs. [START_REF]Formal Systems (Europe) Ltd. Failures-Divergences Refinement, FDR2 User Manual[END_REF](1), ( 2), ( 3) and ( 4) respectively We observe that both P 1 and P 2 deadlock, because in both cases not all of the parallel join gateway's incoming sequence flows can be triggered. Moreover, we observe that P 1 and P 2 admit the same behaviour, that is, P 1 ≡ BPMN P 2. We now consider P 3 and P 4 that are constructed by applying the operation Loop to P 1 and P 2 respectively. We observe that unlike in P 1 and P 2, A can be triggered in both P 3 and P 4. However, after performing A, P 4 can trigger element C , while P 3 cannot. As a result we have P 3 ≡ BPMN P 4. This shows that in general not only the operations are non-monotonic, but more importantly the equivalence ≡ BPMN is not congruent with respect to these operations. To ensure that the operations can be applied monotonically, we assume the following conditions about BPMN diagrams and processes and state that the operations are monotonic with respect to the failures refinement; complete proofs of the following theorems can be found in the author's thesis [START_REF] Wong | Formalisations and Applications of Business Process Modelling Notation[END_REF]Appendix C].

(a) Given any two BPMN pools X , Y : Pool , if we have pToc(X ) F pToc(Y ), then the set of elements X .proc \ Y .proc can be partitioned into two sets A and B :

(i) Each element e ∈ A is either an exclusive split gateway or a subprocess such that there exists an element e ∈ Y .proc \ X .proc where P (e) F P (e ).

(ii) For each element f ∈ B , there exists some exclusive split gateway e ∈ A, such that there exists some element e ∈ Y .proc \ X .proc where P (e) F P (e ). Moreover, ou(e ) ⊂ ou(e) and either in(f ) ⊂ ou(e)\ou(e ) or there exists an element g ∈ B such that in(g) ⊂ ou(e) \ ou(e ) and there exists a sequence of sequence flows connecting g to f . Furthermore, Y .proc \ X .proc can be partitioned into two sets M and N : (iii) For each element m ∈ M , there exists exactly one element e ∈ A such that P (e) F P (m), (iv) Each element e ∈ N is an exclusive join gateway such that there exists an exclusive join gateway f ∈ B with the same outgoing sequence flow and whose set of incoming sequence flows is a superset of e's. Condition (a) is appropriate: according to our process semantics, only exclusive split gateways and subprocesses have nondeterministic behaviour. This condition ensures that when comparing the behaviour of two BPMN processes, every BPMN element from one BPMN process either is related to an element in the other BPMN process via refinement or is only reachable due to nondeterministic behaviour that is removed due to the refinement in the other BPMN process. This condition ensures that there are no hidden behaviour such as element C in Fig. 4 (2). Condition (b) is also appropriate: it is reasonable to compare behaviour of business collaborations if they have the same participants during compositional development. Participants in a business collaboration are typically decided a priori before designing and refining individual processes. These conditions do not reduce the practical expressiveness of BPMN. In particular we have validated the expressiveness via case studies in which we have constructed and verified complex business processes compositionally [START_REF] Wong | Formalisations and Applications of Business Process Modelling Notation[END_REF]Chapter 8].

In general, for any subprocess s, the CSP process that models s's behaviour can be generalised as C [S ] where S is the CSP process that models elements directly contained in s. Here C [.] is a CSP process context that models the incoming, outgoing sequence flows and message flows of s. The following result shows that refinements are preserved from S to C [S ].

Theorem 2. Given any subprocess s satisfying Conditions (a) and (b), and that its behaviour is modelled by CSP process C [S ], where S is the CSP process that models elements contained in s and C [.] is a CSP process context that models s's sequence flows and message flows. Let t be any subprocess whose behaviour is modelled by CSP process C [T ] and T is the CSP process that models elements contained in t. If we have both S F T and C

[S ] F C [T ], then we have C [S ] F C [T ]
where S and T are the results of applying any one of the composition operations on S and T respectively.

A consequence of Theorems 1 and 2 is that refinement is preserved between a subprocess and the BPMN subprocess or pool that contains it. The following result lifts the composition operations to BPMN diagrams, and follows immediately from the fact that the CSP parallel operator is monotonic with respect to refinements.

Corollary 1. Given a BPMN process X that directly contains some subprocess s, such that X 's behaviour is modelled by the CSP process

P (s) |[ αP (s) | αD ]| D,
where D models the behaviour of other elements directly contained in X . For any s such that P (s) F P (s ) we have

P (s) |[ αP (s) | αD ]| D F P (s ) |[ αP (s ) | αD ]| D
Monotonic operations preserve refinement-closed properties. For example, we previously formalized the notion of behavioural compatibility on BPMN pools [START_REF] Wong | Formalisations and Applications of Business Process Modelling Notation[END_REF][START_REF] Wong | Property Specifications for Workflow Modelling[END_REF] as a binary relation compatible(P , Q) on BPMN pools P and Q, such that compatible(P , Q) if and only if P and Q are deadlock free and their collaboration is also deadlock free. We further showed that compatible is a refinement-closed property. As a result, if we let G be one of the composition operations on Pools, if compatible(G(P ), G(Q)), then for all pToc(P ) F pToc(P ) and pToc(Q) F pToc(Q ), compatible(G(P ), G(Q )). Furthermore, due to monotonicity, the equivalence ≡ BPMN defined in Definition 1 is a congruence with respect to the composition operations. A congruence relationship allows one to substitute one part of a BPMN process with another that is semantically equivalent and obtain the same BPMN process.

Receive Offer

(2) Fig. 5. Variants of the customer business process Back to the running example. Fig. 5(1) shows an optimistic version of the customer business process. It is modelled by BPMN pool OpCustomer . After receiving an offer from the online shop, the customer eventually always accepts the offer. Equation 3 defines process OCP that models pool OpCustomer , where for all i ∈ {sCP , s3, s5, s6, s13} process P (i) is defined in Equation 1.

In fact the optimistic customer process is a refinement of the customer process; we verify this by checking the refinement CP F OCP using FDR. Suppose we extend the customer's business process with the following return policy: "After receiving the goods and the invoice, the customer may decide to either keep the goods or return them for repair. Depending on the policy of the online shop, if the customer chooses to return her goods for repair, the shop may either provide a full refund, or repair the goods and deliver them back to the customer. After every repair, the customer has the choice to send the goods back again if further repairs are required.". Fig. 5(2) shows the result of extending the optimistic customer business process with the above return policy. Here we observe that this extension can be constructed by a combination of operations SeqComp, Split and EventSplit, Join and EventLoop. Note that the same combination of operations can be applied to the original customer business process to model this return policy. If we let CP be the resulting CSP process modelling the extended version of CP and OCP be that of OCP , by Theorem 1, we have CP F OCP .

Related Work

Beside the work described in this paper and our earlier work [START_REF] Wong | A Process Semantics for BPMN[END_REF], CSP has been applied to formalize other business process modelling languages. For example Yeung [START_REF] Yeung | Mapping WS-CDL and BPEL into CSP for Behavioural Specification and Verification of Web Services[END_REF] mapped the Web Service Business Process Execution Language (WS-BPEL) and the Web Service Choreography Description Language (WS-CDL) to CSP to verify the interaction of BPEL processes against the WS-CDL description; his approach considers traces refinement and hence only safety properties. There have been attempts to formalize BPMN behaviour using existing formalisms (for example, Dijkman et al. [START_REF] Dijkman | Semantics and analysis of business process models in BPMN[END_REF]), which focus on the semantic definition of BPMN diagrams rather than their construction. Morale et al. [START_REF] Mendoza | Automatic Compositional Verification of Business Processes[END_REF][START_REF] Mendoza Morales | A Formalization Proposal of Timed BPMN for Compositional Verification of Business Processes[END_REF] designed the Formal Composition Verification Approach (FVCA) framework based on an extended timed version of CSP to specify and verify BPMN diagrams. Similar to us, they achieve compositionality by considering the parallel combination of individual business process participants. However, their approach does not consider the semantics of constructing individual BPMN processes. To the best of our knowledge, Istoan's work [START_REF] Istoan | Defining Composition Operators for BPMN[END_REF] is the first attempt at defining composition operations on BPMN. He provided the composition operations to construct a BPMN process by composing two BPMN processes. He also provided these operations with a semantics in terms of Petri Nets [START_REF] Petri | Kommunikation mit Automaten[END_REF]. His notion of refinement is that of functional extension while our work considered the reduction of nondeterminism [START_REF] Eshuis | Comparing refinements for failure and bisimulation semantics[END_REF]. Moreover, Istoan did not consider the semantic property of the composition operations to allow compositional development.

Fig. 1 .

 1 Fig. 1. A running example of a BPMN diagram

  Type ::= start | end | ... to record the type of an element. The free type Element ::= atom Atom | comp Atom × F 1 Element then records individual BPMN elements, where schema Atom = [t : Type; in, ou : F Sflow ; sn, re : F Mflow | in ∩ ou = ∅ ∧ sn ∩ re = ∅] records the type, the sequence flows and the message flows of an element.

  Diagram = [pool : PoolId Pool | pool = ∅]. It states that a diagram consists of one or more BPMN pools, with each pool being uniquely identified by some PoolId value i such that pool (i) gives that pool (where PoolId is a basic type). Similar to Pool , we define InitDiagram = [pool : PoolId Pool | pool = {p1 → proc ; {se, ee} }] to be the initial state of Diagram, where p1 is a PoolId .

1

  A prototypical implementation of the semantic translation can be found at http: //sites.google.com/site/peteryhwong/bpmn

  SeqComp = [∆Pool ; Commons; end ? : Element | #(in new ?) = 1 ∧ #(ou new ?) = 1 ∧ in(end ?) = ou(new ?) ∧ type(end ?) ∈ {end } ∪ ran emsg ∧ #in(end ?) = 1 ∧ #ou(end ?) = 0 ∧ proc = modify(proc, {new ?, end ?}, {ends(proc) from?})] Here SeqComp also declares the following schema Commons: Commons = [Pool ; new ? : Element; from? : Seqflow | (ou(new ?) ∪ sflow (cnt(new ?))) ∩ {e : proc • sflow (cnt(e))} = ∅ ∧ from? ∈ in(new ?) ∧ in(new ?) ⊆ dom(ends proc)]

  OB |[ AB | as({new ?, end ?}) ]| (P (new ?) |[ αP (new ?) | αP (end ?) ]| P (end ?))

  Split = [∆Pool ; Commons; outs? : F 1 Element]

  OB |[ AB | as(outs? ∪ {new ?}) ]| (P (new ?) |[ αP (new ?) | as(outs?) ]| QS ) where OB = i : proc \ {e} • ((αP (i) \ {fn(e)}) ∪ fn(| outs? | )) • cp(proc ∪ outs?, i) and AB = as(proc \ {e}) ∪ fn(| outs? | ). Join The schema Join adds an exclusive join gateway to a BPMN pool. Join = [∆Pool ; gate?, end ? : Element]

  OB |[ AB | as({gate?, end ?}) ]| (P (gate?) |[ αP (gate?) | αP (end ?) ]| P (end ?)) where OB = i : proc \ es • ((αP (i) \ fn(| es | )) ∪ {fn(end ?)}) • cp(proc ∪ {end ?}, i) and AB = (as(proc \ es) \ fn(| es | )) ∪ {fn(end ?)}. Loop The schema Loop adds an exclusive split gateway and an exclusive join gateway to a BPMN pool to construct a loop in the pool. The operation is defined as the conjunction of schemas ConnectSplit, ConnectJoin and Connect, Loop = (ConnectSplit ∧ ConnectJoin ∧ Connect) \ (change, change ) where the declaration of these schemas are shown as follow. ConnectSplit = [Commons[split?/new ?]; connect? : Seqflow ; end ? : Element] ConnectJoin = [Pool ; ch, ch , join? : Element; connect?, f 2?, t2? : Sflow ] Connect = [∆Pool ; from?, f 2?, t2? : Sflow ; ch, ch , split?, join?, end ? : Element]

  OB |[ as(proc \ {e, m}) ∪ {fn(end ?)} | as({split?, join?, end ?, m })]| (P (m ) |[ αP (m ) | as({split?, join?, end ?})]| (P (split?) |[ αP (split?) | as({join?, end ?})]| (P (join?) |[ αP (join?) | αP (end ?) ]| P (end ?))))

Fig. 4 .

 4 Fig. 4. A non-monotonic scenario

  (b) Given any two BPMN diagrams X , Y : Diagram. If we have bToc(X ) F bToc(Y ), we have dom X .pool = dom Y .pool and ∀ i : dom X .pool • pToc(X .pool (i)) F pToc(Y .pool (i)). Theorem 1. Monotonicity. Assuming BPMN diagrams satisfy Conditions (a) and (b), the composition operations are monotonic with respect to F.

Corollary 2 .

 2 Assuming BPMN processes satisfy Conditions (a) and (b), the equivalence ≡ BPMN is a congruence with respect to composition operations.

P

  (s1) = (s.s1 → Skip o 9 (s.s2 → Skip s.s3 → Skip) o 9 P (s1)) 2 c.s14 → Skip OCP = i : {sCP , s1, s3, s5, s6, s13} • αP (i) \ {c.s4} • P (i)

Summary

In this paper we introduced a set of composition operations to construct BPMN diagrams. We provided these operations a CSP semantics, and characterised the conditions under which these operations guarantee monotonicity with respect to F. Refinement-closed properties, such as behavioural compatibility, are preserved by monotonic operations and these operations enable compositional development of business processes.

Acknowledgment We wish to thank Jeremy Gibbons for suggesting improvements to this paper and Stephan Schroevers for proof reading it. We would like to thank anonymous referees for useful suggestions and comments.

Partly funded by Microsoft Research.