Definite Descriptions and Dijkstra's Odd Powers of Odd Integers Problem

The use of Frege-Russell style definite descriptions for giving meaning to functions has been long established and we investigate their use in the development of Functional Programs and from these to the development of correct imperative programs. In particular, we investigate the development of a functional program for a problem, “Odd powers of odd integers”, discussed by Dijsktra. If the correctness of termination is not a concern then it is straightforward to develop a partially correct program. Further properties of the specification are needed to develop a totally correct program.