JUCS - Journal of Universal Computer Science 9(2): 173-188, doi: 10.3217/jucs-009-02-0173
Tool Support for the Interactive Derivation of Formally Correct Functional Programs
expand article infoWalter Guttmann‡, Helmuth Partsch‡, Wolfram Schulte§, Ton Vullinghs‡
‡ University of Ulm, Germany§ Microsoft Research, United States of America

Corresponding author: Walter Guttmann ( walter@informatik.uni-ulm.de )

© Walter Guttmann, Helmuth Partsch, Wolfram Schulte, Ton Vullinghs.
This article is freely available under the J.UCS Open Content License.
Citation: Guttmann W, Partsch H, Schulte W, Vullinghs T (2003) Tool Support for the Interactive Derivation of Formally Correct Functional Programs. JUCS - Journal of Universal Computer Science 9(2): 173-188. https://doi.org/10.3217/jucs-009-02-0173
Open Access
Abstract
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