Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
10329447 | Electronic Notes in Theoretical Computer Science | 2005 | 16 Pages |
Abstract
Alloy is an extension of first-order logic for modelling software systems. Alloy has a fully automatic analyser which attempts to refute Alloy formulae by searching for counterexamples within a finite scope. However, failure to find a counterexample does not prove the formula correct. A system is data-independent in a type T if the only operations allowed on variables of type T are input, output, assignment and equality testing. This paper gives a theorem in a language closely related to Alloy, which applies to models of data-independent systems. The theorem calculates for such types T a threshold size. If no counterexamples are found at the threshold, the theorem guarantees that increasing the scope on T beyond the threshold still yields no counterexamples, and can complete the analysis for data-independent systems.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Lee Momtahan,