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.