Programming from Metaphorisms

TL;DR

This paper explores how metaphorisms, a relational specification pattern, can be refined into recursive programs like sorting algorithms, using relation algebra to formalize and derive implementations such as quicksort and mergesort.

Contribution

It introduces a formal framework for refining metaphorisms into recursive programs through change of virtual data structures, with a relation algebra approach.

Findings

Formal conditions for metaphorism refinement

Derivation of quicksort and mergesort algorithms

Unified view of sorting algorithms via metaphorisms

Abstract

This paper presents a study of the metaphorism pattern of relational specification, showing how it can be refined into recursive programs. Metaphorisms express input-output relationships which preserve relevant information while at the same time some intended optimization takes place. Text processing, sorting, representation changers, etc., are examples of metaphorisms. The kind of metaphorism refinement studied in this paper is a strategy known as change of virtual data structure. By framing metaphorisms in the class of (inductive) regular relations, sufficient conditions are given for such implementations to be calculated using relation algebra. The strategy is illustrated with examples including the derivation of the quicksort and mergesort algorithms, showing what they have in common and what makes them different from the very start of development.