Milao : a novel framework for mixed imperative and declarative formulation and solving of structural constraints
MetadataShow full item record
Advances in constraint solving and increases in processing power have enabled new approaches for automating specification-based testing. However, writing specifications and scaling techniques that utilize them remain challenging. We introduce Milao -- a novel framework for mixed imperative and declarative formulation and solving of structural constraints -- which addresses both these challenges. One, Milao introduces a mixed style for writing specifications using a combination of declarative and imperative styles, which provides flexibility in specification formulation and reduces its burden on the user. Two, it introduces a mixed technique for solving constraints using a combination of solvers in synergy. As enabling technologies, the Alloy tool-set and the Java PathFinder model checker are used. Initial experiments witness the benefits of our framework.