sessions take place in auditorium 10.
||Mark van den Brand, CWI Amsterdam, The
Vinju, CWI Amsterdam, The Netherlands
ASF+SDF technology can be used to develop an action semantics
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
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
See http://www.brics.dk/Projects/AS/2002/BrandVinju/ for further
||Luis Carlos Meneses,
Federal U of Pernambuco, Brazil|
Moura, Federal U of Pernambuco, Brazil
Cansancao, Federal U of Pernambuco, Brazil
Monteiro, Federal U of Pernambuco, Brazil
Sampaio, Federal U of Pernambuco, Brazil
Abaco system: An action tool for programming language
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
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 http://www.cin.ufpe.br/~rat, 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.
||Adnan Sherif, Federal U of Pernambuco,
Cavalcanti, Federal U of Pernambuco, Brazil
Moura, Federal U of Pernambuco, Brazil
Abaco to animate a real-time specification language
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 http://www.brics.dk/Projects/AS/2002/SherifCavalcantiMoura/ for
||Cláudio R. V. Carvilhe, Federal U of
A. Musicante, Federal U of Paraná, Brazil
object-oriented view of action semantics descriptions
separate works, Doh with Mosses and Menezes with Moura propose
the notions of modules (or components) to structure Action Semantics
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
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
See http://www.brics.dk/Projects/AS/2002/CarvilheMusicante/ for
||Luis Carlos Meneses, Federal U of Pernambuco,
Moura, Federal U of Pernambuco, Brazil
extensible definition for action notation
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 http://www.cin.ufpe.br/~rat/abaco to support both versions of
action notation using a single execution engine.
See http://www.brics.dk/Projects/AS/2002/MenesesMoura/ for further
||Peter D. Mosses, U Aarhus, Denmark|
modular SOS for action notation, revisited
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
It may also be desirable to avoid the explicit use of CASL,
using a more streamlined meta-notation for the modular SOS rules.
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 http://www.brics.dk/Projects/AS/2002/Mosses/ for further
||Egon Börger, U Pisa, Italy|
talk: Computation and specification models: A comparative study
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
||Alexey Kalinov, ISP/RAS
S. Kossatchev, ISP/RAS Moscow, Russia
Posypkin, ISP/RAS Moscow, Russia
Shishkov, ISP/RAS Moscow, Russia
ASM specification for automatic test suite generation for mpC
parallel programming language compiler
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
for further details
||Ki-Hwan Choi, Hanyang U, South Korea|
Doh, Hanyang U, South Korea
Cheol Shin, Dongyang U, South Korea
analysis of secure information-flow in actions by abstract
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.
||Jørgen Iversen, U Aarhus, Denmark|
inference for the new action notation
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.
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.
||Tijs van der Storm, U Amsterdam, The Netherlands|
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.
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 http://www.brics.dk/Projects/AS/2002/Storm/ for further