Bonas (France), 13th-14th September 1999ParticipationAbstracts of Talks

Abstracts of Talks


Horst Reichel: KAN Extensions used as Definition and Proof Schemata

Horst Reichel presented on-going work towards a uniform categorical approach to data and process specifications. It is shown that injective (left) Kan extensions, respectively projective (right) Kan extensions, can be used in a very natural way to represent parametric inductive data type definitions, respectively parametric coinductive process type definitions. Injective and projective Limits as special cases of Kan extensions represents the non-recursive cases of data respectively process types.

Analogously to the weakening of limits to sketches we weaken Kan extensions to (Kan) sketches. It turns out that Kan sketchable categories are not sufficient to represent those model classes of parametric data and process types that appear naturally in software specifications as functor categories constraint by conjunctions of projective and injective Kan sketches.

However, the use conditionally (nested) and conjunctively composed systems of Kan sketches leads to an extremely expressive specification formalism, called nested sketches. One can show that the Hennessy-Milner Logic and that primitive-recursive functions are specific instances of the term model of the corresponding nested sketch specifying image finite labeled transition systems, respectively natural numbers.


Peter Padawitz: From (co)algebras and behavior realizations to swinging types

Functor algebras and coalgebras interpreting data type specifications are usually determined by one of two functor schemas, F and G. F is polynomial and bicontinuous. Initial F-algebras consist of finite terms, final F-coalgebras consist of finite and infinite terms. The terms are built up of constructors that form a signature SIG. F-algebras are SIG-algebras. By "inverting" the constructors of SIG one obtains a signature DSIG of destructors such that F-coalgebras are DSIG-algebras. G starts out from a destructor signature SIG' of "attributes" and "methods" and thus involves infinite products. The final G-coalgebra consists of tuples of "context" functions composed of the attributes and methods. If all attributes and methods are unary, the function tuples boil down to (infinite) terms, and the final G-coalgebra agrees with a final F-algebra.

The categorical approach provides guidelines for separating constructors from destructors and other defined functions of a swinging specification SP [2]. The final SP-model may include finite (term) denotations of infinite objects, but usually does not cover all elements of a final G-coalgebra unless the latter is the final realization of the initial SP-model's behavior. This holds true and the final SP-model is embedded in the final G-coalgebra if SP is behaviorally consistent. These relationships between coalgebras and SP-models deal only with the functional part of SP. For interpreting predicates one may employ powerset functors, but here the descriptive or methodological benefit from using category theory instead of simple set theory is questionable.

More on the talk can be found in Section 5 of [2]. The slides of the talk can be downloaded from http://ls5.cs.uni-dortmund.de/~peter/WGSlides.ps.gz.

[1] P. Padawitz, Sample Swinging Types, http://ls5.cs.uni-dortmund.de/~peter/BehExa.ps.gz

[2] P. Padawitz, Swinging Types = Relations, Functions, and Transition Systems, http://ls5.cs.uni-dortmund.de/~peter/Rome.ps.gz


Bart Jacobs: Coalgebras and Temporal Logic

We introduce a temporal logic for coalgebras. Nexttime and lasttime operators are defined for a coalgebra, acting on predicates on the state space. They give rise to what is called a Galois algebra. We illustrate the usefulness of these operators in the (coalgebraic) specification of classes. Galois algebras form models of temporal logics like Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). We show how the mapping from coalgebras to Galois algebras turns out to be functorial, yielding indexed categorical structures.

Reference: The temporal logic of coalgebras via Galois algebras


Peter Gorm Larsen: Proof Rules for Combining Recursion and Underdeterminedness

The model-oriented formal method known as VDM uses a specification language called VDM-SL. The dynamic semantics for this language is solely defined from a model-theoretic point of view. Thus, it is not at all clear that the defined semantics is appropriate for deriving proof rules which reflect the semantics. This presentation focussed on challenging areas for proof rules for VDM-SL. It was illustrated how the combination of underdeterminedness and recursion can be provided with a collection of proof rules and this was illustrated by a few small examples with variations of the factorial function.

The presentation was based mainly on: Semantics of Under-determined Expressions.


Egon Börger: Modeling the Java Virtual Machine using ASM composition principles

We provide concise abstract (ASM) code for running the Java Virtual Machine (JVM). First we define a fast JVM as platform for provably correct Java compilation, exhibiting a general compilation scheme of Java programs to JVM code. These definitions, together with the definition of an abstract interpreter of Java programs, allow us to prove that any compiler that satisfies some natural conditions compiles Java code correctly. As a by-product we provide a challenging realistic case study for mechanical verification of a compiler correctness proof. We have also validated our JVM and compiler specification through experimentation with ASMGofer which has been developed during this summer by Joachim Schmid and Wolfram Schulte.

The modularity of our definitions for Java, the JVM and the compilation scheme exhibit orthogonal language, machine and compiler components, which fit together and provide the basis for a stepwise and provably correct design-for-reuse. We extend the above JVM to a defensive JVM which can be used safely as Java independent platform for executing arbitrary byte code. We then separate the bytecode verification machine part from the executing part and obtain in such a way a model for the bytecode verifier. As last step we integrate this bytecode verifier into a loading machine which together with the executing ASM provides a full JVM model. The construction makes use of new composition techniques for building complex ASMs out of simpler ones.

  1. Börger E., Schulte W., Programmer friendly modular definition of the semantics of Java.
    in: Jim Alves-Foss (Ed.): Formal Syntax and Semantics of Java, Springer LNCS 1523, 353 - 404, 1999. Extended Abstract in: R. Berghammer and F.Simon (Eds.): Programming Languages and Fundamentals of Programming, University of Kiel (Germany) TR 9717, 1997, pp.175-181.
  2. Börger E., Schulte W., Defining the Java Virtual Machine as Platform for Provably Correct Java Compilation.
    in: L. Brim, J. Gruska, J. Zlatuska (Eds.): Proc. MFCS'98. Springer LNCS 1450, 17-35, 1998.
  3. Börger E., Schulte W., Modular Design for the Java Virtual Machine Architecture.
    in: Architecture Design and Validation Methods. Springer Verlag 1999.
  4. Börger E., Schulte W., Initialization Problems for Java .
    in: Software--Concepts and Tools.

See also his home page.


Till Mossakowski: CASL: from semantics to tools

CASL, the common algebraic specification language, has been developed as a language that subsumes many previous algebraic specification frameworks and also provides tool interoperability. CASL is a complex language with a complete formal semantics. It is therefore a challenge to build good tools for CASL. In this work, we present and discuss the Bremen HOL-CASL system, which provides parsing, static checking, conversion to LaTeX and theorem proving for CASL specifications. To make tool construction manageable, we have followed some guidelines: re-use of existing tools, interoperability of tools developed at different sites, and construction of generic tools that can be used for several languages (in particular, it is possible to have an institution-with-symbols-independent static analysis of CASL structured specifications). We describe the structure of and the experiences with our tool and discuss how the guidelines work in practice.

For further information please see the Bremen CoFI Home Page.


Rolf Hennicker: Correct Software Development with UML: From Interfaces to Classes

(joint work with Michel Bidoit, Francoise Tort, and Martin Wirsing)

This talk deals with an enhancement of UML class diagrams by formal notations which specify the properties of interfaces and classes. In the first part of the talk a formal notation for interface constraints is presented which allows us to describe the observable behaviour required by any correct interface implementation (provided by some class). The semantics of interface constraints is defined in terms of the observational logic institution.

In the second part of the talk, the object constraint language OCL is used to specify classes by invariants and pre- and post conditions of the operations. The semantics of the OCL constraints is defined by a schematic translation into a CASL specification. The correctness of an implementation relation between an interface and a class can then be verified by using algebraic proof techniques.

Remark: A corresponding paper appears under the title "Correct Realizations of Interface Constraints with OCL" at the UML '99 conference, Fort Collins, USA.


Martin Wirsing: Software Development with OCL: From Classes to Programs

(joint work with Rolf Hennicker)

The Object Constraint Language OCL is a new specification language which is used for formalizing semantic constraints of UML diagrams. In this lecture we present a method for applying OCL for the development of class implementations and introduce a new Hoare-Calculus for OCL. For simplicity we restrict our approach to total OCL formulae.

In the first part of the lecture we characterize OCL as a first-order logic with bounded quantification whose basic data types such as containers, sets, multisets and sequences can be algebraically axiomatized. "Internal" consistency conditions in the spirit of Z and Z++ are given to ensure the semantic well-definedness of class specifications.

In the second part of the lecture a new Hoare-Calculus for OCL is presented.

As programming language we choose a (sequential) kernel of Java. The Hoare rules are as usual for while programs and for method calls. Access and update of instance variables is handled by an explicit substitution operator which also takes care of aliasing. The rule for creation of objects uses the "allInstances"-operator of OCL.

Our calculus is inspired by Poetzsch-Heffter and Mueller's Hoare calculus for Java; the main difference is that we do not have any explicit representation of state in our formulas. In this respect we rather follow the ideas of Gries and De Boer for handling arrays and references by explicit substitution.

As main result we prove the soundness of our Hoare-Calculus.


Andrea Corradini: A review of the structured transition system method and its application to various rewriting formalisms

I will firstly briefly review the algebraic semantics of structured transition systems originally proposed in my PhD thesis and in [1]. Intuitively, a transition system is a graph (two objects and two parallel arrows in the category of sets), while a structured transition system is an internal graph in a category where usually objects have a richer structure than sets. The categorical framework makes easy to generalize the construction of the path category of a graph to the structured (internal) case, provided that the ambient category satisfies mild assumptions.

Many rule based computational formalisms are usually presented by stressing some algebraic structure of the states, but sticking, for the definition of the rewriting mechanism, to a collection of rule and to some matching mechanism. The basic intuition I will stress next is that the matching mechanism can be more elegantly presented by lifting the algebraic structure from states to transitions or rules, presenting therefore the systems as a structured transition system. This intuition is made explicit for example for P/T Petri Nets in a seminal work by Meseguer and Montanari, and for term rewriting in Meseguer's (unconditional) Rewriting Logic.

This different, more declarative presentation of rule based systems is useful for relating different formalisms and for the analysis of compositional semantics based on left adjoint functors. As a case study,

I will present a categorical description of term graph rewriting, which is a main result of some joint works with Fabio Gadducci [2,3]. This declarative description of term graph rewriting is shown to be equivalent to well-known operational presentations, and fits precisely in the structured transition system methodology.

Here are some pointers to some relevant papers.

[1] Corradini, A. and Montanari, U., An algebraic semantics for structured transition systems and its application to logic programs, TCS 103, 51-106, 1992.

[2] Corradini, A. and Gadducci, F., A 2-Categorical Presentation of Term Graph Rewriting, in Proc. Category Theory and Computer Science, LNCS 1290, Springer Verlag, 1997.

[3] Corradini, A. and Gadducci, F., Rewriting on cyclic structures, Techincal Report TR-98-05, Dipartimento di Informatica, Pisa,, 1998. Extended abstract in Z. Esik, editor, Fixed Points in Computer Science, satellite workshop of MFCS '98. Full version submitted for publication.


Tom Maibaum: A rely-guarantee discipline for open distributed systems design

(Joint work with Carlos Duarte)

There have been a number of studies of the design of distributed systems considering the existence of an environment over which little (if any) control is retained. Perhaps the most systematic of these studies uses rely and guarantee conditions that assert respectively what is assumed about the behaviour of the environment and what behaviour the system is committed to insure, as long as the assumptions hold. This approach is a refinement of the pre and post condition approach extensively studied for sequential program design. We propose a new rely-guarantee discipline based on linear time future temporal connectives applied in a categorical setting where components have open semantics and composition is via colimit constructions. Rely-guarantee becomes a tool for verification, as opposed to earlier uses as part of specifications, to provide a modular proof discipline for the design of open distributed systems.


Kokichi Futatsugi: An overview of Specification and Verification in CafeOBJ

(joint work with Razvan Diaconescu)

Paradigm, theory, and method which support novel style system specification and verification in a new algebraic specification language CafeOBJ is explained. CafeOBJ is a modern successor of OBJ incorporating several recent developments in algebraic specification theory and practice including important features for concurrency and behavioral specifications.

The presentation includes:

  1. An overview of the main features of CafeOBJ.
  2. The behavioral specification paradigm in CafeOBJ.
  3. The object-oriented CafeOBJ specification and verification methodology based on the paradigm.
  4. The mathematical model and theory which support CafeOBJ's paradigm and methodology.
  5. Component-based behavioral specification and verification methodology which features high reusability of both specification code and verification proof scores.

It also includes a demonstration of the above-mentioned topics using CafeOBJ system running on Linux/MacOS/Windows.

For further information, please see the CafeOBJ Home Page.


Edited by: Peter D. Mosses (pdmosses@brics.dk), January 19, 2004
IFIP WG1.3 Home Page: http://www.fiadeiro.org/jose/IFIP-WG1.3/

Bonas (France), 13th-14th September 1999ParticipationAbstracts of Talks