32
Hartmut Ehrig, Friedrich von Henke, José Meseguer, Martin Wirsing, (editors): Specification and Semantics Dagstuhl-Seminar-Report; 64 24.05.28.05.93 (9321)
Hartmut Ehrig, Friedrich von Henke,José Meseguer, Martin Wirsing, (editors):
Specification and Semantics
Dagstuhl-Seminar-Report; 6424.05.�28.05.93 (9321)
ISSN 0940-1121
Copyright © 1994 by IBFI GmbH, Schloss Dagstuhl, D-66687 Wadern, GermanyTel.: +49-6871 - 2458Fax: +49-6871 - 5942
Das Internationale Begegnungs- und Forschungszentrum für lnformatik (IBFI) ist eine gemein-nützige GmbH. Sie veranstaltet regelmäßig wissenschaftliche Seminare, welche nach Antragder Tagungsleiter und Begutachtung durch das wissenschaftliche Direktorium mit persönlicheingeladenen Gästen durchgeführt werden.
Verantwortlich für das Programm ist das Wissenschaftliche Direktorium:Prof. Dr. Thomas Beth.,Prof. Dr.-lng. José Encarnacao,Prof. Dr. Hans Hagen,Dr. Michael Laska,Prof. Dr. Thomas Lengauer,Prof. Dr. Wolfgang Thomas,Prof. Dr. Reinhard Wilhelm (wissenschaftlicher Direktor)
Gesellschafter: Universität des Saarlandes,Universität Kaiserslautern,Universität Karlsruhe,Gesellschaft für Informatik e.V., Bonn
Träger: Die Bundesländer Saarland und Rheinland-Pfalz
Be'°'.ugsadresse: Geschäftsstelle Schloss DagstuhlUniversität des Saarlandes
Postfach 15 11 50
D-66041 Saarbrücken, GermanyTel.: +49 -681 - 302 - 4396
Fax: +49 -681 - 302 - 4397 _
e-mail: [email protected]
Contents
Egidio AstesianoD-oids Models and languages for dynamic and object systems . . . . . . . . . . . . . . . . . . . . . . . . . .2
Rudolf BerghammerPrototyping relational speci�cations using higher-order objects . . . . . . . . . . . . . . . . . . . . . . . . . .2
Michel Bidoit
Modularity, Strongly Persistent Functors and �Stability� . . . . . . . . . . . . . . . . . . . . . . . . . . . . ..3
Andrea Corradini
Relating two (Parametric) Categorical Semantics for Rule-Based Systems . . . . . . . . . . . . ..4
Hans-Dieter Ehrich
Object Roles and Phases . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ..5
Hartmut EhrigFLEX: A Flexible Extension and Integration Concept for Software Development in K ORS Oand COMPASS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ..5
Martin GogollaA Computational Model for TROLL light . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
Ursula Goltz
Temporal Logics and the Semantics of Concurrent Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . .7
Friedrich von Henke
Types, Speci�cations, and Software Development . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ..7
Bernd Krieg-Brückner, Junbo Liu, Burkhart Wolff and Hui ShiTowards Correct, E�icient and Reusable Transformational Developments . . . . . . . . . . . . . ..8
Michael Löwe
Initial Semantics For Speci�cation Developments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
Klaus MadlenerPositive/negative conditional equational speci�cations (Constraints in built-in algebras andtheories) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .10
Narciso Marti�-Oliet and José MeseguerRewriting Logic as a Logical and Semantic Framework . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
Bernhard Möller
An Algebraic Approach To Program Derivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
Peter D. Mosses
Action Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1'2
M. Navarro, F. Orejas, A. Sanchez 1On the Correctness of Modular Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
Peter Padawitz
Speci�cation and Programming: Where is the Difference? . . ., . . . . . . . . . . . . ._ . . . �g . . . . . . g. 14
P. PepperParameterization or Polymorphism or Both? . . . . . . . . . . . �g . . . . . . . . . . . g. @#j� �g . . S . . . . . . . . � . . 14
Axel Poigné r .Modelling and Speci�cation of Reactive Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
Horst Reichel ASpeci�cation of Concurrent Object Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
Wolfgang Reif CSpeci�cation and Veri�cation of Modular Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .16
Don Sannella
Static and logical correctness conditions in formal development of modular programs . . 17
Gunther Schmidt
Ordering Isomorphism Classes of Semantic Domains . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.8
Martin Simons and Stefan Jahnichen
.f5'or"malized Developments in Deva . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ..l8
Carolyn TalcottRecent Results on Actor Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . : . �g . . . . . . . . . .19
Walter VoglerTimed Testing of Concurrent Systems. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .19
Martin WirsingUntyped Constrained Lambda Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
Uwe Wolter
Categorical Concepts for Parameterized Partial Speci�cations . . . . . . . . . . . . . . . . . �ß . . . . . , . 20
Preface
In this seminar recent scienti�c results and new research directions in the area of formal
foundations of software development were discussed by members of the working group FG0.1.7 "Speci�cation and Semantics" of the German Society for Computer Science (GI) andother well-known scientists. The 30 talks focussed in particular on the following topics:
a mathematical foundations of speci�cation and semanticsincluding models and logic calculi, concepts of category and type theory, algebraicconcepts, theorem provers
o methods of formal semantics
including denotational, operational and axiomatic semantics, algebraic and categor-ical semantics, transition systems, term and graph rewriting
o approaches to formal specification including abstract data types, model�orientedspeci�cation, algebraic speci�cation, graphical spe(�i�('a.ti()11, formal spe<-i�(-ation lan-guages
0 formal development and ve1'ifi(r-ation met.l1odsincluding formal requirement analysis and speci�cation, str11(-turing and n1odular-ization techniques, veri�cation and validat.ion of modules and con�gurations, formalaspects of reusability
0 applications of speci�cation and semanticsincluding description of programming languages, methods for software development,parallel and distributed systems, modeling and speci�cation languages, data andknowledge based systems
On behalf of all participants the organizers would like to thank the staff of Schlo� Dagstuhlfor providing an excellent environment to the conference.
The Organizers
Hartmut Ehrig Friedrich von Henke Jose Meseguer Martin W irsing
D-oids Models and languages for dynamic and objectsystems
Egidio Astesiano
DISI-Universita di Geneva, Italy
(joint work with Elena. Zucca.)
D-oids are a model for systems of dynamic entities,based on the following features: Statesare modelled by structures (a1gebras,usually) in some category; we assume that everystructure (called inst.ant structure) has an underlying support consisting in an S-sortedfamily of sets;
Variations of state are modelled by dynamic operat.ions (also called methods) calls, whosesemantics is the most typical features of l.l'l(-� ap1)1'oa(°l1: the effect of a call is a transformationof the source state into a ne.w state, consisting� in a map between t.he unde1'l__ving carriers:this map is called "tracking map", since intuitively it keeps track of the identities of theevolving dynamic entities. An appropriate rather natural notion of niorphisin is given .�.~;u('l1that the d-oids over a category of instant structures are a (-at.ego1'y.
The emphasis of this talk is on a recent new result,consisting in the construction of thed-oid of dynamic terms over a dynamic signature and a family of variables. In the casethat the instant structures are provided of a fre construction of terms over families ofgenerators,then the d-oid of dynamic terms is a free construction. A most notable featureof the constructioii is the unique representation ;in other words a canonical representationis provided (no identi�cation) as it happens in the classical static case. It ca.n be shownthat usual imperative method expressions can be translated into the language of dynamicterms,which then may be seen as the basis of a kernel language for de�ning methods withthe typical �avour of an applicative language.
Prototyping relational speci�cations usinghigher-order objects
Rudolf Berghammer
U iiversitat der Bundeswehr München Neubiberg, Germany
In the last two decades, the axiomatic relation calculus has widely been accepted by com-puter scientists who view it as a convenient formalism to describe fundamental conceptsof programming. Also this talk deals with relation algebra as a formal programming tool.
First, we (les('ribe an approach for the development of executable relational speci�cationsout of non-<.-onstrtrctive first�order problem descriptions. Here certain functionals 011 rela-tions (e.g., residuals, synnnetrie quotients. and functionals for bounds and extremal ele-ments) in ('()111l.)i11a.t.i011 with a. relational description of higlier-order objects (e.g., sets, setsof sets, and mappings) play a.n important role.
In the second part of the talk, we give a. short. description of the computer system RELVIEVVand demonstrate how it can be used to perform execut.a.l)le relational speci�cations.
The algoritlnns (tlesc1'il.)e(l by the e.\'e(+utable speci�ca.tions frequently may be fairly inef-ficient compared to han(l-1na.(le ones. However. they are liuilt-up very quickly and theirproofs of correctness a.re ve1j\;' easy. Fu1't.l1er1nore. as wo Sl1()W in the last part of the talk.t.l1e_\,' can be the Starting points for the (leveluprnent of more efficient algoritlnns using the(talclrlus of rela.t:ions. H(�11(°(�. we ll2l\'(' the t_\'pi<-al situation of rapid })1'<)t()t_\'1)l11g.
Modularity, Strongly Persistent F unctors and�Stability�Michel Bidoit
LIENS, CNRS & Ecole Normale Superieure, Paris, France
(joint work with Rolf Hennicker, Munich U11ive1'sit_\;')
In this talk we first briefly l'e<-all our a.pproa.el1 to nlodularity w.r.t. the serriantics and imple-mentation of software specifications. Based on the strati�ed loose se1na.ntics approach, ourspeeificatiori franiework nieets the following requirements: the independent construction
A of irnplernentation for the single constituent parts (rnodules) of a systeln speci�catiori andthe encapsulated developrnent of each innrlernentation part using the. principle of stepwisere�neinent.
Wo show tha.t inrplernentation and paranieterization can be handled within a uniforniconcept. and we prove cornpatil)ility theorems like the hori7,onta.l colnposition prope1't_\'.
Then we discuss whether the seniautics of a. spe<'i�(°a,tion lll()(llll(-� should be a class offunctors (as in our a.pp1�0a.('l1) or just a. class of niappings (as a.(lvocat.ed in some otherrelated works). A careful study points out the following facts:
o To be of praet.ica.l interest, the logical framework considered should include an ob-
servability concept.
o If observability is handled through a behavioural approach (by means of some be-havioural equivalence between a.lgel,)ras), then the mappings should be ��stable� in�order to ensure the required compositional properties.
3
o If observability is handled through an observational approach (by means of an ob-servational satisfaction relation), then �stability� is required as well, but can beexpressed by the �persistency" of some �observational morphisms� through the map-pings. Hence we show that a �stable mapping� is nothing else but a strongly persis-tent functor in the category having these observational morphisms as arrows.
Relating two (Parametric) Categorical Semantics forRule-Based Systems
Andrea Corradini
Dipartimento di Informatica - Pisa, ITALY
J. Meseguer and U. Montanari proposed in [MM 90] a new categorical semantics for P,/TPetri nets. Generalizing their approach. two parametric categorical semantics for rule-bsed systems have been proposed by J. Meseguer [Mes 92] and by A. Corradini and U.Montanari [CM 92], respectively. Each one of those semantics is applicable to a wide classof formalisms, and both are parament.ric: however, their precise relationship have neverbeen explored before. This is the topic of this presentation, which reports on an ongoingresearch.
After introducing the categorical methodology proposed in [CM 92], we show how it can Abe applied to Term Rewriting Systems, and that this speci�c application captures theunconditional case of Meseguers� Rewriting Logic, in the sense that the same class ofmodels is determined. However, on the one hand the conditional part of Rewriting Logicdoes not seem to fit in the methodology of [CM 92]; on the other hand there are applicationsof such methodology that determine models which do not seem to be characterizable in anatural way in Rewriting Logic. Thus we claim that the two categorical sem_anti(:s are ingeneral uncomparable, although they have a signi�cant intersection.
References
[MM 90] T. Meseguer and U. Montanari, Petri Nets are monoids, Info & Co. 88 (1990).
[Mes 92] J. Meseguer, Conditional rewriting logic as a model of concurrency, TCS 96(1992).
[CM 92] A. Corradini and U. Montanari, An algebraic semantics for structured transi-tion systems and its application to logic programs, TCS 103(1992).
4
Object Roles and PhasesHans-Dieter Ehrich
Abteilung Datenbanken, Technische Universität Braunschweig
in cooperation with Ralf Jungclaus and Grit Denker
Object roles are temporary specializations where the object can go through, possibly morethan once. An example is a person whocan be a patient at times. There may be severalroles like patient, employee, tax payer, etc., the phases of which may be entered and left in-dependently, in any order. The TROLL language� for specifying communities of concurrentinteracting objects offers language features for specifying roles. In his recent dissertation,Ralf J ungclaus offered a close to complete formal semantics of TROLL, based on temporallogic. The semantics of roles, however, as well as that of creation and destruction, was leftout - it was not formalizable in OSL, the logic adopted. The talk offers an approach toextend OSL so that roles as well as creation and destruction of objects can- be expressedin a natural way. The essential idea is to introduce an "in-scope" predicate for actions,in addition to the "enabled" predicate of OSL. While the latter is a way to cope withnondeterminism as introduced by hiding, the former captures visibility of attributes andactions as governed by creating and destroying objects as well as entering and leavingroles. The relationships between roles are made precise by speci�cation morphisms. Theirsemantics is given by process morphisms. These morphisms also capture other kinds ofobject relationships, like generalization, aggregation, and interfaces.
FLEX: A Flexible Extension and Integration Conceptfor Software Development in KORSO and COMPASS
Hartmut Ehrig
Technical University of Berlin
Motivated by the experience within the ESPRIT BR WG COMPASS and the BMF T-project KORSO (Korrekte Software) we propose a �exible extension and integration con-cept for software development, called FLEX. In addition to support software developmentby formal methods the aims of FLEX are mainly to allow a smooth change from classicalsemi-formal techniques for software development to formal techniques with �exible toolsupport for all levels of development. These aims lead to a number of requirements forFLEX which are already partially supported by concepts available in the literature, whileseveral other aspects concerning extension and integration of different subtechniques andlanguages still have to be investigated. To meet these aims and requirements a general and
�rst speci�c tasks are de�ned and it is shown how far recent publications in the area of alge-braic speci�cations are contributions for these tasks already. The general task according toFLEX - which is considered to be a long term project - is to provide generic language, tooland methodology development for KORSO and COMPASS in the spirit of development ofgeneric software systems with �exible extension and interconnection mechanisms.
A Computational l\/I'odel'for TROLL lightMartin Gogolla
Technische Universität Braunschweig, Informatik, Abt. Datenbanken
The object speci�cation language TROLL light is intended to be used for conceptual mod-eling of information systems. It is designed to describe the Universe of Discourse (UoD)as a system of concurrently existing and interacting objects, i.e., an object community.TROLL light is a dialect of the language TROLL. However, TROLL light is not just asubset of TROLL. For example, in TROLL light classes are understood as composite ob-jects having the class extension as subobjects. Therefore in contrast to TROLL an extranotion of class is not needed in TROLL light. This leads to a more orthogonal use ofobject descriptions. Over and above that, concepts like class attributes, meta-classes, orheterogeneous classes are inherent in TROLL light. Second, TROLL light incorporates aquery calculus providing a general declarative query facility for ob ject-oriented databases.
The �rst part of the talk introduces the various language concepts offered by TROLLlight. TROLL light objects have observable properties modeled by attributes, and thebehavior of objects is described by events. Possible object observations may be restrictedby constraints, whereas event occurrences may be restricted to speci�ed life-cycles. TROLLlight objects are organized in an object hierarchy established by sub-object relationships.Communication among objects is supported by event calling.
The second part of our paper outlines a simpli�ed computational model for TROLL light.After introducing signatures for collections of object types (or templates as they are calledin TROLL light) we explain how single states of an object community are constructed. Byparallel occurrence of a �nite set of events the states of object communities change. Theobject community itself is regarded as a graph Where the nodes are the object communitystates reachable from an initial state and the edges represent transitions between states.We shortly indicate how this operational semantics of TROLL light could be also expressedin terms of graph grammars and graph productions.
Temporal Logics and the Semantics of ConcurrentSystems
Ursula Goltz
Institut für Informatik, Universität Hildesheim, Germany
joint work with Ruurd Kuiper, Wojciech Penczek
For a design calculus for concurrent systems or, more speci�cally. for reactive systems, thefollowing components are being proposed:
0 a (logical) language for the property oriented speci�cation of systems,
0 a system description language to represent abstract and more concrete design speci-�cations,
0 models for concurrent systems which are used as semantic domains for both thelogical language and the system description language.
Based on such a framework, methods for the construction of correct systems may be de-
veloped.
A widely used language for the property oriented speci�cation of reactive systems aretemporal logics. For the description of reactive systems, process algebras are being used.Here a link between these two worlds is established by interpreting temporal logics onsemantic models which are being used for (causality based) semantics of process algebras.In particular, it is investigated which semantic equivalences are induced by various versionsof temporal logics.
U. Goltz, R. Kuiper and W. Penczek: Propositional temporal logics and equivalences. InW.R. Cleaveland, editor, Concur �92, volume 630 of Lecture Notes in Cornputer Science,pages 222-236. Springer-Verlag, 1992.
Types, Speci�cations, and Software DevelopmentFriedrich von Henke
Universität Ulm, Germany
We show how a notion of types as speci�cations can be evolved for both speci�cation in-the-small and speci�cations in-the-large. This requires an extension of the type system to
7
include dependent Sigma- and Pi-types, as provided, for instance, in the Extended Calculusof Construction of Luo. In this kind of setting, the semantics part of a speci�cation isexpressed by (higher-order) predicates which impose constraints on signatures; a realizationthen consists of an element of the signature type satisfying the constraints. Using thisframework, we indicate how to formalize both presentation and veri�cation of derivationsteps in the development of software from speci�cations.
5
Towards Correct, Efficient and ReusableTransformational Developments
Bernd Krieg-Brückner, Junbo Liu, Burkhart Wolff and Hui Shi
Universität Bremen, Germany
Transformational development attempts to achieve correct software by integrating the con-struction and veri�cation process. Re�nement is achieved by stepwise application of pre-conceived, correctness-preserving transformations. These transformations are applied bythe system with interactive guidance from the implementor and represent correspondingdesign decisions. Transformations are correct modulo applicability conditions. Transfor~mation can be Seen as a form of deduction, applying transformation rules in a kind of
rewriting process.
A semantic framework is called for that allows formal reasoning at the meta-level (cor-, rectness of rules, their composition, and tactics) in relation to the semantics of the objectlanguage. The framework envisaged tries to abstract from the semantics/logics of a par-ticular object language such that a set of rules need not be adapted and proved over andover again for each new object language. Proofs at the meta-level should be possible withsystem support to guarantee eventual complete correctness of the approach.
At the object-level, applicability conditions need to be established before a transformationrule can be applied. The requirement for ef�ciency calls for utmost automation, to relievethe user from super�ous and tedious interactive proofs and to allow composition of rules andthe use of rules in tactics without the need for intermediate user interaction. Techniquesfrom compiler construction can be applied to evaluate, and to incrementally re-evaluateafter application of a rule, such contextconditions in an efficient way. Context informationnot only encompass static semantic attributes and conditions such as those on typing orvisibility of identi�ers in the object language, but also e. g. the so-called "local theory" thatallows access to visible axioms. This information can be used in interactive or automatedproofs, but also in automatic simpli�cation or normalisation and to obtain parameters fora transformation rule implicitly.
One of the greatest challenges is the reusability of transformational developments. Onewould like to abstract from a particular development (let us say a sequence of transfor-mations) to a class of developments to enable reusability in a similar (but not identical)situation. This calls for powerful matching descriptions and powerful application tacticsto alleviate the need for the tedious application of single rules. Transformations are usedat the meta-level as well to develop optimised meta-programs (transformation tactics and
strategies). ReferencesKrieg-Briickner, B., Hoffmann, B. (eds.): iPROgram development by SPECi�cation andTRAnsformation: The PROSPECTRA Methodology, Language Family, and System. LNCS680 (1993).
Krieg-Bruckner, B., Lin, J., Wolff, B., Shi, H.: Towards Correctness, Efficiency andReusability of Transformational Developments. KORSO Report, FB3 Informatik, Univer-sitat Bremen, 1993. Extended Abstract in Proc. GI Tagung 1993, Informatik Fachberichte,
Springer ( 1993).
Initial Semantics For Speci�cation DevelopmentsMichael Löwe
Technische Universität Berlin, Germany
The talk summarises the framework for speci�cation development for speci�cations withloose semantics that has been worked out by Sannella, Wirsing, Broy, and others in thelast years: It provides a set of (horizontal) operators for building bigger speci�catic 'is fromsmaller pieces and a nice, straightforward, and very attractive notion of (vertical, re�ne-ment or development of speci�cations Wh1Cl1 is compatible with the horizontal operators.The talk provides �rst ideas how this framework can be carried over to speci�cations withinitial semantics, functorial re�nements and constructive horizontal operators. Construc-tive horizontal operators are those which do not only build classes of algebras from classesof algebras, but also provide a pointwise mapping which de�nes how individual objects inthe result class can be obtained from individual algebras in the argument classes. We showthat, in order to provide free-functor semantics for re�nements (which is also called initialsemantics for speci�cation developments), the operators "impose" and "derive" have to beadjusted slightly. "Impose" must be restricted to conditional equations (in�nite premisesare allowed) and "de five" must be extended by a restriction construction allowing only"interface"- reachable algebras as models. In a second step, w : sketch further adjustmentsof the operators to become constructive. llspecially the opera .ors "union" and "translate"are problematic in this respect. Finally we outline how these concepts can be generalised
9
to the parametric case of data type constructors and state the compatibility problem ofhorizontal and vertical steps as a major issue for future research.
Positive / negative conditional equational speci�cations(Constraints in built-in algebras and theories)
Klaus Madlener
Universität Kaiserslautern, Germany
(Joint work SFB 314 Project D4)
We study algebraic speci�cations given by �nite sets R of positive/ negative-conditionalequations with possible constraints in a built-in theory (i.e. universally quanti�ed �rst-order implications with a single equation in the succedent and a conjunction of positiveand negative (negated) equations and further constraints in the antecedent). The class ofmodels of such a speci�ca- tion R does not contain in general a minimum model in thesense that it can be mapped to any other model by some homomorphism. We presenta constructor-based approach for assigning appropriate semantics to such speci�cations.We introduce two syntactic restrictions: �rstly, for a condition to be ful�lled we requirethe evaluation values of the terms of the negative equations (contraints) to be in theconstructor sub-universe which contains the set of evaluation values of all constructor
ground terms; secondly, we restrict the constructor equations to have "Horn"-form andto be "constructor-preserving". A reduction relation for R is de�ned, which allows togeneralize the fundamental results for positive�con� ditional rewrite systems, which doesnot need to be noetherian or restricted to ground terms, and which is monotonic w.r.t.consistent extension of the speci�- cation. Under the assumption of con�uence, the factoralgebra of the ground term algebra modulo the congruence of the reduction relation is aminimal model which is the minimum of all models that do not identify more constructorground terms than necessary. To achieve decidability of reducibility we de�ne several
( kinds of compatibility of R with a reduction ordering and present critical-pair tests for thecon�uence of the reduction relation. Consequences to hierarchical- rewriting and inductive-proofs are discussed.
10
Rewriting Logic as a Logicaland Semantic Framework
Narciso Marti-Oliet and José Meseguer
SRI International, and
Center for the Study of Language and Information�Stanford University
Rewriting logic [2] is proposed as a. logical framework in which other logics can be repre-sented, and as a semantic framework for the speci�cation of languages and systems.
Using concepts from the theory of general logics [1], representations of an object logic L ina framework logic .77 are understood as mappings C �> .7-' that translate one logic into theother in a conservative way. The ease with which such maps can be de�ned for a numberof quite different logics of interest is discussed in detail.
Regarding the different but related use of rewriting logic as a semantic framework, thestraightforward way in which very different models of concurrency can be expressed anduni�ed within rewriting logic is emphasized and illustrated with examples such as concur-rent object-oriented programming and CCS. The relationship with structural operationalsemantics, which can be naturally regarded as a special case of rewriting logic, is alsodiscussed by means of examples.
References
[1] J. Meseguer, General Logics, in: H.-D. Bbbinghaus et al. («=ds.), Logic Colloqui-..'m�87,North-Holland, 198 '9, pages [275-329.
[2] J. Meseguer, Condisional Rewriting Log ic as a Uni�ed Mod.J of Concurrency, Theoret-ical Computer Science 96, 1992, pages '.'3�155.
An Algebraic Approach To Program DerivationBernhard Möller
Universität Augsburg, German P5��
The transformational or calculational apprcach to program devr lopment has by now a longtradition. There one starts from a (possibly non-executable) specificatiori and transforms
ll
it into a (hopefully e�icient) program using semantics-preserving rules. Many speci�ca-tions and derivations, however, suffer from the use of lengthy, obscure and unstructuredexpressions involving formulae from predicate calculus. This makes writing tedious anderror-prone and reading difficult. Frequently, for the sake of completeness, long and boringtrivial assertions have to be included. Moreover, the lack of structure leads to large searchspaces for supporting tools.
The aim of modern algebraic approaches is to make program speci�cation and calculationmore compact and perspicuous. They attempt to identify frequently occurring patterns andto express them by operators satisfying strong algebraic properties. This way the formulasinvolved become smaller and contain less repetition, which also makes their writing saferand speeds up reading (once one is used to the operators). In addition, the search spaces formachine assistance become smaller, since the search can be directed by the combinationsof occurring operators. If one succeeds in finding equational laws, proof chains rather thancomplicated proof trees result as another advantage. Moreover, frequently aggregationsof quanti�ers can be packaged into operators; an equational law involving them usuallycombines a series of inference steps in pure predicate calculus into a single one.
We illustrate these ideas by treating some sorting problems within an algebra of formallanguages. Essential operators are (besides the usual set theoretic ones) concatenation,join (i.e. glueing upon a one�letter overlap) and shuffle. Based on the join we de�ne thepath closure of a binary relation which, for a partial order, is the set of all ordered wordsover the underlying alphabet. The set of permutations of a word is de�ned as the set ofall possible shuffles of its letters. Based on these concepts, the speci�cation of the sortingproblem is straightforward. We give a number of algebraic properties of path closure,shuffle and permutation set which capture the decompositions involved in various sortingalgorithms. Based on these properties we derive mergesort, quicksort and an algorithm forconstructing sorted binary trees.
Different sets of operators have been used to derive algorithms on graphs, pointer struc-tures and binary search trees. A long term goal is the construction of a database of suchoperators, enhanced by indexing and external representation using informal language re-ferring to the intuitive meaning of the operators. Such a component would serve as a�speci�er�s workbench� as a front end to a formal development tool.
Action Semantics
Peter D. Mosses
Computer Science Dept., Aarhus Univ., Denmark
Action Semantics is a framework that combines some of the best features of denotational se-
mantics, operational semantics, and algebraic speci�cations. The combinator-based action
12
notation provided by the framework appears to solve the modularity problems of previoussemantic description techniques, and experiments have shown that action semantic de-scriptions scale up smoothly from simple pedagogical examples to practical programminglanguages.
In this talk, action semantics is introduced by showing how it can be used to describea fragment of Standard ML. The intended interpretation of the required part of actionnotation is explained. The syntax of the described language is then extended with themain constructs of Concurrent ML, and it is shown how the semantic description can beextended to the new constructs � without changing the original semantic equations at all!Finally, the fundamental operational concepts underlying action notation are discussed,and it is argued that the asynchronous communication primitives provided by the standardaction notation are more appropriate than synchronous ones would be �� even for describinglanguages which, like CML, are based on the notion of synchronization.
On the Correctness of Modular SystemsM. Navarro, F. Orejas, A. Sanchez
UPC Barcelona, Spain
In modular software design it is expected that the correctness of an implementation of a.complete system will be a consequence of the correctness of each module. Very often, thisproperty has been associated to the satisfaction of the so-called horizontal and verticalcomposition properties, both at the speci�cation and at the programming language levels.
In this presentation, we introduce an abstract framework that allow us to represent, asspeci�c instances, most concrete modular frameworks. In particular, the framework pre-sented is "parameterized" by the speci�cation and programming language formalisms, bythe semantic constructs associated to modules and by the behavioural equivalence relationused to de�ne module re�nement.
In this framework, it is shown that, to achieve modular correctness, it is sufficient thatthe given programming language satis�es a property of "stability" with respect to thegiven behavioural equivalence relation. In particular, modular correctness is shown tobe independent of the satisfaction (or not) of the horizontal and vertical compositionproperties at the speci�cation level.
13
Speci�cation and Programming: Where is theDifference?
Peter Padawitz
Universität Dortmund, Germany
The talk deals with recent developments of Expander, a prototyping system for declar-ative programs and the data types they use. The system processes programs, given asHorn clause axioms, and requirements to programs, given as Gentzen clauses of the formgs<:hs where gs and hs are goal sets. A goal set is a universally quanti�ed disjunctionof existentially quanti�ed conjunctions of atomic formulas. An Expander proof of gs<=hsconsists in the concurrent strengthening of gs and weakening of hs until the point wheresyntactical criteria imply that hs "subsumes" gs. We may then conclude that gs<=hs isvalid with respect to the initial semantics of the underlying data type speci�cation.
Rules applied in the proof process are resolution of atoms, rewriting of terms and narrow-ing transformations, each followed by automatic simpli�cations of the current goal sets.So far, simpli�cation steps are partial function and predicate evaluation, constructor equa-tionhisplitting, beta-reduction and continuation passing. �They stem from programming orcompilation techniques and thus decrease the gap between speci�cation and programmingin that, on the veri�cation side, they enhance the transparency and ef�ciency of proofs,while, on the prototyping side, they improve the executability of speci�cations.
Parameterization or Polymorphism or Both?P. Pepper
Fachbereich Informatik, Technische Universität Berlin, Germany
In algebraic speci�cation languages and in functional programming languages, two com-peting concepts have evolved for increasing the �exibilty of (strong) typing mechanisms.One is usually referred to under the buzzword "parameterization", and the other underthe buzzword "polymorphism". Since both concepts are complementary in their respective�strengths and weaknesses, we try here to integrate them into a uni�ed framework (that isin�uenced by the type classes of Haskell).
On the syntactic level we employ the concept of "origins" (that is already used in theOpal compiler) to cope with the resulting type analyses; the goal here is that most of thetraditional techniques can still be used. On the semantic level we aim at a solution thatis as simple and 0) thogonal as pOSSibl«.'. Here the concept of comma categories that has
14
already been successfully used for the description of heterogeneous algebras s appears tobe a promising approach. The talk reports about ongoing research in this direction.
Modelling and Speci�cation of Reactive SystemsAxel Poigné
GMD Bonn, Germany
We present a general framework for event-based behaviour and its speci�cation in partic-ular. Our main observation is that a logic of events is needed as well as a logic of actions.The former prescribes in �ne detail how computations proceed while the latter providesgeneric scripts for events to happen.
The work is based on a novel, generic model of event-based behaviour, referred to as eventautomata.The requirement is that every state records the events which have occurred sofar an that transitions correspond to the occurrence of a unique event.
Our framework provides a new semantic basis for the theory of information systems as pro-posed by the IsCore ring where �processes� are considered as the basic semantic frameworkto deal with the dynamic behaviour of objects.
Speci�cation of Concurrent Object SystemsHorst Reichel
Technische Universität Dresden, Germany
Two aspects of specifying concurrent object systems are discussed:
1. Structuring objects (describing the internal structure of objects up to some point);
2. System structure (describing the global state of a concurrent object system and its
possible changes).
By means of the projective universal property of object types, which makes object instancesto �nal co-algebras, one has a framework to de�ne and study object building operationslike sequential composition and parallel composition. In the second part it is skeched how
15
the Rewriting Logic of J. Meseguer can be used to specify the behavior of concurrent objectsystems. As a speci�c topic the addressing of messages to objects is discussed.
Speci�cation and Veri�cation of Modular Systems
Wolfgang Reif
Institut für Logik, Komplexität und DeduktionssystemeUniversität Karlsruhe, Germany
We present the KIV approach �to speci�cation and veri�cation of modular sequential sys-tems. KIV stands for Karlsruhe Interactive Veri�er ([HRS 90, Re 92a], and it is an ad-vanced support tool for correct software development. The basic motivation of this ap-proach is to provide an economic perspective of correct software development. Two majorproblems are the enormous complexity of the deduction problems that are involved in ver-ifying large systems, and the problem of scaling up solutions in the small to solutions inthe large.
To overcome these problems we adopt a strict decompositional design discipline leading tomodular software systems with compositional correctness. This is achieved by restrictingthe designer�s freedom to hierarchy persistent structured specifications and hierarchy re-specting implementations. As a result the correctness of large systems can be completelyreduced to the correctness of its modules. The veri�cation effort for a modular systemthen becomes linear in the number of its modules ([Re 92b]).
Single modules are veri�ed by translating them into a set of proof obligations formulatedin a logic of programs. The set of proof obligations is shown to be necessary and suf�cientfor the correctness of the module ([Re 92c]). These proof obligations are tackled by aspeci�c proof method that has been implemented in the KIV system. Finally, we reporton a number of case studies with the system, and give some statistical performance andproductivity results.
References
[HRS 90] M. Heisel, W. Reif, W. Stephan : Tactical Theorem Proving in Program Veri�-cation. 10th International Conference on Automated Deduction, Kaiserslautern,FRG, Springer LNCS 1990.
[Re 92a] W. Reif : The KIV-System: Systematic Construction of Verified Software.11th Conference on Automated Deduction, Albany, NY, USA, D. Kapur (ed.),Springer LNCS 1992.
16
[Re 92b] W. Reif : Veri�cation of Large Software Systems. Conference on Foundations of Software Technology and Theoretical Computer Science, New Dehli, India,
Shyamasundar (ed.), Springer LNCS 1992.
[Re 92c] W. Reif: Correctness of Generic Modules. Symposium on Logical Foundationsof Computer Science, �Logic at Tver�, Tver, Russia, Nerode, Taitslin (eds.),Springer LN CS 1992.
Static and logical correctness conditions in formaldevelopment of modular programs
Don Sannella
University of Edinburgh
Formal program development by top�down stepwise re�nement. involves (-reation of a se-quence of partial solutions, commencing with the origina.l speci�cation of require1nent.s andconcluding with a11 executable program. Each successive version must satisfy certain cor-rectness conditions with respect t.o the previous version, including both �static� conditionsrequiring the newer version to de�ne objects having the same names and same types as theolder version, and �logical� conditions (so-called �proof obligations�) requiring the de�ni-tions in the newer version to satisfy properties (e.g. axioms) required by the older version.This paper studies the static and logical correctness conditions that arise in the formaldevelopment of modular software systems in a framework such as that of Extended ML.Modules are equipped with explicit interfaces, may have hierarchical structure, and maybe parameterised; each of these aspects of modularity plays an important and distinct rolein formal development of software �in the large�. A formal system for development is
_ given in which these static and logical conditions are explicit, a.nd it is shown that theseconditions suffice to ensure that any program produced by this means satis�es the originalspeci�cation.
Ordering Isomorphism Classes of Semantic DomainsGunther Schmidt
Universität der Bundeswehr München, Germany
The idea of constructing semantic domains using sprouts [1], has been elaborated coveringexplicit domains, natural extensions, sum, product, function space and recursively de�neddomains. Domains with sprouts are, as usual, considered modulo isomorphism. The re-lation A <: B is de�ned to express the existence of an adjoint pair from A to B. Forthe solutions of recursive domain equations to be uniquely determined, it is necessary that<: is an ordering of the isomorphism classes of semantic domains. While some categoriesproposed do not have this property, we prove such a result for the category of domains withsprouts. They constrast to consistently complete cpos, which restrict the cpo but admitall continuous functions. For domains with sprouts the continuous functions are restri('tedto those which are in addition sprout-respecting. We also prove that. in these categoriesthe ordering <:: can fully be represented by the system of approximations of the domainin the different sprouts.
[1] Describing semantic domains with spronts. ACTA INFORMATICA 27 (1989) 16 - 25
Formalized Developments in Deva
Martin Simons and Stefan J ähnichen
TU Berlin / GMD First.
Deva is a platform designed to provide formal support for rigorous developments; formalmeaning that the correctness of a development has to be checkable by a machine. In arigorous development w such as a VDM re�nement or a Squiggol derivation one is notforced to provide that amount of detail required by formality: proofs of proof obligationsmay be omitted and assumptions may be left. implicit. In order to stay on the formal, i.e.machine veri�able side, yet retain the �sketchiness� of the rigorous side without whichformal developments seem unrealistic -��-� it would be nice to have a formal framework inwhich �sketches� of developments may be expressed. An implementation of the formalismwould then �ll in the necessary details. Deva is a step into that direction. Basically, Devais a higher�order typed /\-calculus with dependent types in the tradition of the AUTOMATHfamily of languages, the Calculus of Construction, or the Edinburgh Logical Framework.It is equipped with an implicit level to allow sketches of developments to be expressed.The talk introduced the motivation behind Deva, reported on the tool support �� whichhas been used to develop an impressive range of Deva formalizations �� and illustrated by
18
an example drawn from the area of transformational algorithm design (Bird�s maximumsegment sum derivation) that a Deva. formalization of that m'g01�0us development resemblesclosely in size and shape the original one.
Recent Results on Actor Semantics
Carolyn Talcott
Stanford University
joint work with Gul Agha, University of Illinois, Ian Mason, Stanford University,Scott Smith, Johns Hopkins University
Actors are reactive independent agents that communicate via message passing. In this talkwe report on our investigations of the mathematical properties of a.ct.or systems. We beginby presenting an actor language that serves as a concrete example for study. This languageis the extension of a simple higher-order functional language with primitives for actors: cre-ation; communication; and change of behavior. We de�ne a notion of actor system, and a.set of labelled transitions on actor systems. This gives an operational semantics. We thenconsider two notions of equivalence of actor expressions and systems: the �rst is a formof observational / testing equivalence; the second is a form of trace equivalence called inter-action equivalence. In the full paper [soon available by request tp [email protected]]many laws of equivalence are given. In addition some general methods for establishingequivalence are developed. The study of expression equivalence is a. step towards estab-lishing a sound semantic basis for implementation of such languages. The study of actorsystem equivalence is a step towards developing a calculus of actor systems.
Timed Testing of Concurrent SystemsWalter Vogler
Institut für Mathematik, Universität Augsburg, Germany
My concern are timing considerations for concurrent systems where the time needed for theindividual actions is not known beforehand; it has long been suspected that partial ordersemantics is useful here. I develop a suitable testing scenario to study this idea. Withsome view of timed behaviour, I can con�rm that interval semiword semantics, a specialpartial order semantics, is indeed useful. With another view, the testing scenario leads totimed-refusal-trace semantics, where no relation to partial order semantics is obvious.
19
Untyped Constrained Lambda Calculus
Martin Wirsing
Institut für Informatik, Universität München
joint work with John N. Crossley, Monash University, Melbourne, Australia and LuisMandel, TU München, Germany
The aim of the present work is to develop an enhancement of the traditional untypedlambda-Calculus in a general setting.
For that purpose terms of the form {C}M are introduced where {C} denotes a constraintand M another (possibly constrained) lambda term, and rules are added for describing theinteraction between constraints and lambda terms. The constraints are used in two ways:on one hand, the passive use of a constraint {C} in {C }M restricts the universe of validityof M; on the other hand, the active use of an inference that is made by the constraint solverfrom the constraint {C} causes the replacement of subterms in the target term M.
The constraint language is considered as a bla(:k�box. For different. solvers (over possiblydifferent domains) we get different instantiations of the constraint la1nl)da�(°al('ulus. Typ-ical examples for constraint domains are linear equations, finite domains, logic programsand also assignment constraints. For constraints which admit only unique solutions the cal-culus is locally con�uent i.e. it satis�es the Weak Church Rosser property. A denotationalsemantics can be given in the usual way based on the solution of a domain equation.
Categorical Concepts for Parameterized PartialSpeci�cations
Uwe Wolter
TU} Berlin, GermanyJoint Work with Ingo Cla�en and Martin Große-Rhode
We show that canonical �nite limits are the underlying categorical structure of algebraswith strict partial operations and conditional existence equations.
Speci�cations are shown to be equivalent to freely generated categories with canonical�nite limits and partial algebras are functors preserving these �nite limits. Further alsospeci�cation morphisms turn out to be �nite limit preserving functors between the �nitelimit categories freely generated by speci�cations.
20
Using this categorical description we obtain straigthforwardly a theory of parameterizcdspeci�cations with free semantics and amalgamation thus providing a partial algebra se-mantics for speci�cation languages like ACT ONE, ACT TWO,. . . .
�21
Dagstuhl-Seminar 9321 List of Participants
Egidio Astesiano Hans-Dieter EhrichUniversité di Genova TU BraunschweigDipartimento di Matematica lnstitut für ProgrammiersprachenVia L.B. Alberti 4 und InformationssystemeI-16132 Genova Padawi Postfach 3329
Italy D-38106 [email protected] Germanytel.: +39-10-353-80 22 [email protected]
tel.: +49-531-391-3271Christoph BeierleIBM Germany Hartmut EhrigScientific Center Heidelberg ' TU BerlinInstitute for Knowledge Based Systems Fachbereich 20 InformatikPostfach 10 30 68 Franklinstr. 28-29W-69120 Heidelberg D-10587 BerlinGermany [email protected] [email protected].: +49-6221-59-4393 tel.: +49-30-314-7 35 10
Rudolf Berghammer Wolfgang EverlingUniversität Kiel Universität BonnInst. für lnformat�< und Prakt. Mathematik Institut für InformatikHaus II Römerstr. 164Preusserstraße 1-9 D-53117 Bonn24105 Kiel GermanyGermanyrub@ Informatik.uni-kieI.d400.de Harald Ganzingertel.: +49-431�56 O4 86 MPI - Saarbrücken
Max-Planck-Institut für InformatikMichel Bidoit Im StadtwaldEcole Normale Superieure D-66123 SaarbrückenDepartement de Mathématiques Germany45 Rue d�UIm [email protected] Paris Cedex O5 tel.: +49-681-302-53 [email protected] Martin Gogollatel.: +33�1-4432-2058 TU Braunschweig
Informatik Abt. DatenbankenHeinz Brix Postfach 3329SIEMENS AG - ZFE BT SE 12 D-38106 BraunschweigZentralabt. Forschung und Entwicklung GermanyOtto-Hahn-Ring 6 [email protected] München tel.: +49-531-391-31 09
[email protected] Ursula Goltztel.: +49�89-636-44627 Universität Hildesheim
Institut für InformatikAndrea Corradini Marienburger Platz 22Universit �a di Pisa D�31141 HildesheimDipartimento di lnformatica GermanyCorso Italia 40I-56100 Pisa Gerhard Goosltaly Universität [email protected] (SMD-Forschungsstelletel.: +39�50-51 O2 21 Vincenz-Prießnitz-Str. 1
D-76128 Karlsruhe
[email protected].: +49�721-66 22 66
Friedrich W. v. Henke Klaus MadlenerUniversität Ulm Universität KaiserslauternFakultät für Informatik FB InformatikJames-Franck-Ring Postfach 30 49D-89081 Ulm D-67653 Kaiserslautern
Germany [email protected] [email protected]�kl.detel.: +49-731 502 4120 tel.: +49-631-205-2268
Günter Hotz Tom MaibaumUniversität des Saarlandes Imperial College of ScienceFachbereich 14a - Informatik Department of ComputingPostfach 15 11 50 180 Queen's GateD-66041 Saarbrücken London SW7 2BZGermany Great [email protected] [email protected].: +49-681-302 2414 tel.: +44-71-589-51 11 Ext. 5001/5098
Klaus P. Jantke Jose MeseguerTechnische Hochschule Leipzig SRI InternationalSektion Mathematik/Informatik Department of Computer ScienceKarl-Liebknecht-Straße 132 333 Ravenswood Ave.O-04251 Leipzig Menlo Park CA 94025Germany USAjantke @ informatik.th�leipzig.de meseguer@ csl.sri.comtel.: +49-341-39 28-4 26
Peter MossesBernd Krieg-Brückner Aarhus UniversityUniversität Bremen Computer Science DepartmentFachbereich 3 Mathematik/Informatik Ny MunkegadePostfach 33 04 40 DK-8000 Aarhus CD-28359 Bremen DenmarkGermany 1 . [email protected]
tel.: +45-86127188Michael LöweTU Berlin Fernando OrejasFachbereich20 Informatik Universidad Politécnica de Catalu�aFranklinstr. 28-29 Dept. L.S.I.D-10587 Berlin Pau Gargallo 5Germany E-08028 Barcelona
SpainJacques Loeckx [email protected]ät des Saarlandes tel.: +34-3-401 70 18Fachbereich 14 � InformatikPostfach 15 11 50 Peter PadawitzD-66041 Saarbrücken Universität DortmundGermany Fachbereich [email protected] Postfach 50 05 00tel.: +49-681-302 3435 D-44221 Dortmund
Germanypeter@ ls5.informatik.uni-doertmund.detel.: +49-231-755-5108 /5101
Bernhard MöllerUniversität Augsburg Francesco Parisi-PresicceInstitut für Mathematik Universitä degIiStudi di l�AquilaUniversitätsstr. 2 Dipt. di MathematicaD-86159 Augsburg Via Vetoio 33Germany :-6|7100 L�AquiIa
ta yparisi @aquila.infn.ittel.: +39-862-433 127
Peter Pepper Martin SimonsTU Berlin TU BerlinFachbereich 20 Informatik Fachbereich 20 InformatikFranklinstr. 28-29 Franklinstr. 28-29D-10587 Berlin D-10587 Berlin
Germany [email protected]�berlin.de [email protected].: +49-30-314-7 34 70 tel.: +49-30-31 47 32 30
Axel Poigné Carolyn TalcottGesellschaft für Mathematik und Stanford UniversityDatenverarbeitung mbH Dept. of Computer ScienceSchloß Birlinghoven Stanford CA 94305-4115Postfach 13 16 USAD-53731 St. Augustin ' [email protected] tel.: [email protected].: +49-2241-142440 Walter Vogler
Universität AugsburgHorst Reichel Institut für MathematikTU Dresden Universitätsstr. 2Institut Theoretische Informatik D-86159 AugsburgMommsenstr. 13 GermanyO-01062 Dresden [email protected] '[email protected] Martin Wirsingtel.: +49�351-4575-548 Universität München
Institut für InformatikWolfgang Reif Leopoldstraße 11 BUniversität Karlsruhe D-80802 Münchenlnsitut für Logik Komplexität und Germany lDeduktionssysteme r [email protected] Fasanengarten 5 tel.: +49-89-2180�6318 (6317)D-76128 KarlsruheGermany Uwe [email protected] TU Berlintel.: +49-721-608-4245 Fachbereich 20 Informatik
Sekr. 6-1Donald T. Sannella Franklinstr. 28-29University of Edinburgh D-10587 BerlinDept. of Computer Science GermanyKing�s BuildingMayfield RoadEdinburgh EH9 3JZGreat Britain
[email protected].: +44 31 650 51 84
Gunther SchmidtUniversität der Bundeswehr MünchenFakultät für Informatik
Werner-Heisenberg-Weg 39D-85577 NeubibergGermany . t 1' .schmidt @ informatik.unibw-muenchen.detel.: +49-89 6004 24 49/ 22 63
Zuletzt erschienene und geplante Titel:
J. von zur Gathen, M. Karpinski, D. Kozen (editors):Algebraic Complexity and Parallelism, Dagstuhl-Seminar-Report; 41; 20.07.-24.07.92 (9230)
F. Baader� J. Siekmann, W. Snyder (editors):6th International Workshop on Unification, Dagstuhl-Seminar-Report; 42; 29.07.�31.07.92 (9231)
J.W. Davenport, F. Krückeberg, R.E. Moore, S. Rump (editors):Symbolic, algebraic and validated numerical Computation, Dagstuhl-Seminar�Report; 43; 03.08.-07.08.92 (9232)
R. Cohen, R. Kass, C. Paris, W. Wahlster (editors):Third International Workshop on User Modeling (UM�92), Dagstuhl-Seminar-Report; 44; 10.-13.8.92 (9233)
R. Reischuk, D. Uhlig (editors):Complexity and Realization of Boolean Functions, Dagstuhl-Seminar-Report; 45; 24.08.-28.08.92(9235)
Th. Lengauer, D. Schomburg, M.S. Waterman (editors):Molecular Bioinformatics, Dagstuhl-Seminar-Report; 46; 07.09.-11.09.92 (9237)
V.R. Basili, H.D. Rombach, R.W. Selby (editors):Experimental Software Engineering Issues, Dagstuhl-Seminar-Report; 47; 14.-18.09.92 (9238)
Y. Dittrich, H. Hastedt, P. Schete (editors):Computer Science and Philosophy, Dagstuhl-Seminar-Report; 48; 21 .09.-25.09.92 (9239)
R.P. Daley, U. Furbach, K.P. Jantke (editors):Analogical and Inductive Inference 1992 , Dagstuhl-Seminar-Report; 49; 05.10.-09.10.92 (9241)
E. Novak, St. Smale, J.F. Traub (editors):Algorithms and Complexity for Continuous Problems, Dagstuhl-Seminar-Report; 50; 12.10.-16.10.92 (9242)
J. Encarnacao, J. Foley (editors):Multimedia - System Architectures and Applications, Dagstuhl-Seminar-Report; 51; 02.11.-06.1 1.92 (9245)
F.J. Rammig, J. Staunstrup, G. Zimmermann (editors):Self-Timed Design, Dagstuhl-Seminar-Report; 52; 30.11.-04.12.92 (9249)
B. Courcelle, H. Ehrig, G. Rozenberg, H.J. Schneider (editors):Graph-Transformations in Computer Science, Dagstuhl-Seminar-Fleport; 53; 04.01.-08.01.93(9301)
A. Arnold, L. Priese, R. Vollmar (editors):Automata Theory: Distributed Models, Dagstuhl-Seminar-Report; 54; 11.01 .-15.01 .93 (9302)
W. Cellary, K. Vidyasankar, G. Vossen (editors):Versioning in Database Management Systems, Dagstuhl-Seminar-Report; 55; 01.02.-05.02.93(9305)
B. Becker, R. Bryant, Ch. Meinel (editors):Computer Aided Design and Test , Dagstuhl-Seminar-Report; 56; 15.02.-19.02.93 (9307)
M. Pinkal, R. Scha, L. Schubert (editors):Semantic Formalisms in Natural Language Processing, Dagstuhl-Seminar-Fleport; 57; 23.02.-26.02.93 (9308)
W. Bibel, K. Furukawa, M. Stickel (editors):Deduction , DagstuhI-Seminar-Report; 58; O8.03.-12.03.93 (9310)
H. Alt, B. Chazelle, E. Welzl (editors):Computational Geometry, Dagstuhl-Seminar-Report; 59; 22.03.-26.03.93 (9312)
H. Kamp, J. Pustejovsky (editors):Universals in the Lexicon: At the Intersection of Lexical Semantic Theories, Dagstuhl-Seminar-Report; 60; 29.03.-02.04.93 (9313)
W. Strasser, F. Wahl (editors):Graphics & Robotics, Dagstuhl-Seminar-Report; 61; 19.04.-22.04.93 (9316)
C. Beeri, A. Heuer, G. Saake, S. Urban (editors):Formal Aspects of Object Base Dynamics , Dagstuhl-Seminar-Report; 62; 26.04.-30.04.93 (9317)
R. V. Book, E. Pednault, D. Wotschke (editors):Descriptional Complexity, Dagstuhl-Seminar-Report; 63; 03.05.-07.05.93 (9318)
H. Ehrig, F. von Henke, J. Meseguer� M. Wirsing (editors):Specification and Semantics, Dagstuhl-Seminar-Report; 64; 24.05.-28.05.93 (9321)
M. Droste, Y. Gurevich (editors):Semantics of Programming Languages and Algebra, Dagstuhl-Seminar-Report; 65; 07.06.-1 1 .0693 (9323)
Ch. Lengauer, P. Quinton, Y. Robert, L. Thiele (editors):Parallelization Techniques for Uniform Algorithms, Dagstuhl-Seminar-Report; 66; 21 .06.-25.06.93(9325)
G. Farin, H. Hagen, H. Noltemeier (editors): jGeometric Modelling, Dagstuhl-Seminar-Report; 67; 28.06.-02.07.93 (9326)
Ph. Flajolet, R. Kemp, H. Prodinger (editors):"Average-Case"-Analysis of Algorithms, Dagstuhl-Seminar-Report; 68; 12.07.-16.07.93 (9328)
J.W. Gray, A.M. Pitts, K. Sieber (editors):Interactions between Category Theory and Computer Science, Dagstuhl-Seminar-Report; 69;19.07.-23.07.93 (9329)
D. Gabbay, H.-J. Ohlbach (editors):Automated Practical Reasoning and Argumentation, Dagstuhl-Seminar-Report; 70; 23.08.-27.08.93 (9334)
A. Danthine , W. Effelsberg, O. Spaniol, (editors):Architecture and Protocols for High-Speed Networks, Dagstuli.-Seminar-Report; 71; 30.08.-03.09.93 (9335)
R. Cole, E. W. Mayr, F. Meyer a.d.Heide (editors):Parallel and Distributed Algorithms, Dagstuhl-Seminar-Report; 72; 13.09.-17.09.93 (9337)
V. Marek, A. Nerode, P.H. Schmitt (editors):Non-Classical Logics in Computer Science, Dagstuhl-Seminar-Report; 73; 20.-24.09.93 (9338)
A. M. Odlyzko, C. P. Schnorr, A. Shamir (editors):Cryptography, Dagstuhl-Seminar-Report; 74; 27.09.-01.10.93 (9339)
J. Angeles, G. Hommel, P. Kovécs (editors):Computational Kinematics, Dagstuhl-Seminar-Report; 75; 1 1 .10.-15.10.93 (9341)
T. Lengauer, M. Sarrafzadeh, D. Wagner (editors):Combinatorial Methods for Integrated Circuit Design, Dagstuhl-Seminar-Report; 76; 18.10.-22.10.93 (9342)
S. Biundo, R. Waldinger (editors):Deductive Approaches to Plan Generation and Plan Recognition, Dagstuhl-Seminar-Report; 77;25.10.-29.10.93 (9343)
P. Gritzmann, D. Johnson, V. Klee, Ch. Meinel (editors):Counting Issues: Theory and Application, Dagstuhl-Seminar-Repo; t; 78; 06.12.-10.12.93 (9349)
B. Endres-Niggemeyer, J. Hobbs, K. Sparck Jones (editors): hSummarizing Text for Intelligent Communication, Dagstuhl-Seminar-Report; 79; 13.12.-17.12.93(9350)
