Exploring ideas for Pattern-Based Debugging of Declarative Models
Derek Rayside and Paul Ward
Pattern-based debugging compares the engineer’s model to a pre-computed library of patterns, and generates discriminating examples that help the engineer decide if the model’s constraints need to be strengthened or weakened. A number of tactics are used to help connect the generated examples to the text of the model. This technique augments existing example/counter-example generators and unsatisfiable core analysis tools, to help the engineer better localize and understand defects caused by complete overconstraint, partial overconstraint, and underconstraint. The talk mainly focuses on demonstrating initial ideas and examples to show how the technique is applied to localizing, understanding, and fixing a defect in an Alloy model.