Software Synthesis Procedures.
Automated synthesis of program fragments from specifications can make programs easier to write and easier to reason about. To integrate synthesis into programming languages, software synthesis algorithms should behave in a predictable way: they should succeed for a well-defined class of specificatio...
| Publicado en: | Communications of the ACM Vol. 55; no. 2; pp. 103 - 112 |
|---|---|
| Autores principales: | , , , |
| Formato: | Artículo |
| Publicado: |
Association for Computing Machinery
Feb2012
|
| Materias: | |
| Acceso en línea: | Ver este registro en EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=71681492&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 71681492 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 00010782 ACM jtl: Communications of the ACM issn: 00010782 maglogo: N pubinfo: dt: Feb2012 vid: 55 iid: 2 pid: 68 pub: Association for Computing Machinery artinfo: ui: 71681492 10.1145/2076450.2076472 ppf: 103 ppct: 9 formats: tig: atl: Software Synthesis Procedures. aug: au: Kuncak, Viktor Mayer, Mikaël Piskac, Ruzica Suter, Philippe su: Computer programming Computer software Automatic programming (Computer science) Programming languages Data structures Algorithms sug: subj: Computer programming Computer software Automatic programming (Computer science) Programming languages Data structures Algorithms ab: Automated synthesis of program fragments from specifications can make programs easier to write and easier to reason about. To integrate synthesis into programming languages, software synthesis algorithms should behave in a predictable way: they should succeed for a well-defined class of specifications. We propose to systematically generalize decision procedures into synthesis procedures, and use them to compile implicitly specified computations embedded inside functional and imperative programs. Synthesis procedures are predictable, because they are guaranteed to find code that satisfies the specification whenever such code exists. To illustrate our method, we derive synthesis procedures by extending quantifier elimination algorithms for integer arithmetic and set data structures. We then show that an implementation of such synthesis procedures can extend a compiler to support implicit value definitions and advanced pattern matching. pubtype: Periodical doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y dt: @attributes: year: 2012 holdings: @attributes: islocal: N |
|---|