Tool Support for the Interactive Derivation of Formally Correct Functional Programs
Date
Authors
Guttmann,Walter
Partsch,Helmuth
Schulte,Wolfram
Vullinghs,Ton
Journal Title
Journal ISSN
Volume Title
Publisher
Journal of Universal Computer Science
Abstract
Description
This paper describes the program transformation system Ultra. The intended use of Ultra is to assist programmers in the formal derivation of correct and efficient programs from high-level descriptive or operational specifications. We illustrate its utility by deriving a version of the Heapsort algorithm from a non-deterministic specification. Ultra supports equational reasoning about functional programs using defining equations, algebraic laws of underlying data structures, and transformation rules. The system does not only support modifying terms, but is also useful for bookkeeping and development navigating tasks. The most salient features of Ultra are its sound theoretical foundation, its extendability, its flexible and convenient way to express transformation tasks, its comfortable user interface, and its lean and portable implementation. Ultra itself is written in the functional language Gofer.
Keywords
constructive program development , equational reasoning , functional programming , heapsort , non-deterministic specification , program transformation , Ultra , unfold-fold