Hidden Algebra and Modular Distributed Concurrent Software

9901002 Goguen，Joseph A 隐藏代数和模块化分布式并发软件的工具，理论，案例研究和方法正在开发的隐藏代数，一种新的方法来指定，原型，验证，文档化和生成分布式并发软件。 工具建立在Kumo证明助手和网站生成器的基础上，通过提供新的规范语言，利用新的Web技术（XML，动态HTML，JavaCC等），并使用多个推理引擎，包括新的CafeOBJ系统。 隐代数将代数方法扩展到由PI发起的抽象数据类型（ADT），包括状态，行为抽象，非确定性，并发性和一阶语句;像ADT的代数理论一样，它可以很好地与模块化一起工作。 正在开发更强大的证明原则，以及更好的证明方法。 长期目标是开发高质量软件系统的工具，方法和理论，并提高我们对模块化分布式并发系统的理解。 语义作为设计软件工具的模型是很重要的，并为重要的关系提供正确性标准，如细化，而实验是必不可少的，以确保该方法可以处理现实的问题，并满足真实的需求。

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.