Etienne Kneuss
In this thesis, we explore techniques for the development of recursive functional programs over unbounded domains that are proved correct according to their high-level specifications. We present algorithms for automatically synthesizing executable code, starting from the speci- fication alone. We implement these algorithms in the Leon system. We augment relational specifications with a concise notation for symbolic tests, which are are helpful to characterize fragments of the functionsâ behavior. We build on our synthesis procedure to automatically repair invalid functions by generating alternative implementations. Our approach therefore formulates program repair in the framework of deductive synthesis and uses the existing program structure as a hint to guide synthesis. We rely on user-specified tests as well as automatically generated ones to localize the fault. This localization enables our procedure to repair functions that would otherwise be out of reach of our synthesizer, and ensures that most of the original behavior is preserved. We also investigate multiple ways of enabling Leon programs to interact with external, un- trusted code. For that purpose, we introduce a precise inter-procedural effect analysis for arbitrary Scala programs with mutable state, dynamic object allocation, and dynamic dispatch. We analyzed the Scala standard library containing 58000 methods and classified them into sev- eral categories according to their effects. Our analysis proves that over one half of all methods are pure, identifies a number of conditionally pure methods, and computes summary graphs and regular expressions describing the side effects of non-pure methods. We implement the synthesis and repair algorithms within the Leon system and deploy them as part of a novel interactive development environment available as a web interface. Our implementation is able to synthesize, within seconds, a number of useful recursive functions that manipulate unbounded numbers and data structures. Our repair procedure automatically locates various kinds of errors in recursive functions and fixes them by synthesizing alternative implementations.
EPFL2016
