| This thesis describes the implementation and use of BOBJ and Kumo, two software systems that support behavioral algebraic specification and verification, based on recent developments in hidden algebra and user interface design. BOBJ supports ordinary rewriting for order sorted equational logic, as well as order sorted behavioral rewriting and circular coinductive rewriting for hidden logic; there is also provision for case analysis during circular coinductive rewriting. Behavioral specification provides a uniform framework for concurrency, distribution, nondeterminism, and features of the object paradigm. In addition, BOBJ implements higher order parameterized programming. Parameterized programming introduces parameterized modules with “views” to flexibly fit actual parameter modules to interfaces, and module expressions to compose systems from component modules; default views relieve users from writing obvious code. These technologies facilitate the composition of software systems from components. This thesis extends parameterized programming to higher order modules, and extends views to morphisms, which support both instantiating modules as functors on slice categories, is defined. Mechanical proofs in general, and BOBJ first-order behavioral proofs in particular, can easily become unmanageable by humans in large applications without the use of good proof assistants. Kumo is a proof assistant that supports distributed collaborative reasoning in first order hidden logic, based on BOBJ. Kumo takes proof scripts as inputs and generates a proof object represented as a browsable web site designed by algebraic semiotics. This proof website supports proof debugging and revision. |
