Skip to main content
Top
Published in: Acta Informatica 1-2/2020

30-08-2019 | Original Article

Programming by predicates: a formal model for interactive synthesis

Authors: Hila Peleg, Shachar Itzhaky, Sharon Shoham, Eran Yahav

Published in: Acta Informatica | Issue 1-2/2020

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Footnotes
1
The number of removes has to be at least \(\big |\langle x\in \iota _1 \mid x > \mathrm {head}(\iota _1)\rangle \big |\), but at most \(|\iota _2|\), which is not possible without branches.
 
Literature
1.
go back to reference Albarghouthi, A., Gulwani, S., Kincaid, Z.: Recursive program synthesis. In: International Conference on Computer Aided Verification, pp. 934–950. Springer (2013) Albarghouthi, A., Gulwani, S., Kincaid, Z.: Recursive program synthesis. In: International Conference on Computer Aided Verification, pp. 934–950. Springer (2013)
2.
go back to reference Alur, R., Bodik, R., Juniwal, G., Martin, M.M., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. Dependable software. Syst. Eng. 40, 1–25 (2015)CrossRef Alur, R., Bodik, R., Juniwal, G., Martin, M.M., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. Dependable software. Syst. Eng. 40, 1–25 (2015)CrossRef
3.
4.
go back to reference Alur, R., Radhakrishna, A., Udupa, A.: Scaling enumerative program synthesis via divide and conquer. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 319–336. Springer (2017) Alur, R., Radhakrishna, A., Udupa, A.: Scaling enumerative program synthesis via divide and conquer. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 319–336. Springer (2017)
5.
go back to reference Anton, T.: Xpath-wrapper induction by generalizing tree traversal patterns. In: Lernen, Wissensentdeckung und Adaptivitt (LWA) 2005, GI Workshops, Saarbrcken, pp. 126–133 (2005) Anton, T.: Xpath-wrapper induction by generalizing tree traversal patterns. In: Lernen, Wissensentdeckung und Adaptivitt (LWA) 2005, GI Workshops, Saarbrcken, pp. 126–133 (2005)
6.
go back to reference Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252 (1977) Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252 (1977)
7.
go back to reference Drachsler-Cohen, D., Shoham, S., Yahav, E.: Synthesis with abstract examples. In: Majumdar, R., Kunčak, V. (eds.), Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24–28, 2017, Proceedings, Part I, pp. 254–278 (2017)CrossRef Drachsler-Cohen, D., Shoham, S., Yahav, E.: Synthesis with abstract examples. In: Majumdar, R., Kunčak, V. (eds.), Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24–28, 2017, Proceedings, Part I, pp. 254–278 (2017)CrossRef
8.
go back to reference Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1), 35–45 (2007)MathSciNetCrossRef Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1), 35–45 (2007)MathSciNetCrossRef
9.
go back to reference Feng, Y., Martins, R., Wang, Y., Dillig, I., Reps, T.: Component-based synthesis for complex apis. In: Proceedings of the 44th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2017 (2017) Feng, Y., Martins, R., Wang, Y., Dillig, I., Reps, T.: Component-based synthesis for complex apis. In: Proceedings of the 44th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2017 (2017)
10.
go back to reference Feser, J.K., Chaudhuri, S., Dillig, I.: Synthesizing data structure transformations from input–output examples. In: ACM SIGPLAN Notices, ACM, vol. 50, pp. 229–239 (2015) Feser, J.K., Chaudhuri, S., Dillig, I.: Synthesizing data structure transformations from input–output examples. In: ACM SIGPLAN Notices, ACM, vol. 50, pp. 229–239 (2015)
11.
go back to reference Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for esc/java. In: Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity (London, UK, UK, 2001), FME ’01, pp. 500–517 Springer-Verlag Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for esc/java. In: Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity (London, UK, UK, 2001), FME ’01, pp. 500–517 Springer-Verlag
12.
go back to reference Galenson, J., Reames, P., Bodik, R., Hartmann, B., Sen, K.: Codehint: Dynamic and interactive synthesis of code snippets. In: Proceedings of the 36th International Conference on Software Engineering, ACM, pp. 653–663 (2014) Galenson, J., Reames, P., Bodik, R., Hartmann, B., Sen, K.: Codehint: Dynamic and interactive synthesis of code snippets. In: Proceedings of the 36th International Conference on Software Engineering, ACM, pp. 653–663 (2014)
13.
go back to reference Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (New York, NY, USA, 2011), POPL ’11, ACM, pp. 317–330 Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (New York, NY, USA, 2011), POPL ’11, ACM, pp. 317–330
14.
go back to reference Gulwani, S.: Synthesis from examples: interaction models and algorithms. In: Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 2012 14th International Symposium on, IEEE, pp. 8–14 (2012) Gulwani, S.: Synthesis from examples: interaction models and algorithms. In: Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 2012 14th International Symposium on, IEEE, pp. 8–14 (2012)
15.
go back to reference Gvero, T., Kuncak, V., Kuraj, I., Piskac, R.: Complete completion using types and weights. In: ACM SIGPLAN Notices, ACM, vol. 48, pp. 27–38 (2013) Gvero, T., Kuncak, V., Kuraj, I., Piskac, R.: Complete completion using types and weights. In: ACM SIGPLAN Notices, ACM, vol. 48, pp. 27–38 (2013)
16.
17.
18.
go back to reference Kruskal, J.B.: Well-quasi-ordering, the tree theorem, and vazsonyi’s conjecture. Trans. Am. Math. Soc. 95(2), 210–225 (1960)MathSciNetMATH Kruskal, J.B.: Well-quasi-ordering, the tree theorem, and vazsonyi’s conjecture. Trans. Am. Math. Soc. 95(2), 210–225 (1960)MathSciNetMATH
19.
go back to reference Landauer, J., Hirakawa, M.: Visual awk: a model for text processing by demonstration. In: vl, pp. 267–274 (1995) Landauer, J., Hirakawa, M.: Visual awk: a model for text processing by demonstration. In: vl, pp. 267–274 (1995)
20.
go back to reference Lau, T., Wolfman, S.A., Domingos, P., Weld, D.S.: Learning repetitive text-editing procedures with smartedit. Your Wish Is My Command: Giving Users the Power to Instruct Their Software, pp. 209–226 (2001)CrossRef Lau, T., Wolfman, S.A., Domingos, P., Weld, D.S.: Learning repetitive text-editing procedures with smartedit. Your Wish Is My Command: Giving Users the Power to Instruct Their Software, pp. 209–226 (2001)CrossRef
21.
go back to reference Lau, T., Wolfman, S.A., Domingos, P., Weld, D.S.: Programming by demonstration using version space algebra. Mach. Learn. 53(1), 111–156 (2003)CrossRef Lau, T., Wolfman, S.A., Domingos, P., Weld, D.S.: Programming by demonstration using version space algebra. Mach. Learn. 53(1), 111–156 (2003)CrossRef
22.
go back to reference Le, V., Gulwani, S.: FlashExtract: a framework for data extraction by examples. In: O’Boyle, M.F.P., Pingali, K. (eds.) Proceedings of the 35th Conference on Programming Language Design and Implementation, ACM, p. 55 (2014) Le, V., Gulwani, S.: FlashExtract: a framework for data extraction by examples. In: O’Boyle, M.F.P., Pingali, K. (eds.) Proceedings of the 35th Conference on Programming Language Design and Implementation, ACM, p. 55 (2014)
23.
go back to reference Le, V., Perelman, D., Polozov, O., Raza, M., Udupa, A., Gulwani, S.: Interactive program synthesis (2017) Le, V., Perelman, D., Polozov, O., Raza, M., Udupa, A., Gulwani, S.: Interactive program synthesis (2017)
24.
go back to reference Löding, C., Madhusudan, P., Neider, D.: Abstract learning frameworks for synthesis. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 167–185. Springer (2016) Löding, C., Madhusudan, P., Neider, D.: Abstract learning frameworks for synthesis. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 167–185. Springer (2016)
25.
go back to reference Omari, A., Shoham, S., Yahav, E.: Cross-supervised synthesis of web-crawlers. In: Proceedings of the 38th International Conference on Software Engineering, ICSE 2016, Austin, TX, USA, May 14-22, 2016, pp. 368–379 (2016) Omari, A., Shoham, S., Yahav, E.: Cross-supervised synthesis of web-crawlers. In: Proceedings of the 38th International Conference on Software Engineering, ICSE 2016, Austin, TX, USA, May 14-22, 2016, pp. 368–379 (2016)
26.
go back to reference Osera, P.-M., Zdancewic, S.: Type-and-example-directed program synthesis. In: ACM SIGPLAN Notices, ACM, vol. 50, pp. 619–630 (2015)CrossRef Osera, P.-M., Zdancewic, S.: Type-and-example-directed program synthesis. In: ACM SIGPLAN Notices, ACM, vol. 50, pp. 619–630 (2015)CrossRef
27.
go back to reference Peleg, H., Itzhaky, S., Shoham, S.: Abstraction-based interaction model for synthesis. In: Dillig, I., Palsberg, J. (eds.) Verification, Model Checking, and Abstract Interpretation, pp. 382–405. Springer, Cham (2018)CrossRef Peleg, H., Itzhaky, S., Shoham, S.: Abstraction-based interaction model for synthesis. In: Dillig, I., Palsberg, J. (eds.) Verification, Model Checking, and Abstract Interpretation, pp. 382–405. Springer, Cham (2018)CrossRef
28.
go back to reference Peleg, H., Shoham, S., Yahav, E.: D3: Data-driven disjunctive abstraction. In: Verification, Model Checking, and Abstract Interpretation, pp. 185–205. Springer (2016) Peleg, H., Shoham, S., Yahav, E.: D3: Data-driven disjunctive abstraction. In: Verification, Model Checking, and Abstract Interpretation, pp. 185–205. Springer (2016)
29.
go back to reference Peleg, H., Shoham, S., Yahav, E.: Programming not only by example. In: Proceedings of the 40th International Conference on Software Engineering, ACM, pp. 1114–1124 (2018) Peleg, H., Shoham, S., Yahav, E.: Programming not only by example. In: Proceedings of the 40th International Conference on Software Engineering, ACM, pp. 1114–1124 (2018)
30.
go back to reference Perelman, D., Gulwani, S., Ball, T., Grossman, D.: Type-directed completion of partial expressions. In: ACM SIGPLAN Notices, ACM, vol. 47, pp. 275–286 (2012) Perelman, D., Gulwani, S., Ball, T., Grossman, D.: Type-directed completion of partial expressions. In: ACM SIGPLAN Notices, ACM, vol. 47, pp. 275–286 (2012)
31.
go back to reference Polikarpova, N., Kuraj, I., Solar-Lezama, A.: Program synthesis from polymorphic refinement types. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, ACM, pp. 522–538 (2016)CrossRef Polikarpova, N., Kuraj, I., Solar-Lezama, A.: Program synthesis from polymorphic refinement types. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, ACM, pp. 522–538 (2016)CrossRef
32.
go back to reference Polozov, O., Gulwani, S.: Flashmeta: a framework for inductive program synthesis. ACM SIGPLAN Notices 50(10), 107–126 (2015)CrossRef Polozov, O., Gulwani, S.: Flashmeta: a framework for inductive program synthesis. ACM SIGPLAN Notices 50(10), 107–126 (2015)CrossRef
33.
go back to reference Raychev, V., Vechev, M., Yahav, E.: Code completion with statistical language models. In: ACM SIGPLAN Notices, ACM, vol. 49, pp. 419–428 (2014)CrossRef Raychev, V., Vechev, M., Yahav, E.: Code completion with statistical language models. In: ACM SIGPLAN Notices, ACM, vol. 49, pp. 419–428 (2014)CrossRef
34.
go back to reference Singh, R.: Blinkfill: Semi-supervised programming by example for syntactic string transformations Singh, R.: Blinkfill: Semi-supervised programming by example for syntactic string transformations
35.
go back to reference Solar-Lezama, A.: Program synthesis by sketching. ProQuest, Ann Arbor (2008) Solar-Lezama, A.: Program synthesis by sketching. ProQuest, Ann Arbor (2008)
36.
go back to reference Solar-Lezama, A., Jones, C.G., Bodik, R.: Sketching concurrent data structures. In: ACM SIGPLAN Notices, ACM, vol. 43, pp. 136–148 (2008)CrossRef Solar-Lezama, A., Jones, C.G., Bodik, R.: Sketching concurrent data structures. In: ACM SIGPLAN Notices, ACM, vol. 43, pp. 136–148 (2008)CrossRef
37.
go back to reference Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. ACM SIGOPS Oper. Syst. Rev. 40(5), 404–415 (2006)CrossRef Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. ACM SIGOPS Oper. Syst. Rev. 40(5), 404–415 (2006)CrossRef
38.
go back to reference Udupa, A., Raghavan, A., Deshmukh, J.V., Mador-Haim, S., Martin, M.M., Alur, R.: Transit: specifying protocols with concolic snippets. ACM SIGPLAN Notices 48(6), 287–296 (2013)CrossRef Udupa, A., Raghavan, A., Deshmukh, J.V., Mador-Haim, S., Martin, M.M., Alur, R.: Transit: specifying protocols with concolic snippets. ACM SIGPLAN Notices 48(6), 287–296 (2013)CrossRef
39.
go back to reference Wang, C., Cheung, A., Bodik, R.: Synthesizing highly expressive sql queries from input–output examples. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, ACM, pp. 452–466 (2017)CrossRef Wang, C., Cheung, A., Bodik, R.: Synthesizing highly expressive sql queries from input–output examples. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, ACM, pp. 452–466 (2017)CrossRef
40.
go back to reference Witten, I.H., Mo, D.: Tels: learning text editing tasks from examples. In: Watch what I do, pp. 183–203. MIT Press (1993) Witten, I.H., Mo, D.: Tels: learning text editing tasks from examples. In: Watch what I do, pp. 183–203. MIT Press (1993)
41.
go back to reference Wu, S., Liu, J., Fan, J.: Automatic web content extraction by combination of learning and grouping. In: Proceedings of the 24th International Conference on World Wide Web, ACM, pp. 1264–1274 (2015) Wu, S., Liu, J., Fan, J.: Automatic web content extraction by combination of learning and grouping. In: Proceedings of the 24th International Conference on World Wide Web, ACM, pp. 1264–1274 (2015)
Metadata
Title
Programming by predicates: a formal model for interactive synthesis
Authors
Hila Peleg
Shachar Itzhaky
Sharon Shoham
Eran Yahav
Publication date
30-08-2019
Publisher
Springer Berlin Heidelberg
Published in
Acta Informatica / Issue 1-2/2020
Print ISSN: 0001-5903
Electronic ISSN: 1432-0525
DOI
https://doi.org/10.1007/s00236-019-00340-y

Other articles of this Issue 1-2/2020

Acta Informatica 1-2/2020 Go to the issue

Premium Partner