Pattern Validation - lgwagner/SpeAR GitHub Wiki

SpeAR patterns are useful for capturing functionality that cannot be expressed in the SpeAR base language. However, developing a pattern that expresses exactly what a user intends can be a tricky process. Fortunately, SpeAR provides a capability to both simulate, and prove properties, over patterns.

Users can right-click on a SpeAR pattern and select "Simulate SpeAR Pattern", as shown in the figure below. It will open up an Excel spreadsheet (user must have Excel or comparable program installed) that can be used to simulate the functionality of the pattern.

Once the user has simulated the pattern and believes it is correct, property proving can be used to ensure no corner cases were missed. Users can right-click on a SpeAR pattern and select "Analyze Pattern" and the tool will model check the pattern and ensure it complies with all stated properties.