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

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