Hidden Algebra and Modular Distributed Concurrent Software

点击翻译按钮获取中文摘要

9901002 Goguen, Joseph A University of CaliforniaHidden Algebra and Modular Distributed Concurrent SoftwareTools, theory, case studies, and methods are being developed for hidden algebra, a new approach to specifying, prototyping, verifying, documenting and generating distributed concurrent software. Tools build on the Kumo proof assistant and website generator, by providing a new specification language, taking advantage of new web technology (XML, dynamic HTML, JavaCC, etc.), and using multiple inference engines, including the new CafeOBJ system. Hidden algebra extends the algebraic approach to abstract data types (ADTs) initiated by the PI, by encompassing state, behavioral abstraction, nondeterminism, concurrency, and first order sentences; like the algebraic theory of ADTs, it works well with modularization. More powerful proof principles are being developed, as well as better methods for documenting proofs. Long term goals are to develop tools, methods and theory for high quality software systems, and to advance our understanding of modular distributed concurrent systems. Semantics is important as a model for designing software tools, and providing correctness criteria for important relations like refinement, while experimentation is essential for ensuring that the approach can handle realistic problems and meet real needs.