The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
The ESPRIT Basic Research Working Group COMPASS has brought together most European scientists in the area of algebraic specification methods in an effort to consolidate and integrate the theoretical basis and apply it to software technology. The algebraic approach treats not just the syntactic aspects of interfaces but supports the precise specification of the semantics of generic reusable system...
The paper summarizes the main concepts and paradigms of category theory and explores some of their applications to the area of algebraic specifications. In detail we discuss different approaches to an abstract theory of specification logics. Further we present a uniform framework for developing particular specification logics. We make use of ‘classifying categories’, to present categories of...
Unification of theories is the long-standing goal of the natural sciences; and modern physics offers a spectacular paradigm of its achievement. The structure of modern mathematics has also been determined by its great unifying theories — topology, algebra and the like. The same ideals and goals are shared by researchers and students of theoretical computing science.
The Larch Shared Language for the specification of abstract data types has evolved over a number of years from a simple algebraic language to one that is both more complicated and more useful. This talk reviews some of its major design decisions and then discusses some of the design issues and remaining open problems—most of which are consequences of the same decisions that contribute to LSL's good...
We investigate functorial relationships between the categories of theories in different institutions, namely adjunctions, as a means of translating between the different specification spaces that they provide. We show that there is a canonical way in which adjunctions between the categories of signatures can be lifted to the categories of theories. This lifting is associated with a duality between...
This paper presents a technical approach for solving the problem of inter-operability between the different existing tools and languages for algebraic specifications. We discuss some semantic compatibility criteria required to ensure a minimal level of inter-operability, we describe a proposal for a specification interchange format, and we explain the mechanisms needed to solve the issues raised by...
We describe a method to improve the efficiency of normalization procedures for term rewriting systems. This improvement does not restrict the semantics of the term rewriting specification in any respect. In particular, the expressive power of term rewriting systems as a programming language for generic programs and as a theorem prover has been preserved. Our method is based on the following observation...
In this paper we propose a semantic framework for dealing with class- sort polymorphism as presented in the last version of GLIDER. This kind of polymorphism is quite more powerful than the standard sort polymorphism that can be found in a number of functional languages (e.g. Standard ML, Miranda, etc.).In particular, polymorphic or generic types are considered to be parameterized by specifications...
The aim of our work is the modelling and design of information systems in the object-oriented setting. An object-oriented specification covers structural as well as behavioural aspects of the system. A possibility to describe system dynamics is to use a temporal logic as it is done in the formal object-oriented specification language Troll. Temporal logics is particularly suited to deal with temporal...
This paper exploits the point of view of constraint programming as computation in a logical system, namely constraint logic. We define the basic ingredients of constraint logic, such as constraint models and generalised polynomials. We show that constraint logic is an institution, and we internalise the study of constraint logic to the framework of category-based equational logic. By showing that...
The introduction of a notion of states into algebraic specifications yields the possibility to specify dynamic and communicating systems, and to compare formally algebraic and dynamic specifications. In the approach presented here states are modelled as partial algebras that extend a fixed partial algebra considered as static data type. Transitions are specified by rules that express the replacement...
We construct a category of circuits: the objects are alphabets and the morphisms are deterministic automata. The construction differs in several respects from the bicategories of circuits appearing previously in the literature: it is parameterized by a monad which allows flexibility in the emergent notion of process. We focus on the circuits which arise from a distributive category and the...
Specification frameworks such as B and Z provide power sets and cartesian products as built-in type constructors, and employ a rich notation for defining (among other things) abstract data types using formulae of predicate logic and lambda-notation. In contrast, the so-called algebraic specification frameworks often limit the type structure to sort constants and first-order functionalities, and restrict...
Formally well-founded compilation techniques for Term Rewriting Systems (TRSs) are presented. TRSs are compiled into Minimal Term Rewriting Systems (MTRSs), a subclass of TRSs in which all rules have an extremely simple form. A notion of simulation of (rewrite) relations is presented, under which an MTRS can be said to simulate a TRS. The MTRS rules can be directly interpreted as instructions for...
The InterACT tool is an interactive theorem prover for algebraic specifications emphasizing user-friendliness. InterACT is integrated in the existing ACT environment. The main purpose of InterACT is to teach formal methods in universitary courses about formal specification of software systems. It has already been used successfully in this area. The theoretical and practical concepts underlying...
We consider reasoning and rewriting with set-relations: inclusion, non-empty intersection and singleton identity, each of which satisfies only two among the three properties of the equivalence relations. The paper presents a complete inference system which is a generalization of ordered paramodulation and superposition calculi. Notions of rewriting proof and confluent rule system are defined for such...
This paper studies termination of curryfied term rewriting systems (CTRSs), where functional values are introduced by “partial application” The limitations of syntactic simplification orderings for such systems are discussed. A proof method is proposed, based on three techniques: 1) Requirements on stability and monotonicity are relaxed. 2) Variables and inner function symbols of (potentially) functional...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.