# Research regarding algorithm generation/discovery/heuristics

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

Postcondition:

• 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?

• Please add tags you think are relevant. Related questions:What kind of symbolic transformations/calculus exist on preconditions and postconditions? what closure properties? Are there many possible specifications for the same function, and if so can the equivalence of two specifications be determined symbolically? Can they be transformed into each other? How can we determine the form of the specification that is simultaneously unambiguous, contains no redundant/tautological statements, and contains no irrelevant information or contradictions. – Brent Apr 13 '15 at 4:07
• One area that you might be interested in is "sketching" (program sketching); there's been a bunch of publications on that topic in recent years. It's sort've of the vein you are looking for -- not exactly, but related enough that it might interest you. – D.W. Apr 13 '15 at 5:30
• Sure: enumerate all programs up to some length and try to verify for each that they have the required property. Certainly not computable in general, but you may be lucky. It's basically theory exploration turned around. – Raphael Apr 13 '15 at 10:08