Date of Award


Document Type

Honors Thesis



First Advisor

Tim Wahls




The jmle tool executes JML specifications (formal specifications for Java classes) by translating them to constraint programs. This tool has useful applications such as prototyping and specification testing; however, it uses backtracking, which takes exponential time. To decrease jmle's running time, we can add new constraint handling rules that remove elements from the domains of variables, thus reducing the search space for backtracking. The goal of our project is to improve the running time of jmle by adding rules concerning properties of and relationships between sets. For example, we have treated the size of a set as a finite domain variable instead of as a single integer, so infeasible areas of the search space can be more quickly eliminated. We have also bounded sets from both above and below with collections of their elements. The addition of our rules has dramatically decreased the running time of some specifications in jmle. However, each new rule adds some overhead in running time, so it is important to add rules that are beneficial enough to outweigh this cost. We conclude that the careful addition of constraint handling rules can have a positive impact on jmle's performance.