4
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Brent Apr 13 '15 at 4:07
  • $\begingroup$ 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. $\endgroup$ – D.W. Apr 13 '15 at 5:30
  • $\begingroup$ 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. $\endgroup$ – Raphael Apr 13 '15 at 10:08
2
$\begingroup$

The phrase to look for is "program synthesis". There's lots of literature in the programming literature on this topic; I suggest using Google Scholar to search through the literature and find relevant publications.

These days one hot approach is using "program sketching". In program sketching, the programmer specifies a template for the code: partial code, with some holes left blank. The tool then automatically tries to fill in those holes in a way that is consistent with the preconditions/postconditions, or is consistent with some provided test cases. There's lot of literature on this topic. For an introduction to this line of work, I'll suggest the following tutorial:

The Sketching Approach to Program Synthesis. Armando Solar-Lezama. Tutorial at PLDI 2012.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.