From descriptive specifications to operational ones: a powerful transformation rule, its applications and variants

Abstract

This paper introduces, discusses and proves a transformation rule to convert specification of set-valued functions defined by set comprehension into functional implementations. Variants of the rule for specifications involving existential quantification and arbitrary choice are presented and illustrated by representative examples.