Programming by predicates: a formal model for interactive synthesis
| Autor: | Sharon Shoham, Hila Peleg, Shachar Itzhaky, Eran Yahav |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Computer Networks and Communications
Computer science Programming language Backtracking Process (engineering) 020207 software engineering 0102 computer and information sciences 02 engineering and technology computer.software_genre 01 natural sciences Session (web analytics) Domain (software engineering) 010201 computation theory & mathematics Iterative refinement Realizability Theory of computation 0202 electrical engineering electronic engineering information engineering computer Software Program synthesis Information Systems |
| Zdroj: | Acta Informatica. 57:165-193 |
| ISSN: | 1432-0525 0001-5903 |
| DOI: | 10.1007/s00236-019-00340-y |
| Popis: | Program synthesis is the problem of computing from a specification a program that implements it. New and popular variations on the synthesis problem accept specifications in formats that are easier for the human synthesis user to provide: input–output example pairs, type information, and partial logical specifications. These are all partial specification formats, encoding only a fraction of the expected behavior of the program, leaving many matching programs. This transition into partial specification also changes the mode of work for the user, who now provides additional specifications until they are happy with the synthesis result. Therefore, synthesis becomes an iterative, interactive process. We present a formal model for interactive synthesis, parameterized by an abstract domain of predicates on programs. The abstract domain is used to describe both the iterative refinement of the specifications and reduction of the candidate program space. We motivate the need for a general feedback model via predicates by showing that examples, the most frequent specification tool, are an insufficient tool to differentiate between programs, even when used as a full specification. We use the formal model to describe the behavior of several real-world synthesizers. Additionally, we present two conditions for termination of a synthesis session, one hinging only on the properties of the available partial specifications, and the other also on the behavior of the user. Finally, we show conditions for realizability of the user’s intent, and show the limitations of backtracking when it is apparent a session will fail. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink