Towards behavioral maude: Behavioral membership equational logic

How can algebraic and coalgebraic specifications be integrated? How can behavioral equivalence be addressed in an algebraic specification language? The hidden-sorted approach, originating in work of Goguen and Meseguer in the early 80's, and further developed into the hidden-sorted logic approach by researchers at Oxford, UC San Diego, and Kanazawa offers some attractive answers, and has been implemented in both BOBJ and CafeOBJ. In this work we investigate both further extensions of hidden logic, and an extension of the Maude specification language called BMaude supporting this extended hidden-sorted semantics. Maude's underlying equational logic, membership equational logic, generalizes and increases the expressive power of many-sorted and order-sorted equational logics. We develop a hidden-sorted extension of membership equational logic, and give conditions under which theories have both an algebraic and a coalgebraic semantics, including final (co-)algebras. We also discuss the language design of BMaude, based on such an extended logic and using categorical notions in and across the different institutions involved. We also explain how Maude's reflective semantics provides a systematic method to extend Maude to BMaude within Maude, including module composition operations, evaluation, and automated proof methods.