BRICS RS-99-56 P. D. Mosses: A Modular SOS for Action Notation BRICS

Basic Research in Computer Science

A Modular SOS for Action Notation

Peter D. Mosses BRICS Report Series RS-99-56 ISSN 0909-0878 December 1999 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1999, Peter D. Mosses.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/99/56/

A Modular SOS for Action Notation ^{⋆}

Peter D. Mosses^{1}

BRICS and Department of Computer Science, University of Aarhus, Denmark

Abstract. Modularity is an important pragmatic aspect of semantic descriptions: good modularity is needed to allow the reuse of existing descriptions when extending or changing the described language. In denotational semantics, the issue of modularity has received much attention, and appropriate abstractions have been introduced, so that definitions of semantic functions may be independent of the details of how computations are modelled. In structural operational semantics (SOS), however, this issue has largely been neglected, and SOS descriptions of programming languages typically exhibit rather poor modularity; the original SOS given for Action Notation (the notation for the semantic entities used in action semantics) suffered from the same problem. This paper recalls a recent proposal, called MSOS, for obtaining a high degree of modularity in SOS, and presents an MSOS description of Action Notation. Due to its modularity, the MSOS description pin-points some complications in the design of Action Notation, and should facilitate the design of an improved version of the notation. It also provides a major example of the applicability of the MSOS framework. The reader is assumed to be familiar with conventional SOS and with the basic concepts and constructs of Action Notation. The description of Action Notation is formulated almost entirely in Casl, the common algebraic specification language.

1 Background

This section recalls the main features of MSOS [11], Casl [3, 9], and Action Notation [7]. Subsequent sections introduce and discuss the MSOS of Action Notation, which is provided in the appendices.

1.1 Modular SOS

Conventional SOS [1, 15] involves abstract syntax, computed values, configurations (some of which may be distinguished as terminal), and inference rules for (labelled) transitions. An SOS specifies a labelled transition system (Γ , T , 𝔸, →), where Γ is the set of configurations, T ⊆ Γ is the set of terminal configurations,

⋆ Full version of [13], reporting research carried out while visiting SRI International and Stanford University, USA

𝔸 is the set of labels, and → ⊆ Γ × 𝔸 × Γ is the transition relation. For configurations γ, γ′ ∈ Γ and labels α ∈ 𝔸, the assertion that (γ, α, γ′) is in the transition relation is written γ ⟶^{α} γ′.

Modular SOS, abbreviated MSOS [11], is a particularly simple and uniform discipline of SOS with the following features:

– Configurations γ ∈ Γ are restricted to abstract syntax trees (where nodes may be replaced by the values that they have computed, as in conventional SOS).

– Initial configurations are pure syntax, and terminal configurations are simply computed values.

– All the usual semantic components of configurations (such as environments and stores) are incorporated in the labels α ∈ 𝔸 on transitions.

– The labels on transitions are equipped with a partial composition operation, written α ; α′ (associative whenever the composition is defined), and each label can always be composed on the left and right with identity labels ι ∈ 𝕀[𝔸]. The labels α ∈ 𝔸 are considered to be the arrows of a category, also written 𝔸. The objects o ∈ 𝕆[𝔸] of the category correspond to the usual semantic components of configurations; let us refer to them as states.

– Transitions γ_{1} ⟶^{α_{1}} γ′_{1} and γ_{2} ⟶^{α_{2}} γ′_{2} may be adjacent in a computation only when γ′_{1} = γ_{2} and moreover the composition α_{1} ; α_{2} of their labels is defined.

– The actual representation of the labels α is abstracted from the rules that define the transition relations, allowing the former to be changed without invalidating the latter.

1.2 Label Categories

Label categories are defined succinctly using three standard label transformers, which correspond to some simple monad transformers. The following three label transformers, enriching label categories with further labels and states, are fundamental:

– Context Info adds an extra component of a particular sort both to labels and to states, and its value is preserved by the pre and post operations. The composition α; α′ is defined only when the new component has the same value in both α and α′, and the composition preserves that value. This transformer is typically used for dealing with environments.

– Mutable Info adds an extra component to states, and a pair of extra components (of the same sort) to labels, corresponding to the components of their pre and post states. The composition α; α′ is defined only when this component has the same value in both post(α) and pre(α′). This transformer is typically used for dealing with stores.

– Emitted Info adds an extra component only to labels. The composition α; α′ combines the values of this component in α and α′ using the operations of a given monoid. This transformer is typically used for dealing with output, the given monoid then being sequences with their concatenation.

The notation associated with the above label transformers is specified generically in Casl in Appendix B. It includes the operations set, for initializing or overwriting a particular component of a label or state, and get, for returning the value of a particular component (or a default value, if that component has not been set). Also the operations get pre and set post are provided in the case of Mutable Info, to avoid having to deal with pairs explicitly.

1.3 Casl Specifications

For defining abstract syntax, values, configurations, the notation used for labels, and transition relations, it is convenient to use Casl, the Common Algebraic Specification Language [3, 9]. Casl is quite expressive, providing direct support for specifying sort inclusions, partial operations, predicates, definedness assertions, and first-order axioms. Casl also provides datatype declarations (resembling grammars in BNF) that allow sorts equipped with constructors and selectors to be specified concisely. For structuring specifications, Casl provides union, extension, free extension (with initiality as a special case) and generic specifications. Casl does not allow the specification of inference rules for transitions, but we may write SOS transition rules as implications in Casl; the least relation satisfying the implications is obtained by letting the specification of transitions be a free extension.

Action Notation incorporates Data Notation [7, App. E], which provides various familiar datatypes: truth-values, numbers, characters, strings, lists, trees, sets, and finite maps, as well as some that are more closely connected with actions: data tuples, bindings, tokens, stores, cells, and agents. Data Notation is specified algebraically in the framework of Unified Algebras [5, 6]. Action Notation does not depend on the way that data is specified, except that a few primitive actions and yielders do require sorts of data as arguments (e.g., the action written ‘choose natural’ gives an arbitrary element of the sort natural), which is not allowed by Casl . To specify Data Notation in Casl, sorts that are to be used as arguments have to be represented by ordinary constants (or terms).

In fact the unified algebra treatment of sorts as values in a universe Univ can easily be simulated in Casl by distinguishing a subsort of ‘individual’ values Indiv < Univ, and declaring suitable operations and relations on Univ. The constant nothing : Univ corresponds to an empty subsort of Univ. The unified algebra operations of sort union | and intersection & are provided as ordinary operations on Univ, whereas the unified algebra subsort inclusion ≤ and individual inclusion :< ^{1} are simply binary predicates in Casl. The predicate u :< s holds iff the value u is both in Indiv and in the subsort represented by the value s. For instance, the unified algebra sort data is represented in Casl by declaring the subsorts Data < Indiv and DataSort < Univ, and the constant data : DataSort, with d : Data ⟺ d :< data. The full properties of the general unified algebra notation are specified in Casl in Appendix C.

1 The unified algebra notation ‘ : ’ cannot be declared as a symbol in Casl.

Furthermore, Casl specifications of various basic abstract datatypes have recently been proposed [16], subsuming much of the standard Data Notation.

Therefore we may employ Casl for specifying both Action Notation (operationally, in the MSOS style) and Data Notation (algebraically), and avoid any direct involvement of the Unified Algebras framework in the foundations of Action Semantics.

The only feature of Action Notation that cannot be specified directly in (firstorder) Casl is that all data operations are supposed to be implicitly extended to yielder arguments. Here, we give a schematic specification of this lifting; a fully formal treatment would involve the use of higher-order Casl [4].

1.4 Action Notation

Action Notation is a rich algebraic notation for expressing actions, which are used (along with data, and ‘yielders’ of data) to represent the semantics of constructs of conventional programming languages. Actions are essentially dynamic, computational entities. The performance of an action directly represents information processing behaviour and reflects the gradual, step-wise nature of computation: each step of an action performance may access and/or change the current information. Yielders occurring in actions may access, but not change, the current information. The evaluation of a yielder always results in a data entity (including a special entity used to represent undefinedness). For example, a yielder might always evaluate to the datum currently stored in a particular cell, which could change during the performance of an action, and become undefined when the cell is freed.

A performance of an action either: completes, corresponding to normal termination; or escapes, corresponding to exceptional termination; or fails, corresponding to abandoning an alternative; or diverges.

Action notation consists of several rather independent parts, corresponding to the following so-called ‘facets’ of information processing:

Basic: for specifying the flow of control in actions; Functional: for specifying the flow of the data that are given to and by actions; Declarative: for specifying the scopes of the bindings that are received and

produced by actions; Reflective: for specifying procedural abstraction and application; Imperative: for specifying the allocation of storage for the values of variables;

and Communicative: for specifying (asynchronous) message passing.

Compound actions are formed from primitive actions and action combinators. Each primitive action is single-faceted, affecting information in only one facet—although any yielders that it contains may refer to all kinds of information. An action combinator determines control and information flow for each facet of the combined actions, allowing the expression of multi-faceted actions, such as an action that both (imperatively) reserves a cell of storage and then (functionally) gives the identity of the reserved cell. For instance, one combinator determines left-to-right sequencing together with left-to-right transient data flow, but letting the received bindings flow to its sub-actions; another combinator differs from that only regarding data flow: it concatenates any transients that the sub-actions give when completing, not passing transients between the actions at all. Some selections of control and information flow are disallowed, e.g., interleaving together with transient data flow between the interleaved sub-actions. In particular, imperative and communicative information processing always follows the flow of control.

Further informal explanation of the design of Action Notation may be found in the main sources for action semantics [7, 8, 17].

2 Introduction to the MSOS of Action Notation

The intended interpretation of Action Notation was originally defined [7, App. C] using a rather unorthodox style of SOS, exploiting the novel algebraic specification framework of Unified Algebras [5, 6]. The main features of unified algebras are that operations can be applied to, and return, entire sorts, and that individual values are regarded as singleton sorts. Transition relations can thus be represented as functions that map individual configurations to entire sorts of configurations (representing the sets of alternative transitions).

Unfortunately, the unorthodox style of the original SOS of Action Notation, combined with the unfamiliarity of Unified Algebras, made the specification somewhat inaccessible. Its lack of modularity also meant that even minor changes to Action Notation (or extensions of it, such as the proposal to allow agents to share storage [14]) might require a major reformulation of the given SOS. Moreover, to decrease the size of the description, the full Action Notation was reduced to a substantially-smaller kernel notation (by means of algebraic equations), and only the latter was given a direct operational semantics.

Appendix A of this paper gives an MSOS for all of Action Notation. It is structured in much the same way as [7, Apps. B and D], describing the various facets of Action Notation in turn; however, the semantics of each construct is here specified directly, without resort to an intermediate kernel notation.

Each section of the MSOS specifies the data notation, abstract syntax, computed values, configurations, label notation, and transition rules for the action notation in the facet concerned. The following explanatory comments apply to all the sections.

2.1 Data

Data notation is specified by reusing abstract datatypes that are already available, perhaps with renaming or instantiation of generic specifications and adding declarations and axioms for new notation. For instance: spec Basic Data = Truth Values

with Truth Value, true value, false value, either and

sorts Data < Indiv; DataSort < Univ

The symbols listed above after ‘with’ are assumed to be declared by the Casl specification of Truth Values (which uses slightly different identifiers than those in [7, App. E], to avoid confusion with the reserved Casl predicate symbols true and false). Many of the symbols of Data Notation are not valid Casl symbols, but generally become so once internal spaces and hyphens have been replaced by underscores.

As mentioned earlier, it is envisaged that the standard Data Notation used in Action Semantics may be replaced by a library of Casl specifications, perhaps incorporating the basic Casl datatype specifications that have recently been proposed [16].

By the way, only the data notation actually needed for the MSOS of Action Notation is specified in Appendix C. In particular, the declarations of constants such as data : DataSort, representing proper sorts in unified algebras, are omitted, since assertions such as d :< data can be expressed equivalently as d ∈ Data, and ds ≤ data as ds ∈ DataSort.

2.2 Syntax

Abstract syntax is specified in Casl using a datatype declaration, which resembles a BNF-like grammar. Mixfix notation is allowed—for instance, the following fragment specifies and as an infix operation:

spec Basic Syntax = Basic Data then

types

Action ::= … | and (Action; Action) | …;
Yielder ::= … | sort DataSort | …

The abstract syntax for actions and yielders extends the associated data notation, and data components are regarded as already evaluated.

It is possible to specify a syntactic congruence by adding axioms to the given datatype declarations, for instance asserting that A_{1} and A_{2} = A_{2} and A_{1} , thereby reducing the need for various symmetric pairs of inference rules when specifying the transition relation.

By the way, several of the words used in Action Notation, such as ‘and’, are reserved keywords in Casl, and cannot be complete tokens in Casl input symbols. So-called display annotations (not shown here) allow them to be produced in the formatted specification (using a distinct font, as in ‘and ’, to avoid confusion between symbols and keywords).

One might expect the types for the abstract syntax of actions and yielders for each facet of Action Notation to be specified as ‘free’, to ensure that there can be no syntactic ‘junk’ (i.e., all syntactic values can be expressed by the declared constructors) nor ‘confusion’ (i.e., different terms denote different syntactic values, up to syntactic congruence) in models of the specification. However, that would prevent the subsequent combination of facets (as well as the extension of abstract syntax to configurations, see below). Instead, a free extension is specified after the facets have been combined.

2.3 Outcomes

The values that may be computed by action performance (and yielder evaluation) are specified algebraically in Casl, by declaring sorts, operations, and predicates, and asserting their essential properties. The specifications often use datatype declarations for conciseness. For instance:

spec Functional Outcomes = Basic Outcomes and Functional Data then

types

Terminated ::= sort Completed | …;
Completed ::= completed | gave(Data)

axioms

%[1] gave(none) = completed;

…

2.4 Configurations

The ‘value-added’ syntax used for configurations is specified simply by adding further alternatives for the datatype declarations which specified abstract syntax: for each sort of the abstract syntax, the sort of value computed by elements of that sort is included as a subsort. Auxiliary syntactic constructs for use in configurations may be added here too.

In fact the configurations for non-distributed action performance are always the same, as specified by:

spec Basic Configurations = Basic Syntax and Basic Outcomes then

type Action ::= sort Terminated | @ (Action; Action)

The sort Terminated (of values computed by actions) depends on the facet. (The auxiliary construct A_{1} @ A_{2} is used only in the basic facet, in connection with unfolding.)

The distributed performance of communicative actions by separate agents is described by embedding Action in an auxiliary sort of configurations, Processing, which allows collections of agents (with their actions), pending messages, and contracts all to be composed in parallel.

The datatype declaration for Action above augments the constructors for this sort, which is left loosely specified in Basic Syntax.

2.5 Labels

Each facet of Action Notation generally requires the transformation of the category of labels 𝔸 to include one or more further components. This is specified concisely in Casl by instantiating one of the generic specifications corresponding to the three fundamental kinds of enrichment described in Section 1.2. For example, the functional facet specifies:

spec Functional Labels = Basic Labels and Functional Data then Context Info

[ sort 𝔸 ] [ op data : Index ]

[ sort Data < ContextInfo op none : Data ]

which defines the operation set(α, data, d) to return a label α′ with data component d, and the operation get(α, data) to return the data component of d, if defined (otherwise none).^{2} The values of sort Index (such as data) may be thought of as selection indices; their only property is that different constants denote distinct values.

The fitting morphisms from the parameter specifications of Context Info to the argument specifications above are uniquely determined, and may therefore be left implicit.

2.6 Transitions

Transition rules are of three main kinds:

– Rules that allow performance of a compound construct to start (or continue) with a particular sub-construct: a transition for the sub-construct gives rise to a transition for the enclosing construct, often with the same unrestricted label α. For instance, the following rules allow interleaved performance of A_{1} and A_{2} :

A_{1} ⟶^{α} A′_{1} %%  %% ⇒

A_{1} and A_{2} ⟶^{α} A′_{1} and A_{2} ;

A_{2} ⟶^{α} A′_{2} %%  %% ⇒

A_{1} and A_{2} ⟶^{α} A_{1} and A′_{2} (The line between the conditions and the conclusion is not part of Casl notation, and has to be enclosed in comment signs ‘%%’.)

– Rules that specify the computation of a value by an atomic construct: the label on the transition is generally well-determined by the current state. For instance, the following rule lets the value computed by regive depend on the current state, which is not changed by the identity ι:

2 set(α, data, d) might be written even more suggestively as α[data := d], and get(α, data) as α.data.

d = get(ι, data)

%%  %% ⇒

regive ⟶^{ι} gave(d)

– Rules that reduce a compound configuration: once one or more components of a compound construct have computed values, the construct may be ‘silently’ reduced to a single computed value or syntactic component, the label on the transition being an identity ι. For instance, the following rule combines the values computed by performing the sub-actions of A_{1} and A_{2} :

gave(d_{1} ) and gave(d_{2} ) ⟶^{ι} gave(concatentation(d_{1} , d_{2} ))

An action is regarded as ‘incorrect’ when its performance can get stuck, i.e., lead to a configuration (other than a computed value) from which there is no further transition. For example, the action ‘check abstraction of A’ is incorrect, since transitions are possible for ‘check tv’ only when tv ∈ Truth Value. The question of whether or not an arbitrary action is ‘correct’ is undecidable; a static semantics using type inference for action notation could however provide a useful decidable safe approximation to this notion.

The mathematical nature of the evaluation of yielders to data (sorts or individuals) is reflected by the labels on the transitions always being identities ι:

Y ⟶^{ι} ds.

In general, the evaluation of yielders in a primitive action may be done in any order, and the result is independent of the chosen order. (Primitive actions are supposed to be indivisible, so a small-step gradual evaluation of yielder arguments would be incorrect.)

The ordinary transitive closure ⟶^{α}^{+} of ⟶^{α} is used in the rule for indivisible actions; its inductive definition is standard:

A ⟶^{α} A′ %%  %% ⇒

A ⟶^{α}^{+} A′

A ⟶^{α′} A′ ∧ A′ ⟶^{α′′}^{+} A′′ ∧ α = α′; α′′ %%  %% ⇒

A ⟶^{α}^{+} A′′

It is occasionally convenient to abbreviate two rules with the same conclusion by use of a single rule that has a disjunction of conditions. (Casl requires the intended grouping of a mixture of conjunctions and disjunctions to be made explicit, so there can be no doubt about the expansion of such an abbreviated rule.)

3 Discussion

The full MSOS of Action Notation is about 25 pages long, which is roughly twice as long as the original SOS for the kernel of Action Notation. The main reason for this expansion is not so much the difference in size between the kernel and full Action Notation, but more that the author went to great pains to achieve brevity in the original SOS. For instance, various subsorts that corresponded to restrictions of the original grammar were used—such subsorts are easy to express with the sort union operation of unified algebras. Auxiliary operations, effecting internal simplifications of the configuration, were introduced. Each combinator was classified into subsorts, e.g., according to whether it was sequential or interleaving; this allowed transitions to be specified for many combinators at once, rather concisely. Although such techniques might also be applicable in the MSOS of Action Notation, they would tend to undermine its modularity, and make it more difficult to cut down the description when removing entire facets.

The main hope for reducing the size of the MSOS of Action Notation is by means of a substantial simplification of Action Notation during the current reconsideration of its design. For instance, it appears that there is not much use for actions that simultaneously give some transient data and produce some bindings; eliminating them would allow all the hybrid combinators to be removed, and reduce the size of the MSOS of Action Notation by about 10%. The high degree of modularity of MSOS facilitates pin-pointing just which Action Notation constructs are excessively complicated.

It is hoped that the MSOS of Action Notation is much easier to follow than the original SOS—once one has grasped how dependencies between labels determine the flow of processed information, that is. (Readers who have difficulty with this aspect of MSOS might like to contemplate the reduction of MSOS to SOS [11] by moving the pre and post components of the labels to the configurations.)

Given the good modularity properties of MSOS, one might ask which is better: to describe the operational semantics of a programming language directly, using MSOS, or indirectly, using Action Semantics? In the author’s opinion, it is generally better to use Action Semantics, for the following reasons.

The main advantage of the Action Semantics approach over MSOS is that the combinators of Action Notation provide concise abbreviations for particular patterns of MSOS (or SOS) transition rules. For instance, the combinator for sequential action performance without data-flow (written A_{1} and then A_{2} ) abbreviates the pattern of transitions that occurs in many (M)SOS rules for left-to-right evaluation. A further advantage would show up in connection with the description of ML-style exceptions: Action Notation provides the escape primitive for escaping from normal action performance (with a value), and the combinator A_{1} trap A_{2} for trapping such escapes; in (M)SOS, the propagation of the exception value through all the syntactic constructs—apart from the exception handler—has to be specified explicitly.

However, MSOS also has some advantages over Action Semantics. Perhaps the main one is that the only unfamiliar notation provided by MSOS is that for the label transformers, whereas the full standard Action Notation is quite rich, and becoming familiar with it requires a significant initial investment of effort. Another stems from the very generality of the full Action Notation: its equational theory is too weak to be of much practical use. With MSOS, one may be able to prove stronger properties, exploiting awareness of the exact patterns of transitions and configurations that can arise.

Finally, for practical large-scale use of semantic descriptions, tool support is just as crucial as good modularity. Various tools have already been developed for Action Semantics (see other papers in this volume), whereas implementation of tools for MSOS is only just starting.

Those who have grown attached to the expressiveness provided by the framework of Unified Algebras may regret the switch to the more orthodox algebraic specification language Casl; indeed, the author himself has somewhat mixed feelings about abandoning this major application of the Unified Algebras framework, despite the ease with which it can be simulated in Casl . However, the adoption of Casl should not only increase the accessibility of Action Notation (by removing the need to learn first about Unified Algebras), but also it should pave the way for future exploitation of Casl libraries of standard abstract datatypes, and of Casl-based interfaces to existing tools (such as theoremprovers), in connection with action-semantic descriptions. The author was in any case happy to discover that Casl, itself originally designed for algebraic specification and development of software, appears to be quite well-suited also as a meta-notation for MSOS and for Action Semantics.

Acknowledgements Thanks to Christiano Braga, Søren B. Lassen and Carolyn Talcott for comments on earlier versions of the MSOS of Action Notation. The author is supported by BRICS (Centre for Basic Research in Computer Science), established by the Danish National Research Foundation in collaboration with the Universities of Aarhus and Aalborg, Denmark; by an International Fellowship from SRI International; and by DARPA-ITO through NASA-Ames contract NAS2-98073.

References

1. E. Astesiano. Inductive and operational semantics. In E. J. Neuhold and M. Paul, editors, Formal Description of Programming Concepts, IFIP State-of-the-Art Report, pages 51–136. Springer-Verlag, 1991.

2. CoFI. The Common Framework Initiative for algebraic specification and development, electronic archives. Notes and Documents accessible from http://www.brics.dk/Projects/CoFI.

3. CoFI Language Design Task Group. Casl – The CoFI Algebraic Specification Language – Summary. Documents/CASL/Summary, in [2], Oct. 1998.

4. A. Haxthausen, B. Krieg-Brückner, and T. Mossakowski. Subsorted partial higherorder logic as an extension of Casl. Note L-10, in [2], Oct. 1998.

5. P. D. Mosses. Unified algebras and institutions. In LICS’89, Proc. 4th Ann. Symp. on Logic in Computer Science, pages 304–312. IEEE, 1989.

6. P. D. Mosses. Unified algebras and modules. In POPL’89, Proc. 16th Ann. ACM Symp. on Principles of Programming Languages, pages 329–343. ACM, 1989.

7. P. D. Mosses. Action Semantics. Number 26 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992.

8. P. D. Mosses. Theory and practice of action semantics. In MFCS ’96, Proc. 21st Int. Symp. on Mathematical Foundations of Computer Science (Cracow, Poland, Sept. 1996), volume 1113 of LNCS, pages 37–61. Springer-Verlag, 1996.

9. P. D. Mosses. CASL: A guided tour of its design. In J. L. Fiadeiro, editor, Recent Trends in Algebraic Development Techniques, Proceedings, volume 1589 of LNCS. Springer-Verlag, 1999.

10. P. D. Mosses. Foundations of modular SOS. Research Series BRICS-RS-99-54, BRICS, Dept. of Computer Science, Univ. of Aarhus, 1999. http://www.brics. dk/RS/99/54. Full version of [11].

11. P. D. Mosses. Foundations of Modular SOS (extended abstract). In MFCS’99, Proc. 24th Intl. Symp. on Mathematical Foundations of Computer Science, Szklarska-Poreba, Poland, volume 1672 of LNCS, pages 70–80. Springer-Verlag, 1999. Full version available [10].

12. P. D. Mosses. A modular SOS for Action Notation. Research Series BRICS-RS-99-56, BRICS, Dept. of Computer Science, Univ. of Aarhus, 1999. http://www. brics.dk/RS/99/56. Full version of [13].

13. P. D. Mosses. A modular SOS for Action Notation (extended abstract). In P. D. Mosses and D. A. Watt, editors, AS’99, Proc. Second International Workshop on Action Semantics, Amsterdam, The Netherlands, number NS-99-3 in Notes Series, pages 131–142, BRICS, Dept. of Computer Science, Univ. of Aarhus, May 1999. Full version available [12].

14. P. D. Mosses and M. A. Musicante. An action semantics for ML concurrency primitives. In FME’94, Proc. Formal Methods Europe: Symposium on Industrial Benefit of Formal Methods, Barcelona, volume 873 of LNCS, pages 461–479. Springer-Verlag, 1994.

15. G. D. Plotkin. A structural approach to operational semantics. Lecture Notes DAIMI FN–19, Dept. of Computer Science, Univ. of Aarhus, 1981.

16. M. Roggenbach and T. Mossakowski. Basic datatypes in Casl. Note L-12, in [2], Nov. 1999.

17. D. A. Watt. Programming Language Syntax and Semantics. Prentice-Hall, 1991.

%[Appendix A] library Action Notation

%% The specification Basic Syntax below is formulated schematically, %% which is not allowed in Casl.

from Label Categories %% Appendix B get Context Info, Mutable Info, Emitted Info

from Data Notation %% Appendix C get Tuples, Truth Values, Numbers, Lists, Sets, Maps, Data Notation

%% A.1 The Basic Facet

spec Basic Data =

Truth Values

with Truth Value, true value, false value, either and

sorts Data < Indiv; DataSort < Univ

spec Basic Syntax =

Basic Data then types

Action ::= or (Action; Action) | fail | commit | and (Action; Action) | complete | indivisibly (Action) | and then (Action; Action) | trap (Action; Action) | escape | unfolding (Action) | unfold | diverge

Yielder ::= the yielded by (DataSort; Yielder) | sort DataSort | data op(Yielder; …; Yielder)

%% The schematic alternative data op(Yielder; …; Yielder) %% stands for a set of alternatives, one for every declared %% operation data op on DataSort.

spec Basic Outcomes =

Basic Data and type Terminated ::= completed | escaped | failed

spec Basic Configurations = Basic Syntax and Basic Outcomes then

type Action ::= sort Terminated | @ (Action; Action) spec Basic Labels =

Basic Syntax then Context Info

[ sort 𝔸 ] [ op unfolding : Index ] [ sort Action < ContextInfo op fail : Action ]

then Emitted Info

[ sort 𝔸 ] [ op commitment : Index ] [ Truth Values fit default ↦ false value, combine ↦ either ]

spec Basic Transitions = Basic Configurations and Basic Labels then

pred ⟶ : Action × 𝔸 × Action

vars α, α′ : 𝔸; ι : 𝕀[𝔸];

A, A_{0} , A_{1} , A_{2} , A′, A′_{1} , A′_{2} : Action; t : Terminated axioms

%[1] A_{1} ⟶^{ι} A′_{1} %%  %% ⇒

A_{1} or A_{2} ⟶^{ι} A′_{1} or A_{2} ;

%[2] A_{2} ⟶^{ι} A′_{2} %%  %% ⇒

A_{1} or A_{2} ⟶^{ι} A_{1} or A′_{2} ;
%[3]  fail ⟶^{ι} failed;
%[4]  completed or A_{2} ⟶^{ι} completed;
%[5]  A_{1} or completed ⟶^{ι} completed;
%[6]  escaped or A_{2} ⟶^{ι} escaped;
%[7]  A_{1} or escaped ⟶^{ι} escaped;
%[8]  failed or A_{2} ⟶^{ι} A_{2} ;
%[9]  A_{1} or failed ⟶^{ι} A_{1} ;

%[10]

A_{1} ⟶^{α} A′_{1} ∧ get(α, commitment) = true value
%%  %% ⇒

A_{1} or A_{2} ⟶^{α} A′_{1} ;

%[11]

A_{2} ⟶^{α} A′_{2} ∧ get(α, commitment) = true value
%%  %% ⇒

A_{1} or A_{2} ⟶^{α} A′_{2} ;

%[12]

α = set(ι, commitment, true value)

%%  %% ⇒

commit ⟶^{α} completed;

%[13] A_{1} ⟶^{α} A′_{1} %%  %% ⇒

A_{1} and A_{2} ⟶^{α} A′_{1} and A_{2} ;

%[14] A_{2} ⟶^{α} A′_{2} %%  %% ⇒

A_{1} and A_{2} ⟶^{α} A_{1} and A′_{2} ;
%[15]  complete ⟶^{ι} completed;
%[16]  completed and completed ⟶^{ι} completed;
%[17]  escaped and A_{2} ⟶^{ι} escaped;
%[18]  A_{1} and escaped ⟶^{ι} escaped;
%[19]  failed and A_{2} ⟶^{ι} failed;
%[20]  A_{1} and failed ⟶^{ι} failed;

%[21] A ⟶^{α}^{+} t %%  %% ⇒

indivisibly A ⟶^{α} t;

%[22] A_{1} ⟶^{α} A′_{1} %%  %% ⇒

A_{1} and then A_{2} ⟶^{α} A′_{1} and then A_{2} ;

%[23] A_{2} ⟶^{α} A′_{2} %%  %% ⇒

completed and then A_{2} ⟶^{α} completed and then A′_{2} ;

%[24]  completed and then completed ⟶^{ι} completed;
%[25]  completed and then escaped ⟶^{ι} escaped;
%[26]  completed and then failed ⟶^{ι} failed;
%[27]  escaped and then A_{2} ⟶^{ι} escaped;
%[28]  failed and then A_{2} ⟶^{ι} failed;

%[29] A_{1} ⟶^{α} A′_{1} %%  %% ⇒

A_{1} trap A_{2} ⟶^{α} A′_{1} trap A_{2} ;
%[30]  escape ⟶^{ι} escaped;
%[31]  escaped trap A ⟶^{ι} A;
%[32]  completed trap A_{2} ⟶^{ι} completed;
%[33]  failed trap A_{2} ⟶^{ι} failed;
%[34]  unfolding A ⟶^{ι} A @ A;
%[35]  t @ A_{0} ⟶^{ι} t;

%[36]

α′ = set(α, unfolding, A_{0} ) ∧ A ⟶^{α′} A′
%%  %% ⇒

A @ A_{0} ⟶^{α} A′ @ A_{0} ;

%[37]

get(ι, unfolding) = A_{0}

%%  %% ⇒

unfold ⟶^{ι} A_{0} ;

%[38]  diverge ⟶^{ι} diverge ;

pred ⟶ : Yielder × 𝕀[𝔸] × DataSort
vars Y : Yielder; d : Data; ds : DataSort

axioms

%[39] Y ⟶^{ι} d ∧ d :< ds %%  %% ⇒

the ds yielded by Y ⟶^{ι} d;

%[40] Y ⟶^{ι} d ∧ ¬(d :< ds) %%  %% ⇒

the ds yielded by Y ⟶^{ι} nothing;

%[41]

Y ⟶^{ι} nothing
%%  %% ⇒

the ds yielded by Y ⟶^{ι} nothing;

%[42] %% For each n-ary data op, the rule:

Y_{1} ⟶^{ι} ds_{1} ∧ ⋯ ∧ Y_{n} ⟶^{ι} ds_{n} ∧

ds = data op(ds_{1} , …, ds_{n})

%%  %% ⇒

data op(Y_{1} , …, Y_{n}) ⟶^{ι} ds

%% A.2 The Functional Facet

spec Functional Data

Tuples [ sort Datum ]

with Tuple[Datum] ↦ Data, none, concatenation, nth and Numbers with Positive

spec Functional Syntax = Basic Syntax and Functional Data then

types

Action ::= give (Yielder) | regive | choose (Yielder) | check (Yielder) | then (Action; Action) | escape with (Yielder);

Yielder ::= it | them | given (DataSort) | given # (DataSort; Positive)

spec Functional Outcomes = Basic Outcomes and Functional Data then

types

Terminated ::= sort Completed | sort Escaped;
Completed ::= completed | gave(Data);
Escaped ::= escaped | escape gave(Data)

axioms %[1] gave(none) = completed; %[2] ¬(escape gave(none) = escaped) spec Functional Labels =

Basic Labels and Functional Data then Context Info

[ sort 𝔸 ] [ op data : Index ]

[ sort Data < ContextInfo op none : Data ]

spec Functional Transitions = Basic Transitions and Functional Syntax and Functional Outcomes and Functional Labels then

vars α, α′ : 𝔸; ι : 𝕀[𝔸];

A, A_{1} , A_{2} , A′, A′_{1} , A′_{2} : Action; Y : Yielder;

t_{1} , t_{2} : Terminated; c_{1} , c_{2} : Completed; e_{1} , e_{2} : Escaped; d, d_{1} , d_{2} : Data; ds : DataSort; p : Positive

axioms

%[1] Y ⟶^{ι} d %%  %% ⇒

give Y ⟶^{ι} gave(d);

%[2]

Y ⟶^{ι} nothing

%%  %% ⇒

give Y ⟶^{ι} failed;

%[3]

d = get(ι, data)

%%  %% ⇒

regive ⟶^{ι} gave(d);

%[4] Y ⟶^{ι} ds ∧ d :< ds %%  %% ⇒

choose Y ⟶^{ι} gave(d);

%[5]

Y ⟶^{ι} nothing

%%  %% ⇒

choose Y ⟶^{ι} failed;

%[6]

Y ⟶^{ι} true value

%%  %% ⇒

check Y ⟶^{ι} gave(none);

%[7]

Y ⟶^{ι} false value ∨ Y ⟶^{ι} nothing
%%  %% ⇒

check Y ⟶^{ι} failed;

%[8]  c_{1} or A_{2} ⟶^{ι} c_{1} ;
%[9]  A_{1} or c_{2} ⟶^{ι} c_{2} ;
%[10]  e_{1} or A_{2} ⟶^{ι} e_{1} ;
%[11]  A_{1} or e_{2} ⟶^{ι} e_{2} ;
%[12]  e_{1} and A_{2} ⟶^{ι} e_{1} ;
%[13]  A_{1} and e_{2} ⟶^{ι} e_{2} ;
%[14]  e_{1} and then A_{2} ⟶^{ι} e_{1} ;
%[15]  c_{1} and then e_{2} ⟶^{ι} e_{2} ;
%[16]  gave(d_{1} ) and gave(d_{2} ) ⟶^{ι} gave(concatentation(d_{1} , d_{2} ));
%[17] gave(d_{1} ) and then gave(d_{2} ) ⟶^{ι} gave(concatentation(d_{1} , d_{2} ));

%[18] A_{1} ⟶^{α} A′_{1} %%  %% ⇒

A_{1} then A_{2} ⟶^{α} A′_{1} then A_{2} ;

%[19]

α′ = set(α, data, d_{1} ) ∧ A_{2} ⟶^{α′} A′_{2}
%%  %% ⇒
gave(d_{1} ) then A_{2} ⟶^{α} A′_{2} ;
%[20]  gave(d_{1} ) then c_{2} ⟶^{ι} c_{2} ;
%[21]  c_{1} then e_{2} ⟶^{ι} e_{2} ;
%[22]  e_{1} then A_{2} ⟶^{ι} e_{1} ;
%[23]  c_{1} then failed ⟶^{ι} failed;
%[24]  failed then A_{2} ⟶^{ι} failed;

%[25] Y ⟶^{ι} d %%  %% ⇒

escape with Y ⟶^{ι} escape gave(d);

%[26]

Y ⟶^{ι} nothing
%%  %% ⇒

escape with Y ⟶^{ι} failed;

%[27]

α′ = set(α, data, d_{1} ) ∧ A_{2} ⟶^{α′} A′_{2}
%%  %% ⇒
escape gave(d_{1} ) trap A_{2} ⟶^{α} A′_{2} ;
%[28]  e_{1} trap t_{2} ⟶^{ι} t_{2} ;
%[29]  c_{1} trap A_{2} ⟶^{ι} c_{1} ;
%[30]  failed trap A_{2} ⟶^{ι} failed;

%[31]

d = get(ι, data) ∧ d :< datum

%%  %% ⇒

it ⟶^{ι} d;

%[32]

d = get(ι, data)

%%  %% ⇒

them ⟶^{ι} d;

%[33]

d = get(ι, data) ∧ d :< ds

%%  %% ⇒
given ds ⟶^{ι} d;

%[34]

d = nth(get(ι, data), p) ∧ d :< ds

%%  %% ⇒
given ds#p ⟶^{ι} d;

%% A.3 The Declarative Facet

spec Declarative Data =

Maps [ sort Token ] [ free type Range ::= sort Bindable | unknown ] with Map[Token, Range] ↦ Bindings, empty map, map of to , at , overlay, disjoint union, mapped set

and Sets [ sort Token ]

with Set[Token], empty set, set of , is in

spec Declarative Syntax = Basic Syntax and Declarative Data then

types

Action ::= bind to (Yielder; Yielder) | rebind | unbind (Yielder) | produce (Yielder) | furthermore (Action) | moreover (Action; Action) | hence (Action; Action) | before (Action; Action);

Yielder ::= current bindings | the bound to (DataSort; Yielder) | receiving (Yielder; Yielder)

spec Declarative Outcomes = Basic Outcomes and Declarative Data then

type Completed ::= produced(Bindings)

axiom

%[1] produced(empty map) = completed

spec Declarative Labels = Basic Labels and Declarative Data then Context Info

[ sort 𝔸 ] [ op bindings : Index ]

[ sort Bindings < ContextInfo op empty map : Bindings ] spec Declarative Transitions =

Basic Configurations and Declarative Syntax and Declarative Outcomes and Declarative Labels then

vars α, α′ : 𝔸; ι, ι′ : 𝕀[𝔸];

A, A_{1} , A_{2} , A′, A′_{1} , A′_{2} : Action; Y , Y_{1} , Y_{2} : Yielder; t_{2} : Terminated; c_{1} , c_{2} : Completed; e, e_{1} , e_{2} : Escaped; d, d′ : Data; ds : DataSort; b, b′, b_{1} , b_{2} : Bindings; k : Token; bv : Bindable

axioms

%[1] Y_{1} ⟶^{ι} k ∧ Y_{2} ⟶^{ι} bv %%  %% ⇒

bind Y_{1} to Y_{2} ⟶^{ι} produced(map of k to bv);

%[2]

Y_{1} ⟶^{ι} nothing ∨ Y_{2} ⟶^{ι} nothing
%%  %% ⇒
bind Y_{1} to Y_{2} ⟶^{ι} failed;

%[3]

b = get(ι, bindings)

%%  %% ⇒

rebind ⟶^{ι} produced(b);

%[4]

Y ⟶^{ι} k ∧ b = map of k to unknown

%%  %% ⇒

unbind Y ⟶^{ι} produced(b);

%[5]

Y ⟶^{ι} nothing

%%  %% ⇒

unbind Y ⟶^{ι} failed;

%[6] Y ⟶^{ι} b %%  %% ⇒

produce Y ⟶^{ι} produced(b);

%[7]

Y ⟶^{ι} nothing
%%  %% ⇒

produce Y ⟶^{ι} failed;

%[8] A ⟶^{α} A′ %%  %% ⇒

furthermore A ⟶^{α} furthermore A′;

%[9]

b = get(ι, bindings)

%%  %% ⇒

furthermore produced(b′) ⟶^{ι} produced(overlay(b′, b));

%[10]  furthermore e ⟶^{ι} e;
%[11]  furthermore failed ⟶^{ι} failed;

%[12] A_{1} ⟶^{α} A′_{1} %%  %% ⇒

A_{1} moreover A_{2} ⟶^{α} A′_{1} moreover A_{2} ;

%[13] A_{2} ⟶^{α} A′_{2} %%  %% ⇒

A_{1} moreover A_{2} ⟶^{α} A_{1} moreover A′_{2} ;

%[14] produced(b_{1} ) moreover produced(b_{2} ) ⟶^{ι} produced(overlay(b_{2} , b_{1} ));

%[15]  e_{1} moreover A_{2} ⟶^{ι} e_{1} ;
%[16]  A_{1} moreover e_{2} ⟶^{ι} e_{2} ;
%[17]  failed moreover A_{2} ⟶^{ι} failed;
%[18]  A_{1} moreover failed ⟶^{ι} failed;

%[19]

b = disjoint union(b_{1} , b_{2} )
%%  %% ⇒

produced(b_{1} ) and produced(b_{2} ) ⟶^{ι} produced(b);

%[20]

¬ def disjoint union(b_{1} , b_{2} )
%%  %% ⇒

produced(b_{1} ) and produced(b_{2} ) ⟶^{ι} failed;

%[21]

b = disjoint union(b_{1} , b_{2} )
%%  %% ⇒

produced(b_{1} ) and then produced(b_{2} ) ⟶^{ι} produced(b);

%[22]

¬ def disjoint union(b_{1} , b_{2} )
%%  %% ⇒

produced(b_{1} ) and then produced(b_{2} ) ⟶^{ι} failed;

%[23] A_{1} ⟶^{ι} A′_{1} %%  %% ⇒

A_{1} hence A_{2} ⟶^{ι} A′_{1} hence A_{2} ;

%[24]

α′ = set(α, bindings, b_{1} ) ∧ A_{2} ⟶^{α′} A′_{2}
%%  %% ⇒
produced(b_{1} ) hence A_{2} ⟶^{α} A′_{2} ;
%[25]  produced(b) hence t_{2} ⟶^{ι} t_{2} ;
%[26]  e_{1} hence A_{2} ⟶^{ι} e_{1} ;
%[27]  failed hence A_{2} ⟶^{ι} failed;

%[28] A_{1} ⟶^{ι} A′_{1} %%  %% ⇒

A_{1} before A_{2} ⟶^{ι} A′_{1} before A_{2} ;

%[29] α′ = set(α, bindings, overlay(b_{1} , get(α, bindings)) ∧

A_{2} ⟶^{α′} A′_{2} %%  %% ⇒

produced(b_{1} ) before A_{2} ⟶^{α} A′_{2} ;

%[30]

produced(b_{1} ) before produced(b_{2} ) ⟶^{ι}
produced(overlay(b_{2} , b_{1} ));
%[31]  e_{1} before A_{2} ⟶^{ι} e_{1} ;
%[32]  c_{1} before e_{2} ⟶^{ι} e_{2} ;
%[33]  failed before A_{2} ⟶^{ι} failed;
%[34]  c_{1} before failed ⟶^{ι} failed;

b = get(ι, bindings)

%%  %% ⇒

current bindings ⟶^{ι} b;

%[36]

Y ⟶^{ι} k ∧ bv = get(ι, bindings) at k ∧ bv :< ds

%%  %% ⇒

the ds bound to Y ⟶^{ι} bv;

%[37]

Y ⟶^{ι} k ∧ bv = get(ι, bindings) at k ∧ ¬(bv :< ds)

%%  %% ⇒

the ds bound to Y ⟶^{ι} nothing;

%[38]

Y ⟶^{ι} k ∧ ¬(k is in mapped set(get(ι, bindings))

%%  %% ⇒

the ds bound to Y ⟶^{ι} nothing;

%[39]

Y ⟶^{ι} nothing
%%  %% ⇒

the ds bound to Y ⟶^{ι} nothing;

%[40]

Y_{2} ⟶^{ι} b ∧ ι′ = set(ι, bindings, b) ∧ Y_{1} ⟶^{ι′} ds
%%  %% ⇒
Y_{1} receiving Y_{2} ⟶^{ι} ds;

%[41]

Y_{2} ⟶^{ι} nothing
%%  %% ⇒
Y_{1} receiving Y_{2} ⟶^{ι} nothing

%% A.4 The Imperative Facet

spec Imperative Data =

Maps [ sort Cell ] [ free type Range ::= sort Storable | uninitialized ] with Map[Cell, Range] ↦ Storage, empty map, map of to , at , overlay, omitting, mapped set

and Sets [ sort Cell ]

with Set[Cell], empty set, set of , [not in ], is in

spec Imperative Syntax = Basic Syntax and Imperative Data then

types

Action ::= store in (Yielder; Yielder) | unstore (Yielder) | reserve (Yielder) | unreserve (Yielder);

Yielder ::= current storage | the stored in (DataSort; Yielder)

spec Imperative Labels = Basic Labels and Imperative Data then Mutable Info

[ sort 𝔸 ] [ op storage : Index ] [ sort Storage < MutableInfo op empty map : Storage ] spec Imperative Transitions =

Basic Transitions and Imperative Syntax and Imperative Labels then

vars α : 𝔸; ι : 𝕀[𝔸]; Y , Y_{1} , Y_{2} : Yielder; d, d′ : Data; ds : DataSort; s, s′ : Storage; c : Cell; sv : Storable

axioms

%[1] Y_{1} ⟶^{ι} sv ∧ Y_{2} ⟶^{ι} c ∧

s = get(ι, storage) ∧ c is in mapped set(s) ∧ s′ = overlay(map of c to sv, s) ∧ α = set(\begin{matrix}set post(ι, storage, s′), \\ commitment, true value) \end{matrix}

%%  %% ⇒

store Y_{1} in Y_{2} ⟶^{α} completed;

%[2] Y_{1} ⟶^{ι} sv ∧ Y_{2} ⟶^{ι} c ∧

s = get(ι, storage) ∧ ¬(c is in mapped set(s))

%%  %% ⇒
store Y_{1} in Y_{2} ⟶^{ι} failed;

%[3]

Y_{1} ⟶^{ι} nothing ∨ Y_{2} ⟶^{ι} nothing
%%  %% ⇒
store Y_{1} in Y_{2} ⟶^{ι} failed;

%[4] Y ⟶^{ι} c ∧ s = get(ι, storage) ∧ c is in mapped set(s) ∧ s′ = overlay(map of c to uninitialized, s) ∧ α = set(\begin{matrix}set post(ι, storage, s′), \\ commitment, true value) \end{matrix}

%%  %% ⇒

unstore Y ⟶^{α} completed;

%[5]

Y ⟶^{ι} c ∧ s = get(ι, storage) ∧ ¬(c is in mapped set(s))

%%  %% ⇒

unstore Y ⟶^{ι} failed;

%[6]

Y ⟶^{ι} nothing
%%  %% ⇒

unstore Y ⟶^{ι} failed;

%[7]

Y ⟶^{ι} ds ∧ s = get(ι, storage) ∧ ¬(c is in mapped set(s)) ∧ c :< ds ∧ s′ = overlay(map of c to uninitialized, s) ∧ α = set(\begin{matrix}set post(ι, storage, s′), \\ commitment, true value) \end{matrix}

%%  %% ⇒

reserve Y ⟶^{α} completed;

%[8]

Y ⟶^{ι} ds ∧ s = get(ι, storage) ∧

(ds & (cell[not in mapped set(s)])) = nothing

%%  %% ⇒

reserve Y ⟶^{ι} failed;

%[9]

Y ⟶^{ι} nothing

%%  %% ⇒

reserve Y ⟶^{ι} failed; Y ⟶^{ι} c ∧ s = get(ι, storage) ∧ c is in mapped set(s) ∧ s′ = omitting(c, s) ∧ α = set(\begin{matrix}set post(ι, storage, s′), \\ commitment, true value) \end{matrix}

%%  %% ⇒

unreserve Y ⟶^{α} completed;

%[11]

Y ⟶^{ι} c ∧ s = get(ι, storage) ∧ ¬(c is in mapped set(s))

%%  %% ⇒

unreserve Y ⟶^{ι} failed;

%[12]

Y ⟶^{ι} nothing
%%  %% ⇒

unreserve Y ⟶^{ι} failed;

%[13]

s = get(ι, storage)

%%  %% ⇒

current storage ⟶^{ι} s;

%[14]

Y ⟶^{ι} c ∧ sv = get(ι, storage) at c ∧ sv :< ds

%%  %% ⇒

the ds stored in Y ⟶^{ι} sv;

%[15]

Y ⟶^{ι} c ∧ sv = get(ι, storage) at c ∧ ¬(sv :< ds)
%%  %% ⇒

the ds stored in Y ⟶^{ι} nothing;

%[16]

Y ⟶^{ι} c ∧ ¬(c is in mapped set(get(ι, storage))

%%  %% ⇒

the ds stored in Y ⟶^{ι} nothing;

%[17]

Y ⟶^{ι} nothing
%%  %% ⇒

the ds stored in Y ⟶^{ι} nothing

%% A.5 The Reflective Facet

spec Reflective Data = Basic Syntax then

type Abstraction ::= abstraction of (Action) sort Abstraction < Data

spec Reflective Syntax = Basic Syntax and Functional Syntax and Declarative Syntax and Reflective Data then

types

Action ::= enact (Yielder);
Yielder ::= application to (Yielder; Yielder) | closure (Yielder)

spec Reflective Transitions = Basic Transitions and Functional Transitions and Declarative Transitions and Reflective Syntax then

vars α : 𝔸; ι : 𝕀[𝔸];

A : Action; Y , Y_{1} , Y_{2} : Yielder; d : Data; b : Bindings axioms %[1]

Y ⟶^{ι} abstraction of (A)

%%  %% ⇒

enact Y ⟶^{ι}

gave(none) then (produced(empty map) hence A);

%[2]

Y ⟶^{ι} nothing

%%  %% ⇒

enact Y ⟶^{ι} failed;

%[3]

Y_{1} ⟶^{ι} abstraction of (A) ∧ Y_{2} ⟶^{ι} d

%%  %% ⇒

application Y_{1} to Y_{2} ⟶^{ι} abstraction of (gave(d) then A);

%[4]

Y_{1} ⟶^{ι} nothing ∨ Y_{2} ⟶^{ι} nothing
%%  %% ⇒
application Y_{1} to Y_{2} ⟶^{ι} nothing;

%[5]

Y ⟶^{ι} abstraction of (A) ∧ b = get(ι, bindings)

%%  %% ⇒
closure Y ⟶^{ι}

abstraction of (produced(b) hence A);

%[6]

Y ⟶^{ι} nothing
%%  %% ⇒

closure Y ⟶^{ι} nothing %% A.6 The Communicative Facet

spec Communicative Data

Lists [ sort Message ] with List[Message] ↦ Buffer, empty list, concatenation, is in , omitting

and Numbers with Natural, 0 , successor then

sorts Agent, Communication, Sendable < Data; Message, Contract < Communication; AgentSort, MessageSort < DataSort

ops

user agent  : Agent;
contents  : Message → Sendable;
sender, receiver : Message → Agent;
serial  : Message → Natural;
[containing ] : MessageSort × DataSort → MessageSort;
[from ], [to ] : MessageSort × AgentSort → MessageSort;
[at ]  : MessageSort × DataSort → MessageSort;

axioms %% See [7, App. B.6.3].

spec Communicative Syntax = Basic Syntax then Communicative Data then

types

Action ::= send (Yielder) | remove (Yielder) | offer (Yielder) | patiently (Action);
Yielder ::= current buffer | performing agent | contracting agent

spec Communications = Communicative Data then

type Communicating ::= nil | sort Communication | ∥ (Communicating; Communicating)
op  ∥ : Communicating × Communicating → Communicating, assoc, comm, unit nil

spec Communicative Configurations = Basic Configurations and Communicative Syntax and Communications then

types Processing ::= performing (Agent; Action) | sort Action | sort Communicating | ∥ (Processing; Processing)

op  ∥ : Processing × Processing → Processing, assoc, comm, unit nil

var A : Action axiom %[1] A : Processing = user agent performing A;

spec Communicative Labels = Basic Labels and Communicative Data then Context Info

[ sort 𝔸 ] [ op performer : Index ] [ sort Agent < ContextInfo op user agent : Agent ] and

Context Info [ sort 𝔸 ] [ op contractor : Index ] [ sort Agent < ContextInfo op user agent : Agent ] and

Mutable Info [ sort 𝔸 ] [ op buffer : Index ] [ sort Buffer < MutableInfo op empty list : Buffer ] and

Mutable Info [ sort 𝔸 ] [ op serial : Index ] [ sort Natural < MutableInfo op 0 : Natural ]

then Emitted Info

[ sort 𝔸 ] [ op communicating : Index ] [ Communications fit default ↦ nil, combine ↦ ∥ ]

then Set [ sort 𝕆[𝔸] ] then Mutable Info

[ sort 𝕊 ] [ op states : Index ] [ sort Set[𝕆[𝔸]] < MutableInfo op empty set : Set[𝕆[𝔸]] ] and

Emitted Info [ sort 𝕊 ] [ op acting : Index ] [ Set [ sort Agent ] fit default ↦ empty set, combine ↦ union ] spec Communicative Transitions =

Basic Transitions and Communicative Configurations and Communicative Labels then

vars α : 𝔸; ι : 𝕀[𝔸]; t : Terminated; Y : Yielder; ds : DataSort; n : Natural; m : Message; a : Agent; c : Contract; l : Buffer

axioms %[1]

Y ⟶^{ι} ds ∧ n = get(ι, serial) ∧

m = ds[from get(ι, performer)][at n] ∧ α = set(\begin{matrix}set(\begin{matrix}set post(ι, serial, successor(n)), \\ communicating, set of (m)), \end{matrix} \\ commitment, true value) \end{matrix}

%%  %% ⇒

send Y ⟶^{α} completed;

%[2]

Y ⟶^{ι} ds ∧ n = get(ι, serial) ∧

ds[from get(ι, performer)][at n] = nothing

%%  %% ⇒

send Y ⟶^{ι} failed;

%[3] Y ⟶^{ι} m ∧ l = get pre(ι, buffer) ∧ m is in items(l) ∧

α = set(\begin{matrix}set post(ι, buffer, l omitting m), \\ commitment, true value) \end{matrix}

%%  %% ⇒

remove Y ⟶^{α} completed;

%[4]

Y ⟶^{ι} m ∧ l = get pre(ι, buffer) ∧ ¬(m is in items(l))

%%  %% ⇒

remove Y ⟶^{ι} failed;

%[5]

Y ⟶^{ι} nothing

%%  %% ⇒

remove Y ⟶^{ι} failed;

%[6]

Y ⟶^{ι} ds ∧ n = get(ι, serial) ∧ c = ds[from get(ι, performer)][at n] ∧

α = set(\begin{matrix}set(\begin{matrix}set post(ι, serial, successor(n)), \\ communicating, set of (c)), \end{matrix} \\ commitment, true value) \end{matrix}

%%  %% ⇒

offer Y ⟶^{α} completed;

%[7]

Y ⟶^{ι} ds ∧ n = get(ι, serial) ∧

ds[from get(ι, performer)][at n] = nothing

%%  %% ⇒

offer Y ⟶^{ι} failed;

%[8]

A ⟶^{α}^{+} t ∧ ¬(t = failed)

%%  %% ⇒

patiently A ⟶^{α} t;

%[9] A ⟶^{α}^{+} failed %%  %% ⇒

patiently A ⟶^{α} patiently A;

l = get(ι, buffer)

%%  %% ⇒

current buffer ⟶^{ι} l;

%[11]

a = get(ι, performer)

%%  %% ⇒

performing agent ⟶^{ι} a;

%[12]

a = get(ι, contractor)

%%  %% ⇒

contracting agent ⟶^{ι} a

pred ⟶ : Processing × 𝕊 × Processing

vars α : 𝔸; o, o′ : 𝕆[𝔸]; σ, σ_{1} , σ_{2} : 𝕊; ϵ : 𝕀[𝕊];

P_{1} , P_{2} , P′_{1} , P′_{2} : Processing; C : Communicating;

s, s′ : Set[𝕆[𝔸]]

axioms

%[13]  \begin{aligned}& P_{1} ⟶^{σ} P′_{1} \\ _{%%} & & _{%% ⇒} \\ & P_{1} ∥ P_{2} ⟶^{σ} P′_{1} ∥ P_{2} ; \end{aligned}

%[14] P_{1} ⟶^{σ_{1}} P′_{1} ∧ P_{2} ⟶^{σ_{2}} P′_{2} ∧

intersection(get(σ_{1} , acting), get(σ_{2} , acting)) = empty set ∧

σ = σ_{1} ; σ_{2} %%  %% ⇒

P_{1} ∥ P_{2} ⟶^{σ} P′_{1} ∥ P′_{2} ;

%[15] s = get pre(σ, states) ∧ o is in s ∧ a = get(o, performer) ∧

o = pre(α) ∧ A ⟶^{α} A′ ∧

C = get(α, communicating) ∧ o′ = post(α) ∧ s′ = union(difference(s, set of (o)), set of (o′)) ∧ σ = set post(set(ϵ, acting, set of (a)), states, s′)

%%  %% ⇒

a performing A ⟶^{σ} a performing A′ ∥ C ;

%[16]

s = get pre(σ, states) ∧ o is in s ∧ receiver(m) = get(o, performer) ∧ l = get(o, buffer) ∧ o′ = set(o, buffer, concatenation(l, list of (m))) ∧ s′ = union(difference(s, set of (o)), set of (o′)) ∧ σ = set post(ϵ, states, s′)

%%  %% ⇒

m ⟶^{σ} nil;

%[17] s = get pre(σ, states) ∧ a :< receiver(c) ∧ ¬(∃o • o is in s ∧ get(o, performer) = a) ∧ o′ = set(set(void, performer, a), contractor, sender(c)) ∧ s′ = union(s, set of (o′)) ∧ σ = set post(set(ϵ, acting, set of (a)), states, s′) ∧ contents(c) = abstraction of A

%%  %% ⇒

c ⟶^{σ} a performing A; %% A.7 The Directive Facet

spec Directive Data =

Maps [ sort Token ] [ free type Range ::= sort Bindable | unknown ] with Map[Indirection, Range] ↦ Redirections, empty map, map of to , at , overlay, disjoint union, mapped set

and Sets [ sort Indirection ]

with Set[Indirection], empty set, set of , is in

spec Directive Syntax = Declarative Syntax and Reflective Syntax then types

Action ::= indirectly bind to (Yielder; Yielder) | redirect to (Yielder; Yielder) | recursively bind to (Yielder; Yielder) | undirect (Yielder) | indirectly produce (Yielder);

Yielder ::= current redirections | indirect closure (Yielder)

spec Directive Labels = Directive Data then Mutable Info

[ sort 𝔸 ] [ op redirections : Index ]

[ sort Redirections < MutableInfo op empty map : Redirections ]

spec Directive Transitions = Basic Configurations and Declarative Outcomes and Directive Labels then

vars α, α′, α′′ : 𝔸; ι, ι′, ι′′ : 𝕀[𝔸];

Y , Y_{1} , Y_{2} : Yielder;

r, r′ : Redirections; i : Indirection;

b, b′, b_{1} , b_{2} : Bindings; k : Token; bv : Bindable axioms

%[1] Y_{1} ⟶^{ι} k ∧ Y_{2} ⟶^{ι} bv ∧

r = get(ι, redirections) ∧ ¬(i is in mapped set(r)) ∧ r′ = overlay(map of i to bv, r) ∧ α = set(\begin{matrix}set post(ι, redirections, r′), \\ commitment, true value) \end{matrix}

%%  %% ⇒

indirectly bind Y_{1} to Y_{2} ⟶^{α} produced(map of k to i);

%[2]

Y_{1} ⟶^{ι} nothing ∨ Y_{2} ⟶^{ι} nothing
%%  %% ⇒
indirectly bind Y_{1} to Y_{2} ⟶^{ι} failed;

%[3] Y_{1} ⟶^{ι} k ∧ Y_{2} ⟶^{ι} bv ∧

i = get(ι, bindings) at k ∧

r = get(ι, redirections) ∧ i is in mapped set(r) ∧ r′ = overlay(map of i to bv, r) ∧ α = set(\begin{matrix}set post(ι, redirections, r′), \\ commitment, true value) \end{matrix}

%%  %% ⇒

redirect Y_{1} to Y_{2} ⟶^{α} completed;

%[4] Y_{1} ⟶^{ι} k ∧ Y_{2} ⟶^{ι} bv ∧

¬(k is in mapped set(get(ι, bindings)))

%%  %% ⇒

redirect Y_{1} to Y_{2} ⟶^{ι} failed;

%[5] Y_{1} ⟶^{ι} k ∧ Y_{2} ⟶^{ι} bv ∧

i = get(ι, bindings) at k ∧

r = get(ι, redirections) ∧ ¬(i is in mapped set(r))

%%  %% ⇒

redirect Y_{1} to Y_{2} ⟶^{ι} failed;

%[6]

Y_{1} ⟶^{ι} nothing ∨ Y_{2} ⟶^{ι} nothing

%%  %% ⇒

redirect Y_{1} to Y_{2} ⟶^{ι} failed;

%[7] Y ⟶^{ι} i ∧

r = get(ι, redirections) ∧ i is in mapped set(r) ∧

r′ = omitting(i, r) ∧ α = set(\begin{matrix}set post(ι, redirections, r′), \\ commitment, true value) \end{matrix}

%%  %% ⇒

undirect Y ⟶^{α} completed;

%[8] Y ⟶^{ι} i ∧

r = get(ι, redirections) ∧ ¬(i is in mapped set(r))

%%  %% ⇒

undirect Y ⟶^{ι} failed;

%[9]

Y ⟶^{ι} nothing
%%  %% ⇒

undirect Y ⟶^{ι} failed;

%[10] Y ⟶^{ι} r ∧

α = set(\begin{matrix}set post(ι, redirections, r), \\ commitment, true value) \end{matrix}

%%  %% ⇒

indirectly produce Y ⟶^{α} completed;

%[11]

Y ⟶^{ι} nothing
%%  %% ⇒

indirectly produce Y ⟶^{ι} failed;

%[12] Y_{1} ⟶^{ι} k ∧

r = get(ι, redirections) ∧ ¬(i is in mapped set(r)) ∧ r′ = overlay(map of i to unknown, r) ∧ α′ = set post(ι, redirections, r′) ∧ b = overlay(map of k to i, get(ι, bindings)) ∧

ι′′ = set(ι′, bindings, b) ∧ Y_{2} ⟶^{ι′′} bv ∧ r′′ = overlay(map of i to bv, r) ∧ α′′ = set post(ι′, redirections, r′′) ∧ α = set(α′; α′′, commitment, true value)

%%  %% ⇒

recursively bind Y_{1} to Y_{2} ⟶^{α} produced(map of k to i);

%[13] Y_{1} ⟶^{ι} k ∧

r = get(ι, redirections) ∧ ¬(i is in mapped set(r)) ∧ r′ = overlay(map of i to unknown, r) ∧ α′ = set post(ι, redirections, r′) ∧ b = overlay(map of k to i, get(ι, bindings)) ∧

ι′′ = set(ι′, bindings, b) ∧ Y_{2} ⟶^{ι′′} nothing

%%  %% ⇒

recursively bind Y_{1} to Y_{2} ⟶^{ι} failed;

%[14]

Y_{1} ⟶^{ι} nothing
%%  %% ⇒
recursively bind Y_{1} to Y_{2} ⟶^{α} failed

%[15]

r = get(ι, redirections)

%%  %% ⇒

current redirections ⟶^{ι} r;

%% A.8 Hybrid Facets

spec Hybrid Syntax = Functional Syntax and Declarative Syntax and Reflective Syntax and Communicative Syntax then

types Action ::= allocate (Yielder) | receive (Yielder) | subordinate (Yielder) | and then moreover (Action; Action) | then moreover (Action; Action) | thence (Action; Action) | then before (Action; Action)

spec Hybrid Outcomes = Basic Outcomes and Functional Outcomes and Declarative Outcomes and Communicative Outcomes then

type Completed ::= gave produced(Data; Bindings)

axioms

%[1] gave produced(none, b) = produced(b); %[2] gave produced(d, empty map) = gave(d)

spec Hybrid Labels = Functional Labels and Declarative Labels and Imperative Labels and Communicative Labels

spec Hybrid Transitions = Basic Configurations and Hybrid Outcomes and Hybrid Labels then

vars α, α′ : 𝔸; ι, ι′ : 𝕀[𝔸];

A, A_{1} , A_{2} , A′, A′_{1} , A′_{2} : Action; Y , Y_{1} , Y_{2} : Yielder; t_{2} : Terminated; c_{1} , c_{2} : Completed; e, e_{1} , e_{2} : Escaped; d, d′ : Data; ds : DataSort; b, b′, b_{1} , b_{2} : Bindings; k : Token; bv : Bindable; m : Message; ms : MessageSort; as : AgentSort

axioms

%[1] Y ⟶^{ι} ds ∧

s = get(ι, storage) ∧ ¬(c is in mapped set(s)) ∧ c :< ds ∧ s′ = overlay(map of c to uninitialized, s) ∧ α = set(set post(ι, storage, s′), commitment, true value)

%%  %% ⇒

allocate Y ⟶^{α} gave(c);

%[2]

Y ⟶^{ι} ds ∧ s = get(ι, storage) ∧

(ds & (cell[not in mapped set(s)])) = nothing

%%  %% ⇒

allocate Y ⟶^{ι} failed; Y ⟶^{ι} ms ∧ l = get pre(ι, buffer) ∧ m :< ms ∧ m is in items(l) ∧

α = set(\begin{matrix}set post(ι, buffer, l omitting m), \\ commitment, true value) \end{matrix}

%%  %% ⇒

receive Y ⟶^{α} gave(m);

%[4] Y ⟶^{ι} ms ∧ l = get pre(ι, buffer) ∧ ¬(∃m • m :< ms ∧ m is in items(l))

%%  %% ⇒

receive Y ⟶^{ι} receive Y ;

%[5]

Y ⟶^{ι} nothing

%%  %% ⇒

receive Y ⟶^{ι} failed;

%[6]

Y ⟶^{ι} as ∧ a = get(ι, performer) ∧

A = send message[to a][containing performing agent ] then (\begin{matrix}receive message[from a][containing abstraction] \\ then enact contents(it)) ∧ \end{matrix}

A′ = offer contract[to as][containing abstraction of (A)] and then (\begin{matrix}receive message[from as][containing as] \\ then give contents(it)) \end{matrix}

%%  %% ⇒

subordinate Y ⟶^{ι} A′;

%[7]

Y ⟶^{ι} nothing
%%  %% ⇒

subordinate Y ⟶^{ι} failed;

%[8]

b = disjoint union(b_{1} , b_{2} )
%%  %% ⇒
gave produced(d_{1} , b_{1} ) and gave produced(d_{2} , b_{2} ) ⟶^{ι}

gave produced(concatentation(d_{1} , d_{2} ), b);

%[9]

¬ def disjoint union(b_{1} , b_{2} )
%%  %% ⇒
gave produced(d_{1} , b_{1} ) and gave produced(d_{2} , b_{2} ) ⟶^{ι}

failed;

%[10]

b = disjoint union(b_{1} , b_{2} )
%%  %% ⇒

gave produced((d_{1} , b_{1} ) and then gave produced(d_{2} , b_{2} ) ⟶^{ι} gave produced(concatentation(d_{1} , d_{2} ), b);

%[11]

¬ def disjoint union(b_{1} , b_{2} )

%%  %% ⇒

gave produced(d_{1} , b_{1} ) and then gave produced(d_{2} , b_{2} ) ⟶^{ι} failed;

%[12]

b = disjoint union(b_{1} , b_{2} )

%%  %% ⇒
gave produced(d_{1} , b_{1} ) then gave produced(d_{2} , b_{2} ) ⟶^{ι}

gave produced(d_{2} , b);

%[13]

¬ def disjoint union(b_{1} , b_{2} )
%%  %% ⇒
gave produced(d_{1} , b_{1} ) then gave produced(d_{2} , b_{2} ) ⟶^{ι}

failed;

b = get(ι, bindings)

%%  %% ⇒

furthermore gave produced(d, b′) ⟶^{ι} gave produced(d, overlay(b′, b));

%[15]

gave produced(d_{1} , b_{1} ) moreover gave produced(d_{2} , b_{2} ) ⟶^{ι}
gave produced(concatentation(d_{1} , d_{2} ), overlay(b_{2} , b_{1} ));

%[16]

gave produced(d_{1} , b_{1} ) hence gave produced(d_{2} , b_{2} ) ⟶^{ι}

gave produced(concatentation(d_{1} , d_{2} ), b_{2} );

%[17]

gave produced(d_{1} , b_{1} ) before gave produced(d_{2} , b_{2} ) ⟶^{ι}
gave produced(concatentation(d_{1} , d_{2} ), overlay(b_{2} , b_{1} ));

%[18] A_{1} ⟶^{α} A′_{1} %%  %% ⇒

A_{1} and then moreover A_{2} ⟶^{α}
A′_{1} and then moreover A_{2} ;
%[19]  t_{1} and then moreover A_{2} ⟶^{ι} t_{1} moreover A_{2} ;

%[20] A_{1} ⟶^{α} A′_{1} %%  %% ⇒

A_{1} then moreover A_{2} ⟶^{α} A′_{1} then moreover A_{2} ;

%[21]

α′ = set(α, data, d_{1} ) ∧ A_{2} ⟶^{α′} A′_{2}
%%  %% ⇒
gave produced(d_{1} , b_{1} ) then moreover A_{2} ⟶^{α}
gave produced(d_{1} , b_{1} ) then moreover A′_{2} ;

%[22] gave produced(d_{1} , b_{1} )then moreover gave produced(d_{2} , b_{2} ) ⟶^{ι} gave produced(d_{2} , overlay(b_{2} , b_{1} ));

%[23]  e_{1} then moreover A_{2} ⟶^{ι} e_{1} ;
%[24]  c_{1} then moreover e_{2} ⟶^{ι} e_{2} ;
%[25]  failed then moreover A_{2} ⟶^{ι} failed;
%[26]  c_{1} then moreover failed ⟶^{ι} failed;

%[27] A_{1} ⟶^{ι} A′_{1} %%  %% ⇒

A_{1} thence A_{2} ⟶^{ι} A′_{1} thence A_{2} ;

%[28]

α′ = set(set(α, data, d_{1} ), bindings, b_{1} ) ∧ A_{2} ⟶^{α′} A′_{2}
%%  %% ⇒
gave produced(d_{1} , b_{1} ) thence A_{2} ⟶^{α}
gave produced(d_{1} , b_{1} ) thence A′_{2} ;
%[29]  gave produced(d_{1} , b_{1} ) thence t_{2} ⟶^{ι} t_{2} ;
%[30]  e_{1} thence A_{2} ⟶^{ι} e_{1} ;
%[31]  failed thence A_{2} ⟶^{ι} failed;

%[32] A_{1} ⟶^{ι} A′_{1} %%  %% ⇒

A_{1} then before A_{2} ⟶^{ι} A′_{1} then before A_{2} ;

%[33]

b = overlay(b_{1} , get(α, bindings)) ∧ α′ = set(set(α, data, d_{1} ), bindings, b) ∧

A_{2} ⟶^{α′} A′_{2} %%  %% ⇒

gave produced(d_{1} , b_{1} ) then before A_{2} ⟶^{α} A′_{2} ;

%[34]

gave produced(d_{1} , b_{1} ) then before gave produced(d_{2} , b_{2} ) ⟶^{ι}
gave produced(d_{2} , overlay(b_{2} , b_{1} ));
%[35]  e_{1} then before A_{2} ⟶^{ι} e_{1} ;
%[36]  c_{1} then before e_{2} ⟶^{ι} e_{2} ;
%[37]  failed then before A_{2} ⟶^{ι} failed;
%[38]  c_{1} then before failed ⟶^{ι} failed;

%% A.9 The Full Action Notation

spec Action Notation = Basic Transitions and Functional Transitions and Declarative Transitions and Imperative Transitions and Reflective Transitions and Directive Transitions and Communicative Transitions and Hybrid Transitions

%[Appendix B] library Label Categories

spec Categories [ sort 𝔸 ] = sorts 𝕀[𝔸] < 𝔸; 𝕆[𝔸] = 𝕀[𝔸] ops

; : 𝔸 × 𝔸 →? 𝔸, assoc;
pre, post : 𝔸 → 𝕆[𝔸]
vars α, α′ : 𝔸; ι : 𝕀[𝔸]

axioms %[1] def (α; α′) ⇔ post(α) = pre(α′); %[2] ι; α = α if def (ι; α); %[3] α; ι = α if def (α; ι)

spec Indices = sort Index

spec Components =

sorts ContextInfo, MutableInfo, EmittedInfo

type LabelComp ::= sort ContextInfo | pair(π_{1} , π_{2} : MutableInfo) | sort EmittedInfo

type StateComp ::= sort ContextInfo | sort MutableInfo

spec Label Categories [ sort 𝔸 ] = Categories [ sort 𝔸 ] and Indices and Components then

ops void: 𝕆[𝔸];

get : 𝔸 × Index →? LabelComp;
set : 𝔸 × Index × LabelComp →? 𝔸

vars α : 𝔸; i, i′ : Index; c, c′ : LabelComp

axioms

%[1] get(set(α, i, c), i′) = c when i = i′ else get(α, i′);

%[2] set(set(α, i, c), i′, c′) =

set(α, i, c′) when i = i′ else set(set(α, i′, c′), i, c)

ops get pre(α : 𝔸; i : Index) :?MutableInfo = π_{1} (get(α, i)); set post(α : 𝔸; i : Index; m : MutableInfo) :?𝔸 =

set(α, i, pair(π_{1} (get(α, i)), m))

ops

get: 𝕆[𝔸] × Index →? StateComp;
set : 𝕆[𝔸] × Index × StateComp →? 𝕆[𝔸]

vars o : 𝕆[𝔸]; i, i′ : Index; s, s′ : StateComp axioms

%[3] get(set(o, i, s), i′) = s when i = i′ else get(o, i′);

%[4] set(set(o, i, s), i′, s′) =

set(o, i, s′) when i = i′ else set(set(o, i′, s′), i, s) spec Context Info [ sort 𝔸 ] [ op i : Index ]

[ sort CI < ContextInfo op default : CI ] given Label Categories [ sort 𝔸 ] =

vars α, α_{1} , α_{2} : 𝔸; c, c′ : CI

axioms %[1] get(void, i) = default; %[2] set(void, i, default) = void; %[3] pre(set(α, i, c)) = set(pre(α), i, c); %[4] post(set(α, i, c)) = set(post(α), i, c); %[5] set(α_{1} , i, c) ; set(α_{2} , i, c) = set(α_{1} ; α_{2} , i, c); %[6] def set(α_{1} , i, c) ; set(α_{2} , i, c′) ⇒ c = c′

spec Mutable Info [ sort 𝔸 ] [ op i : Index ] [ sort MI < MutableInfo op default : MI ] given Label Categories [ sort 𝔸 ] =

vars α, α_{1} , α_{2} : 𝔸; m, m′, m_{1} , m_{2} : MI

axioms %[1] get(void, i) = default; %[2] set(void, i, default) = void; %[3] pre(set(α, i, pair(m_{1} , m_{2} ))) = set(pre(α), i, m_{1} ); %[4] post(set(α, i, pair(m_{1} , m_{2} ))) = set(post(α), i, m_{2} ); %[5]

set(α_{1} , i, pair(m_{1} , m)) ; set(α_{2} , i, pair(m, m_{2} )) =
set(α_{1} ; α_{2} , i, pair(m_{1} , m_{2} ));

%[6] def set(α_{1} , i, pair(m_{1} , m) ; set(α_{2} , i, pair(m′, m_{2} )) ⇒ m = m′

spec Emitted Info [ sort 𝔸 ] [ op i : Index ] [ \begin{matrix}sort EI < EmittedInfo \\ ops default : EI ; combine : EI × EI → EI , assoc, unit default ] \end{matrix}

given Label Categories [ sort 𝔸 ] =

vars α, α_{1} , α_{2} : 𝔸; e, e′ : EI

axioms %[1] get(ι, i) = default; %[2] set(ι, i, default) = ι; %[3] pre(set(α, i, e)) = pre(α); %[4] post(set(α, i, e)) = post(α); %[5] set(α_{1} , i, e) ; set(α_{2} , i, e′) = set(α_{1} ; α_{2} , i, f (e, e′))

%[Appendix C] library Data Notation

spec Unified Algebras = sorts Indiv < Univ pred ≤ : Univ × Univ vars u, u′, u′′ : Univ axioms %[1] u ≤ u′ ∧ u′ ≤ u′′ ⇒ u ≤ u′′ %[2] u ≤ u′ ∧ u′ ≤ u ⇒ u = u′ %[3] u ≤ u op nothing : Univ axiom %[4] nothing ≤ u pred :< (u, u′) ⇔ u ∈ Indiv ∧ u ≤ u′ axiom %[5] ¬(u :< nothing) ops | : Univ × Univ → Univ, assoc, comm, idem, unit nothing; & : Univ × Univ → Univ, assoc, comm, idem;

axioms %[6] u & nothing = nothing; %[7] u ≤ u′′ ∧ u′ ≤ u′′ ⇒ (u | u′) ≤ u′′; %[8] u ≤ (u | u′); %[9] u′′ ≤ u ∧ u′′ ≤ u′ ⇒ u′′ ≤ (u & u′); %[10] (u & u′) ≤ u; %[11] u & (u′ | u′′) = (u & u′) | (u & u′′); %[12] u | (u′ & u′′) = (u | u′) & (u | u′′)

from [7, App. E] get Tuples, Truth Values, Numbers, Lists, Sets, Maps %% with translation to Casl!

Recent BRICS Report Series Publications

RS-99-56 Peter D. Mosses. A Modular SOS for Action Notation. December 1999. 39 pp. Full version of paper appearing in Mosses and Watt, editors, Second International Workshop on Action Semantics, AS ’99 Proceedings, BRICS Notes Series NS-99-3, 1999, pages 131–142.

RS-99-55 Peter D. Mosses. Logical Specification of Operational Semantics. December 1999. 18 pp. Invited paper. Appears in Flum, Rodríguez-Artalejo and Mario, editors, European Association for Computer Science Logic: 13th International Workshop, CSL ’99 Proceedings, LNCS 1683, 1999, pages 32–49.

RS-99-54 Peter D. Mosses. Foundations of Modular SOS. December 1999. 17 pp. Full version of paper appearing in Kuty�owski, Pacholski and Wierzbicki, editors, Mathematical Foundations of Computer Science: 24th International Symposium, MFCS ’99 Proceedings, LNCS 1672, 1999, pages 70–80.

RS-99-53 Torsten K. Iversen, Kåre J. Kristoffersen, Kim G. Larsen, Morten Laursen, Rune G. Madsen, Steffen K. Mortensen, Paul Pettersson, and Chris B. Thomasen. Model-Checking Real-Time Control Programs — Verifying LEGO Mindstorms Systems Using UPPAAL. December 1999. 9 pp.

RS-99-52 Jesper G. Henriksen, Madhavan Mukund, K. Narayan Kumar, and P. S. Thiagarajan. Towards a Theory of Regular MSC Languages. December 1999.

RS-99-51 Olivier Danvy. Formalizing Implementation Strategies for First-Class Continuations. December 1999. Extended version of an article to appear in Programming Languages and Systems: Ninth European Symposium on Programming, ESOP ’00 Proceedings, LNCS, 2000.

RS-99-50 Gerth Stølting Brodal and Srinivasan Venkatesh. Improved Bounds for Dictionary Look-up with One Error. December 1999. 5 pp.

RS-99-49 Alexander A. Ageev and Maxim I. Sviridenko. An Approximation Algorithm for Hypergraph Max k-Cut with Given Sizes of Parts. December 1999. 12 pp.