Skip to main content
main-content

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

16.03.2019 | SPIN 2017 | Ausgabe 3/2019

International Journal on Software Tools for Technology Transfer 3/2019

EdSketch: execution-driven sketching for Java

Zeitschrift:
International Journal on Software Tools for Technology Transfer > Ausgabe 3/2019
Autoren:
Jinru Hua, Yushan Zhang, Yuqun Zhang, Sarfraz Khurshid
Wichtige Hinweise

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Abstract

Sketching is a synthesis approach that allows users to provide high-level insights into a synthesis problem and let synthesis tools complete low-level details. Users write sketches—partial programs that have “holes” and provide test assertions as the correctness criteria. The sketching techniques fill the holes with code fragments such that the complete program satisfies all test assertions. Traditional techniques translate the sketching problem to propositional satisfiability formulas and leverage SAT solvers to generate programs with the desired functionality. While effective for a range of small well-defined domains, such translation-based approaches have a key limitation when applying to real applications: They require either translating all relevant libraries that are invoked directly or indirectly by the given sketch or creating models of those libraries, which requires much manual effort. This paper introduces execution-driven sketching, a novel approach for synthesizing Java programs with on-demand candidate generation. The key novelty of our work is to leverage runtime behavior to prune a large amount of search space. EdSketch explores the actual program behaviors in the presence of libraries and sketches small parts of real-world applications, which may use complex constructs of modern languages, such as reflection, native calls and File I/O. We further leverage a set of pruning strategies based on Java syntax to expedite the synthesis process. EdSketch embodies our approach in two forms: a stateful search based on the Java PathFinder model checker; and a stateless search based on re-execution inspired by the VeriSoft model checker. Experimental results show that EdSketch can complete some sketches that contain complex constructs in the presence of libraries, recursive procedures and advanced features like reflection. Without translating to SAT, EdSketch ’s performance compares well with the SAT-based Sketch system for a range of small but complex data structure subjects.

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

  • über 69.000 Bücher
  • über 500 Zeitschriften

aus folgenden Fachgebieten:

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

Testen Sie jetzt 30 Tage kostenlos.

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 50.000 Bücher
  • über 380 Zeitschriften

aus folgenden Fachgebieten:

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




Testen Sie jetzt 30 Tage kostenlos.

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 58.000 Bücher
  • über 300 Zeitschriften

aus folgenden Fachgebieten:

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




Testen Sie jetzt 30 Tage kostenlos.

Literatur
Über diesen Artikel

Weitere Artikel der Ausgabe 3/2019

International Journal on Software Tools for Technology Transfer 3/2019 Zur Ausgabe

Premium Partner

    Bildnachweise