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.
