Say I have a specification of preconditions and postconditions for a function. Is there a field of computer science that studies the automated generation of functions that satisfy those specifications?
For example: Preconditions:
- I is a list
- Q is a binary relation specifying a total order on the elements in I
- O is a list
- There exists a bimap B (and its complement B') such that
- O[B[j]] = I[j], and
- O[j] = I[B'[j]],
- for every j, 0 <= j < n,
- For every x, 0 < x < n, Q(O[x - 1], O[x]) is true.
The set of functions that satisfy this (I hope unambiguous) specification are the sorting algorithms. So, how do we get a computer to take this specification, and give us a sorting algorithm?