nach oben

Acta Informatica

Erschienen in:

30.08.2019 | Original Article

Programming by predicates: a formal model for interactive synthesis

verfasst von: Hila Peleg, Shachar Itzhaky, Sharon Shoham, Eran Yahav

Erschienen in: Acta Informatica | Ausgabe 1-2/2020

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Vorheriger Artikel Synthesis from hyperproperties

Nächster Artikel Synthesizing optimally resilient controllers

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

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.

Albarghouthi, A., Gulwani, S., Kincaid, Z.: Recursive program synthesis. In: International Conference on Computer Aided Verification, pp. 934–950. Springer (2013)

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., Fisman, D., Singh, R., Solar-Lezama, A.: Sygus-comp 2016: Results and analysis. arXiv preprint arXiv:1611.07627 (2016)

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)

Anton, T.: Xpath-wrapper induction by generalizing tree traversal patterns. In: Lernen, Wissensentdeckung und Adaptivitt (LWA) 2005, GI Workshops, Saarbrcken, pp. 126–133 (2005)

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)

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

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

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.

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.

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.

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.

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.

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.

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.

Higman, G.: Ordering by divisibility in abstract algebras. Proc. Lond. Math. Soc. 3(1), 326–336 (1952)MathSciNetCrossRef

17.

Jha, S., Seshia, S.A.: A theory of formal synthesis via inductive learning. Acta Inform. 54, 693–726 (2017)MathSciNetCrossRef

18.

Kruskal, J.B.: Well-quasi-ordering, the tree theorem, and vazsonyi’s conjecture. Trans. Am. Math. Soc. 95(2), 210–225 (1960)MathSciNetMATH

19.

Landauer, J., Hirakawa, M.: Visual awk: a model for text processing by demonstration. In: vl, pp. 267–274 (1995)

20.

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.

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.

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.

Le, V., Perelman, D., Polozov, O., Raza, M., Udupa, A., Gulwani, S.: Interactive program synthesis (2017)

24.

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.

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.

Osera, P.-M., Zdancewic, S.: Type-and-example-directed program synthesis. In: ACM SIGPLAN Notices, ACM, vol. 50, pp. 619–630 (2015)CrossRef

27.

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.

Peleg, H., Shoham, S., Yahav, E.: D3: Data-driven disjunctive abstraction. In: Verification, Model Checking, and Abstract Interpretation, pp. 185–205. Springer (2016)

29.

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.

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.

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.

Polozov, O., Gulwani, S.: Flashmeta: a framework for inductive program synthesis. ACM SIGPLAN Notices 50(10), 107–126 (2015)CrossRef

33.

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.

Singh, R.: Blinkfill: Semi-supervised programming by example for syntactic string transformations

35.

Solar-Lezama, A.: Program synthesis by sketching. ProQuest, Ann Arbor (2008)

36.

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.

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.

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.

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.

Witten, I.H., Mo, D.: Tels: learning text editing tasks from examples. In: Watch what I do, pp. 183–203. MIT Press (1993)

41.

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)

Titel: Programming by predicates: a formal model for interactive synthesis
verfasst von: Hila Peleg
Shachar Itzhaky
Sharon Shoham
Eran Yahav
Publikationsdatum: 30.08.2019
Verlag: Springer Berlin Heidelberg
Erschienen in: Acta Informatica / Ausgabe 1-2/2020
Print ISSN: 0001-5903
Elektronische ISSN: 1432-0525
DOI: https://doi.org/10.1007/s00236-019-00340-y

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 1-2/2020

Preface for the SYNT

A symbolic algorithm for lazy synthesis of eager strategies

Practical synthesis of reactive systems from LTL specifications via parity games

Parameterized synthesis of self-stabilizing protocols in symmetric networks

Safety synthesis for incrementally stable switched systems using discretization-free multi-resolution abstractions

Synthesis from hyperproperties