AS on Sunday

Detailed program
Sunday July 21st, 2002
See also the unified by-slot program

All sessions take place in auditorium 10.

08:45-09:00  Session 1: Opening and Introduction

Session 2: Tools and Applications

09:00-09:30  Mark van den Brand, CWI Amsterdam, The Netherlands
Jurgen Vinju, CWI Amsterdam, The Netherlands
How ASF+SDF technology can be used to develop an action semantics environment
The next generation of the ASF+SDF Meta-Environment is again used to develop an environment for action semantics. The modularity of ASF+SDF has been fully exploited, each language construct is formulated in a separate module.
We will present the technical background of the new ASF+SDF Meta-Environment from the perspective of developing the action semantics environment. The new ASF+SDF Meta-Environment is based on a software coordination architecture and this should offer the possibility to connect tools like a type checker, an interpreter, and a compiler for action semantics in a straightforward manner. We will discuss the various approaches to do this. The aspect of genericity of the Meta-Environment will be discussed and what has to be done when the action semantics modules become less ASF+SDF like. The current prototype of the action semantics environment based on ASF+SDF technology uses directly SDF to describe the syntax rules. This means that quite some SDF specific keywords are used, given the fact that only one syntax rule is specified per module, half of such a module consists of SDF keywords. A logical step would be to develop an action semantics specific SDF variant. This step has quite some consequences on the architectural level of the ASF+SDF Meta-Environment.
See for further details

09:30-10:00  Luis Carlos Meneses, Federal U of Pernambuco, Brazil
Hermano Moura, Federal U of Pernambuco, Brazil
Wanderley Cansancao, Federal U of Pernambuco, Brazil
Monique Monteiro, Federal U of Pernambuco, Brazil
Pablo Sampaio, Federal U of Pernambuco, Brazil
The Abaco system: An action tool for programming language designers
We describe the structure of the Abaco System, an action semantics tool that enables the programming language designer to build and test action semantics descriptions. The system is formed by a set of compiler generation tools like parser generators, specification processors, including sort checkers and interpreters for action semantic descriptions. These tools can be used to process action semantics descriptions for programming languages and to generate interpreters and compilers for them.
Abaco's tools are integrated in a graphical user interface environment, allowing a friendly design of new specifications and their immediate test. One important Abaco's feature is its ability to handle complex descriptions that use new user-defined actions. It allows the building of semantic libraries that can be useful to easy the description of complex languages and to improve the reusability of a specification.
We also propose to demonstrate the newest release of the system, which is freely available on the net, and which is based on a more generic action semantics interpreter that can be used to execute both current versions of action notation and allows the user to describe and to execute action extensions for them.

10:00-10:30  Adnan Sherif, Federal U of Pernambuco, Brazil
Ana Cavalcanti, Federal U of Pernambuco, Brazil
Hermano Moura, Federal U of Pernambuco, Brazil
Using Abaco to animate a real-time specification language
The Algebraic Based Action COmpiler (ABACO) is an action semantics specification tool. In this work we focus on the framework provided by the ABACO tool. The framework allows the creation of actions and yielders using the Java programming language. We illustrate the use of the framework with a case study: We study a real time specification language similar to Timed CSP. The semantics of our case study language is given with focus on integration with the a Timer developed using the framework. Finally we consider some example programs written in the target language and study the result of animating them in the tool.
See for further details

Session 3: Foundations

11:00-11:30  Cláudio R. V. Carvilhe, Federal U of Paraná, Brazil
Martín A. Musicante, Federal U of Paraná, Brazil
An object-oriented view of action semantics descriptions
In separate works, Doh with Mosses and Menezes with Moura propose the notions of modules (or components) to structure Action Semantics descriptions.
In this work, we introduce Object-Oriented Action Semantics, a new form of modularization within the action semantics framework. In our approach, objects are defined by grouping syntactic and semantic entities, using a notation based on that proposed by Doh and Mosses.
In Object-Oriented Action Semantics, semantic equations are seen as defining methods. Method names can be overloaded.
In the full paper, we present an example of use of the new notation, as well as its operational semantics. A novel feature of the operational semantics of Object-Oriented Action Notation is the introduction of a method environment, a mapping from method names to actions. The introduction of this mapping allows us to describe the semantics of the complete notation, including the definition of methods.
See for further details

11:30-12:00  Luis Carlos Meneses, Federal U of Pernambuco, Brazil
Hermano Moura, Federal U of Pernambuco, Brazil
An extensible definition for action notation
Action notation allows the construction of modular and reusable formal definitions of programming languages. However, this notation does not contain any well-defined process to define new action operators.
Recently action notation has been reviewed and a new version of it was proposed (Action Notation 2). Using the traditional action semantics based compiler generation tools we will need to rebuild these tools to support the new notation.
To avoid the design a different tool for each action notation and define a mechanism to facilitate the definition of new action operators, we design a simple action "assembler" language formed by a set of operators that defines abstract facet's behaviors.
Defining the action notation semantics using this "assembler" language, the designer is free to extend or customize their definition with new semantic combinators without loose the supporting of existing action semantics tools. The proposed notation is the base engine used by the latest version of the Abaco system to support both versions of action notation using a single execution engine.
See for further details

12:00-12:30  Peter D. Mosses, U Aarhus, Denmark
A modular SOS for action notation, revisited
A draft modular SOS for the new version of AN, referred to as AN-2, has been available since 2000. It is written in CASL and has been checked for well-formedness using CATS (CASL Tool Set). It appears to be significantly more accessible than the original SOS of AN-1. However, it now appears that further improvements are possible:
* The description of exceptions and failures can be made completely modular.
* A more perspicuous notation for accessing and changing components of labels is available.
It may also be desirable to avoid the explicit use of CASL, using a more streamlined meta-notation for the modular SOS rules.
After discussing the issues, we look at some illustrative examples taken from an improved modular SOS of AN-2 (in preparation). We also look at the possibility of empirical testing of the modular SOS by a straightforward translation to Prolog.
See for further details

Session 4: Related Frameworks

14:00-15:00  Egon Börger, U Pisa, Italy
Invited talk: Computation and specification models: A comparative study
For each of the principal current models of computation and of high-level system design, we present a uniform set of transparent easily understandable descriptions, which are faithful to the basic intuitions and concepts of the investigated systems. Our main goal is to provide a mathematical basis for technical comparison of established models of computation which can contribute to rationalize the scientific evaluation of different system specification approaches in the literature, clarifying in detail their advantages and disadvantages. As a side effect we obtain a powerful yet simple new approach for teaching the fundamentals of computation theory. Abstract State Machines are used as modeling framework.

15:00-15:30  Alexey Kalinov, ISP/RAS Moscow, Russia
Alexander S. Kossatchev, ISP/RAS Moscow, Russia
Mikhail Posypkin, ISP/RAS Moscow, Russia
V. Shishkov, ISP/RAS Moscow, Russia
Using ASM specification for automatic test suite generation for mpC parallel programming language compiler
The mpC is a parallel programming language for heterogeneous computer networks. It is a two-level ANSI C extension. The first level extends C with new operators supporting array computations. The next level of extension includes different language constructs for explicit parallel programming. Since mpC expressions are very powerful and rather complex there raised a problem of producing a comprehensive test suite for checking the correctness of mpC expressions translation.
The approach proposed in this paper is based on using executable ASM specifications (implemented in Gem-Mex framework) for separating semantically correct tests from incorrect ones and for building test oracles. The syntactically correct expressions are generated by combining abstract syntax tree nodes. The semantically correct tests are detected by executable ASM specification. These tests are used for validation of correctness of code generation. The output of generated application is compared with the output of test interpretation by ASM-specification.
The test suite was generated using this technique. It helped us to improve quality of mpC compiler significantly.
See for further details

Session 5: Foundations

16:00-16:30  Ki-Hwan Choi, Hanyang U, South Korea
Kyung-Goo Doh, Hanyang U, South Korea
Seung Cheol Shin, Dongyang U, South Korea
The analysis of secure information-flow in actions by abstract interpretation
This talk reports our ongoing work on the analysis of secure information-flow in actions.
Information flow analysis is to statically determine how an action's outputs are dependent, directly and indirectly, on its inputs. The analysis is used to certify that an action is secure meaning that the information classified as "secret" is not revealed to unauthorized objects during its flow through the action's performance.
The analysis is defined using the abstract interpretation framework, and is to be proved sound.

16:30-17:00  Jørgen Iversen, U Aarhus, Denmark
Type inference for the new action notation
In the proposal for a new version of Action Notation (AN-2) an effort has been made in making the kernel of the notation smaller, and the whole notation less complicated. We identify some problems introduced with AN-2 with respect to type inference, and give solutions to them together with solutions to problems which have not been addressed in previous work on inferring types of actions. Some of them are:
* Action combinators in the declarative facet have been replaced with data operators.
* We have given type inference rules for some of the new action combinators.
* Overloaded operators is a problem, because we can not choose the operator with the best matching signature before the input types for the operator have been inferred.
* Some actions has the possibility of both terminating exceptionally and normally, and giving different types of data in the two cases.
Compared to the previous version of Action Notation, AN-2 makes it easier to write and read action semantic descriptions, but is it at the expense of worse analysis? We try to compare the two versions with respect to type inference.

Session 6: Tools

17:00-17:30  Tijs van der Storm, U Amsterdam, The Netherlands
AN-2 tools
We present a number of action interpreters and compilers based on the new proposed action notation, AN-2. Our effort can be seen as a testcase for different approaches towards implementing actions. In addition to the benefits of executing actions, we concentrated on three desirable properties: portability, scalability and deployability.
The tools presented all support the complete kernel of AN-2 including the interacting facet. Interpretation is implemented in three more or less different ways. The first interpreter consists of a compiled ASF+SDF specification. The second interpreter is implemented in C using termrewriting of abstract AN-2 syntax. Both closely follow the definition of AN-2 in MSOS. The third interpreter operates in two stages. First an action is compiled to Action Intermediate Language (AIL) which can be seen as a serialized form of action notation. AIL is again optimized and interpreted by a virtual machine (avm). The action compilers target C (acc) and Java (acj). The target source is generated from optimized AIL code.
See for further details

Session 7: The Future of Action Semantics and Related Frameworks

17:30-18:00  Discussion