• English
    • Deutsch
View Item 
  •   OPARU Home
  • Fakultät für Ingenieurwissenschaften, Informatik und Psychologie
  • Publikationen
  • View Item
  •   OPARU Home
  • Fakultät für Ingenieurwissenschaften, Informatik und Psychologie
  • Publikationen
  • View Item
  • English 
    • English
    • Deutsch
  • Login
JavaScript is disabled for your browser. Some features of this site may not work without it.

Tool Support for the Interactive Derivation of Formally Correct Functional Programs

Thumbnail
Download
JUCS2003.pdf (151.1Kb)
Erstveröffentlichung
2003
DOI
10.18725/OPARU-35283
Wissenschaftlicher Artikel


Authors
Guttmann, Walter
Partsch, Helmuth
Schulte, Wolfram
Vullinghs, Ton
Faculties
Fakultät für Ingenieurwissenschaften, Informatik und Psychologie
Institutions
Abteilung Programmiermethodik und Compilerbau
Published in
Journal of Universal Computer Science ; 9 (2003), 2. - S. 173-188. - ISSN 0948-695x. - eISSN 0948-6968
Link to original publication
https://dx.doi.org/10.3217/jucs-009-02-0173
Peer review
ja
Document version
publishedVersion
License
in copyright
http://rightsstatements.org/vocab/InC/1.0/
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.
Subject Headings
Funktionale Programmierung [GND]
Program transformation (Computer programming) [LCSH]
Functional programming (Computer science) [LCSH]
Computer algorithms [LCSH]
Keywords
Constructive Program Development; Equational Reasoning; Heapsort; Non-deterministic Specification; Ultra; Unfold-Fold
Dewey Decimal Group
DDC 000 / Computer science, information & general works

Metadata
Show full item record

Citation example

Guttmann, Walter et al. (2021): Tool Support for the Interactive Derivation of Formally Correct Functional Programs. Open Access Repositorium der Universität Ulm. http://dx.doi.org/10.18725/OPARU-35283

Other citation formats



About OPARU | Contact Us
Impressum | Privacy statement
 

 

Advanced Search

Browse

All of OPARUCommunities & CollectionsFacultiesInstitutionsPersonsResource typesUlm SerialsDewey Decimal ClassesFundingThis CollectionFacultiesInstitutionsPersonsResource typesUlm SerialsDewey Decimal ClassesFunding

My Account

LoginRegister

Statistics

View Usage Statistics

About OPARU | Contact Us
Impressum | Privacy statement