Constructing Software From Specifications

软件工程形式化方法的研究主要集中在软件规格说明方面。本研究探讨下一步的工作：在给定构造性规格说明的基础上，利用程序转换和专业化技术生成实用高效的软件。通过（1）通过基于规则的程序转换的算法改进和（2）由指定数据表示的接口规范指导的翻译，已经对从可执行规范构造软件进行了研究。本研究集中在两个具体的问题：（a）扩展程序转换规则，以便引入异常对应的断言条件的数据和（B）原型的程序实例化工具，翻译成一个独立指定的语义模型的可执行规范。将探讨证明数据类型表示的语义有效性的系统技术。

Research in formal methods for software engineering has been primarily concerned with software specification. This research explores the next step: given a means of constructive specification, to generate practical and efficient software by the technologies of program transformation and specialization. Studies have been done for the construction of software from executable specifications by (1) algorithms improvement by means of rule-based program transformation and (2) a translation directed by an interface specification that specifies data representations. This research is focused on two specific problems: (a) extending program transformation rules so as to introduce exceptions corresponding to asserted conditions of data and (b) prototyping a program instantiation tool that translates an executable specification into an independently specified semantic model. Systematic techniques for proving the semantic validity of representations for data types will be explored.