The Mathematical Laws of S*M: An Axiomatic Specification Language for Firmware and Architecture Design.

迄今为止，PI工作的主要成果是设计和实现了一种新的公理化、非过程性语言，称为S*M，用于固件和计算机体系结构的功能规范。S*M的实现由一个编译器、一个模拟器和一个运行在VAX 11/780 unix环境下的用户界面组成。S*M已被广泛用于指定固件和架构的行为和推理，因此，对其优点和局限性有了相当大的理解。该语言的特性也使S*M对科罗拉多州立大学（固件工程）、加拿大安大略省圭尔夫大学（设计自动化）和西德亚琛工业大学（多处理器设计的正式开发）的研究项目产生了足够的吸引力。该项目通过确定S*M的基本数学定律来继续这项工作。这些定律将以“P = Q”的形式出现，其中P， Q是S*M结构，这意味着，在功能和行为上，“P与Q是相同的”。因此，给定P在S*M描述中出现，我们可以用等价的q变换或替换P。这些数学定律将是这样的：(i) S*M中所有正确的规格必须遵守这些法律。（ii）通过应用这些定律，正确的S*M规范可以转换为等效的（可能更简洁或更有效的）规范。

The main results of the PI's work to date are the design and implementation of a novel axiomatic, non-procedural language called S*M for the functional specification of firmware and computer architectures. The implementation of S*M consists of a compiler, a simulator, and a user interface running on VAX 11/780 UNIXTM environment. S*M has been used extensively to specify the behavior of, and reason about, firmware and architectures and, consequently, considerable understanding of its strengths and limitations has been gained. The features of the language have also made it sufficiently attractive for S*M to have influenced research projects in Colorado State University (firmware engineering), University of Guelph, Ontario, Canada (design automation), and the Technical University of Aachen, West Germany (formal development of multiprocessor designs). The project continues this work by identifying the basic mathematical laws of S*M. These laws will take the form "P = Q" where, P, Q, are S*M constructs and will mean that, functionally and behaviorally, "P is the same as Q". Thus, given an occurrence of P in an S*M description, one can transform or replace P by the equivalent Q. These mathematical laws will be such that: (i) All correct specifications in S*M must obey these laws. (ii) A correct S*M specification may be transformed into a equivalent (possibly more concise or more efficient) specification by applying these laws.