| |||||||||||||
RTLWS: Modeling systems with AlloyRTLWS: Modeling systems with AlloyPosted Nov 8, 2012 10:13 UTC (Thu) by epa (subscriber, #39769)Parent article: RTLWS: Modeling systems with Alloy
The analyzer in Alloy is exhaustiveI understood that the analysis is not 'exhaustive' in the sense that it will find any counterexample that exists. Instead you specify a maximum structure size to check against - a counterexample might be found with 4 elements, or 5 elements, but the larger the number of elements you test the longer it takes to run. I suspect, but do not know for sure, that the Alloy language is Turing-complete and therefore an exhaustive analysis would be impossible.
(Log in to post comments)
RTLWS: Modeling systems with Alloy Posted Nov 8, 2012 19:12 UTC (Thu) by david.a.wheeler (guest, #72896) [Link]
That's my understanding as well, it's not completely exhaustive. But because of the way it works, it can go through exponentially more possibilities than traditional testing could in the same time.
It's actually an interesting compromise compared to traditional formal methods. It doesn't prove *absolutely* something in most cases, but it's a far more rigorous analysis approach than many approaches.
RTLWS: Modeling systems with Alloy Posted Nov 8, 2012 23:04 UTC (Thu) by epa (subscriber, #39769) [Link]
The point is that Alloy has just the same downside as traditional testing: it can be used to prove the presence of bugs, but not their absence. Nothing wrong with that, but the article seems to suggest otherwise.
|
|||||||||||||