代数语言规约的ML原型翻译系统

A Prototype Translation System from the Specification of Algebraic Language into ML

形式化的规约说明对于提高软件开发的正确性和效率有很大作用,一个形式化的规约说明语言开发环境如图1所示。目前有的原型系统是用常规高级语言,即一般的过程语言来写的,如C。这种原型环境涉及大量低层细节.程序繁琐冗长,且和计算机状态相联系,破坏了原有规约的证明特性。

A prototype for the specifications of algebraic language is required. A translation system from the specification OBSCURE into ML(OTM), in which both the concept and approach of mapping of the atomic, simple and composed specification are introduced, is proposed in this paper. This method gave the algebraic specifications a good programming environment and it is available to be integrated with a verification environment.