This paper generalizes many-sorted algebra (MSA) to order-sorted algebra (OSA) by
allowing a partial ordering relation on the set of sorts. This supports abstract data types with …

This paper proposes membership equational logic—a Horn logic in which the basic
predicates are equations t= t′ and membership assertions t: s stating that a term t belongs …

This is an introduction to the philosophy and use of OBJ, emphasizing its oper-ational
semantics, with aspects of its history and its logical semantics. Release 2 of OBJ3 is …

As its title promises, this book provides foundations for software specification and formal
software development from the perspective of work on algebraic specification. It …

This paper is part of a long-term effort to increase expressiveness of algebraic specification
languages while at the same time having a simple semantic foundation on which efficient …

This book can be seen either as a text on theorem proving that uses techniques from
general algebra, or else as a text on general algebra illustrated and made concrete by …

Cleverly designed software often fails to satisfy its requirements strictly, but instead satisfies
them behaviorally, in the sense that they appear to be satisfied under every experiment that …

This paper surveys ways in which the ideas and concepts developed in the research field of
abstract data types have undergone a vigorous process of generalization that has led to the …

Modern software is no more developed in a single programming language. Instead,
programmers tend to exploit cross-language interoperability mechanisms to combine code …

Order-sorted specifications (ie many-sorted specifications with subsort relations) have been
proved to be a useful tool for the description of partially defined functions and error handling …