TY - GEN
T1 - Solver-based sketching of alloy models using test valuations
AU - Wang, Kaiyuan
AU - Sullivan, Allison
AU - Marinov, Darko
AU - Khurshid, Sarfraz
N1 - Publisher Copyright:
© Springer International Publishing AG, part of Springer Nature 2018.
PY - 2018
Y1 - 2018
N2 - We introduce ASketch, the first framework for sketching models in the Alloy language. The Alloy Analyzer is a SAT-based constraint solver that allows users to create valuations for relations with respect to given constraints and bound on the universe of discourse. Alloy users routinely use the valuations to validate their models: enumerate some valuations and inspect them to detect underconstraints or overconstraints. Our key insight is that valid and invalid valuations enable sketching Alloy models where the user writes a partial model with holes and provides some valuations, and the sketching infrastructure completes the model by synthesizing Alloy fragments for the holes. ASketch offers the following extensions to Alloy: (1) it expands the Alloy grammar, allowing users to write holes in an Alloy model; (2) it can parse regular expressions and automatically generate pools of matching fragments to replace the holes; (3) it includes a solver-based technique that encodes the model with holes, the fragments for each hole, and the expected valuations to a meta-model which completes the holes when solved. Experimental results show that ASketch works well for different Alloy models with various number of holes, providing a promising approach to bring the success of traditional program sketching for imperative and functional programs to declarative, relational logic.
AB - We introduce ASketch, the first framework for sketching models in the Alloy language. The Alloy Analyzer is a SAT-based constraint solver that allows users to create valuations for relations with respect to given constraints and bound on the universe of discourse. Alloy users routinely use the valuations to validate their models: enumerate some valuations and inspect them to detect underconstraints or overconstraints. Our key insight is that valid and invalid valuations enable sketching Alloy models where the user writes a partial model with holes and provides some valuations, and the sketching infrastructure completes the model by synthesizing Alloy fragments for the holes. ASketch offers the following extensions to Alloy: (1) it expands the Alloy grammar, allowing users to write holes in an Alloy model; (2) it can parse regular expressions and automatically generate pools of matching fragments to replace the holes; (3) it includes a solver-based technique that encodes the model with holes, the fragments for each hole, and the expected valuations to a meta-model which completes the holes when solved. Experimental results show that ASketch works well for different Alloy models with various number of holes, providing a promising approach to bring the success of traditional program sketching for imperative and functional programs to declarative, relational logic.
UR - http://www.scopus.com/inward/record.url?scp=85047398688&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85047398688&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-91271-4_9
DO - 10.1007/978-3-319-91271-4_9
M3 - Conference contribution
AN - SCOPUS:85047398688
SN - 9783319912707
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 121
EP - 136
BT - Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Proceedings
A2 - Butler, Michael
A2 - Hoang, Thai Son
A2 - Raschke, Alexander
A2 - Reichl, Klaus
PB - Springer
T2 - 6th International Conference on ABZ Conference on ASM, Alloy, B, TLA, VDM, and Z, ABZ 2018
Y2 - 5 June 2018 through 8 June 2018
ER -