Software synthesis procedures
| Autor: | Viktor Kuncak, Ruzica Piskac, Mikaël Mayer, Philippe Suter |
|---|---|
| Rok vydání: | 2012 |
| Předmět: |
correctness by construction
Class (computer programming) Theoretical computer science General Computer Science Programming language Computer science Computation software synthesis 020207 software engineering 02 engineering and technology computer.software_genre Data structure Set (abstract data type) 020204 information systems Quantifier elimination 0202 electrical engineering electronic engineering information engineering Code (cryptography) Pattern matching Compiler computer |
| Zdroj: | Communications of the ACM |
| ISSN: | 1557-7317 0001-0782 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|