Catálogo de publicaciones - libros

Interfaces became one of the most important features in modern software systems, especially in object-oriented systems. They provide for abstraction and detail hiding and, therefore, contribute to readable and reusable software construction. Formal specification methods have also addressed interfaces and provided formal semantics to them. These semantics are always based on some forgetful and/or restriction constructions. The main focus has been laid on integrating these constructions with free or behaviourable constructions in order to provide some combined semantics for specification modules.

In this paper, we investigate the algebraic properties of “forgetting” and “restricting”. We define two different notions of model category for algebraic specification with explicit interface signatures, so-called interface specifications. The first one uses forgetful constructions only, the second one integrates the restriction to the part reachable by the interface.

We investigate closure properties of these categories w.r.t. subalgebras, products and directed limits. This analysis provides the first result, namely that interface specifications with Horn-axioms do not exceed the expressiveness of Horn-axiom specifications without interfaces. The inverse is more interesting. We show that each category specified by Horn-axioms can be specified by simple equations on possibly hidden operations. The constructive proof for this theorem leads to the next main result that every class specified by an interface specification with restriction semantics possesses an interface specification using forgetful semantics only.

∈-logic was first designed by Werner Sträter as a first-order propositional logic with quantification, reference, and predicates for and . It is motivated by reconstruction of natural language semantics and allows, as a logic with self-reference and impredicativity, among others the treatment of the liar paradox despite the totality of its truth predicates. Its intensional models form a theory of propositions for which a correct and complete calculus is given.

∈-logic was picked up by Philip Zeitz to study the extension of abstract logics by the concepts of truth, reference and classical negation, thereby rebuilding the meta-level of judgements in a formal level of propositional logic. His parameterized ∈-logic allows formulas from a parameter logic to become the constants in his ∈-logic. Parameter-passing of logics with correct and complete calculus also admits, under certain conditions, the entailment of a calculus which is correct and complete for the extended logic.

Since in parameterized ∈-logic Tarski Biconditionals not only apply for the truth of ∈-logic sentences, but also for the meta-level truth of the parameter logic it is natural to view ∈-logic as a theory of judgements whose propositions are expressed in the parameter logic.

We add a new interpretation to ∈-logic as a theory of truth and judgements, and introduce ∈-logic as a means for the integration of logics. Based on a particular choice of uniform view and treatment of logics we define ∈-logics and ∈-extensions as the foundation for ∈-integration of logics and models.

Studies in ∈-logic, which have started to deal with the difficulties of truth in natural language semantics, have evolved into a concept of logic integration where application oriented logics can be plugged in as parameters. This paper very much relies on the work of Philip Zeitz, but opens it for the new perspective of integration.

This paper develops a close analogy between Lawvere’s functorial semantics of equational theories [21], and a similar 2-functorial semantics for rewrite theories, which specify concurrent systems and whose models are “true concurrency” models of such systems. This has the advantage of unifying within a single 2-functorial framework both models and rewrite theory morphisms. Such morphisms are used in Maude to “put rewrite theories together” in different constructions, including parameterized rewrite theory specifications.

Expander2 is a flexible multi-purpose workbench for interactive rewriting, verification, constraint solving, flow graph analysis and other procedures that build up proofs or computation sequences. Moreover, tailor-made interpreters display terms as two-dimensional structures ranging from trees and rooted graphs to a variety of pictorial representations that include tables, matrices, alignments, piles, partitions, fractals and turtle systems.

Proofs and computations performed with Expander2 follow the rules and the semantics of swinging types. Swinging types are based on many-sorted predicate logic and combine constructor-based types with state-based types. The former come as term models, the latter as models consisting of context interpretations. Relation symbols are interpreted as least or greatest solutions of their respective axioms.

This paper presents an overview of Expander2 with particular emphasis on the system’s prover capabilities.

This paper explores the relationship between equational algebraic specifications (using initial algebra semantics) and specifications based on simple inductive types (least fixed points of equations using just products and coproducts, e.g. ≅1+). The main result is a proof that computable data type (one in which the corresponding algebra is computable in the sense of Mal’cev) can be specified inductively. This extends an earlier result of Bergstra and Tucker showing that any computable data type can be specified equationally.

The paper investigates the construction of cofree coalgebras for ‘unsorted signature morphisms’. Thanks to the perfect categorical duality between the traditional concept of equations and the concept of coequations developed in [14] we can fully take profit of the methodological power of Category Theory [2] and follow a clean three step strategy: Firstly, we analyse the traditional construction of free algebras and reformulate it in a systematic categorical way. Then, by dualizing the construction, we obtain, in a second step, corresponding results for cofree coalgebras. And, thirdly, we will interpret the new “abstract” categorical results in terms of more familiar concept. The analysis of a sample cofree construction will provide, finally, some suggestions concerning the potential rôle of cofree coalgebras in System Specifications.

Constraints and application conditions are most important for transformation systems in a large variety of application areas. In this paper, we extend the notion of constraints and application conditions to nested ones and show that nested constraints can be successively transformed into nested right and left application conditions.

Constructing a program from a specification is a long-known general and fundamental problem. Besides its theoretical interest, this question also has practical implications, since finding good synthesis algorithms could bring about a major improvement in the reliable development of complex systems. In this paper we describe a methodology for synthesizing statechart models from scenario-based requirements. The requirements are given in the language of live sequence charts (LSCs), and may be played in directly from the GUI, and the resulting statecharts are of the object-oriented variant, as adopted in the UML. We have implemented our algorithms as part of the Play-Engine tool and the generated statechart model can then be executed using existing UML case tools.

The aim of this paper is to introduce a modelling concept and structuring principle for rule-based systems the semantics of which is not restricted to a sequential behavior, but can be applied to various types of parallelism and concurrency. The central syntactic notion is that of a transformation unit that encapsulates a set of rules, imports other transformation units, and regulates the use and interaction of both by means of a control condition. The semantics is given by interlinking the applications of rules with the semantics of the imported units using a given collection of semantic operations. As the main result, the interlinking semantics turns out to be the least fixed point of the interlinking operator. The interlinking semantics generalizes the earlier introduced interleaving semantics of rule-based transformation units, which is obtained by the sequential composition of binary relations as only semantic operation.

Graph-rewriting has been a growing discipline for over three decades. It grew out of the study of graph grammars, in which – analogously to string and tree grammars – a principal interest was to describe the families of graphs that could be generated from a given set of productions. A fundamental contribution was, of course, the construction of Ehrig and his colleagues [4]; it made precise how the left-hand side of a production, or rewriting rule, could be found to in a host graph, and how it should then be replaced by the right-hand side. This break-through led to many theoretical developments and many applications. It relies firmly upon the treatment of graphs as in a category whose arrows are embedding maps.