Between functions and relations in calculating programs - Hutton, Graham (1992)
This thesis is about the calculational approach to programming, in which one derives programs from specifications. One such calculational paradigm is Ruby, the relational calculus developed by Jones and Sheeran for describing and designing circuits. We identify two shortcomings with derivations made using Ruby. The first is that the notion of a program being an implementation of a specification has never been made precise. The second is to do with types. Fundamental to the use of type information in deriving programs is the idea of having types as special kinds of programs. In Ruby, types are partial equivalence relations (pers). Unfortunately, manipulating some formulae involving types has proved difficult within Ruby. In particular, the preconditions of the ‘induction’ laws that are much used within program derivation often work out to be assertions about types; such assertions have typically been verified either by informal arguments or by using predicate calculus, rather than by applying algebraic laws from Ruby.