Comfusy: A Tool for Complete Functional Synthesis

Synthesis of program fragments from specifications can make programs easier to write and easier to reason about. We present Comfusy, a tool that extends the compiler for the general-purpose programming language Scala with (non-reactive) functional synthesis over unbounded domains. Comfusy accepts expressions with input and output variables specifying relations on integers and sets. Comfusy symbolically computes the precise domain for the given relation and generates the function from inputs to outputs. The outputs are guaranteed to satisfy the relation whenever the inputs belong to the relation domain. The core of our synthesis algorithm is an extension of quantifier elimination that generates programs to compute witnesses for eliminated variables. We present examples that demonstrate software synthesis using Comfusy and illustrate how synthesis simplifies software development.


Editeur(s):
Touili, Tayssir
Cook, Byron
Jackson, Paul
Publié dans:
Proceedings of the 22nd International Conference on Computer-Aided Verification (CAV), 6174, 430-433
Présenté à:
22nd International Conference on Computer Aided Verification, Edinburgh, Scotland, UK, July 15-19, 2010
Année
2010
Publisher:
Springer
Mots-clefs:
Note:
Tool Presentation
Laboratoires:




 Notice créée le 2010-12-01, modifiée le 2019-08-12

Preprint:
Télécharger le document
PDF

Évaluer ce document:

Rate this document:
1
2
3
 
(Pas encore évalué)