Functional languages for the implementation of formal specifications

摘要

A programming language concept called functional programming has developed to the extent that programs can be viewed as being executable formal specifications. These languages can be manipulated using a technique known as 'program transformation' which alters the form of the program but not it's behaviour. The authors examine work in the System and Software Engineering Division at Martlesham Heath which uses functional languages as part of a formal lifecycle. This approach allows specifications to be executed, somewhat slowly, from the beginning of development and uses program transformation to derive a correct implementation which matches speed and size constraints. All programs in the article are given in the functional language Haskell (P. Wadler, P. Hudak, 1989). The authors present an overview of the transliteration method, show how program transformation can be used to increase the efficiency of a program and give examples of each method. Issues requiring further work are highlighted.