Towards A Small Model Theorem for Alloy
Lee Momtahan
Alloy brings automation to Z-style specification and proof. The Alloy
Analyser is a model-finder which tries to refute a formula by searching
within a finite scope for a model of the formula's negation. Although
the Analyser cannot generally validate formulas -- the Alloy
language is undecidable -- it can improve confidence in a formula by
appealing to the small scope hypothesis: "most bugs occur at small
enough scopes to be checked".
However, it is desirable to reduce any dependency on this hypothesis. A
Small Model Theorem gives for some formulas a threshold scope. If no
counter examples are found at the threshold scope, none exist at all.
I will sketch out a Small Model Theorem which for some formulas can give
thresholds on some of the base types. Whenever data-independent systems
are verified in Alloy this theorem should apply and generate thresholds
on the data-independent types.