When I search for “small scope hypothesis”, I find something along the lines of “a high proportion of errors can be found by testing a program for all test inputs within some small scope”.
So, the question: is Alloy used for generating test cases? If yes, what is the workflow?
It’s not testing in the strict sense of testing, but rather saying that the whole state space is explored up to a certain bound. Which is akin to “testing” all combinations in that bound.
That being said, Sarfraz Khurshid and his colleagues have worked a lot on the topics of Alloy and testing, under various guises.
I mean, I understand how Alloy is used for modeling. Now I once again have a vague idea that it could also be used for testing. Here’s an interesting paper: Simple Testing Can Prevent Most Critical Failures: An Analysis of Production Failures in Distributed Data-Intensive Systems.
I wonder if Alloy could be used for enumerating test cases so that edge cases get tested along with happy paths. According to the paper and the hypothesis, this doesn’t have to be exhaustive to eliminate a large portion of problems.
I used to have some ideas about this. In a nutshell, I think programming APIs should be designed in an Alloy like language and then mechanically mapped to the implementation language. I think you can then automatically create test cases, verifiers that verifies the information that passes the API boundary, and automatically create mocks that react according to the specification.
In java terms, I’d like to see syntax changes in Alloy (or another language) that maps close to the Java interface model. The Alloy code is then used to generate the interfaces. This is the proper direction since Java has far more structural complexity than Alloy. It is easier for Java to adhere to Alloy than Alloy to understand the Java code.
Using proxying techniques, you can then intercept & verify the calls from the consumer of the API and the provider of the API. Same techniques could be used to create a proxy that answers something but that is according to specification. The extremely powerful reflection model of Java can help with this. With the Alloy code, it should be possible to create test cases that are mapped to Java.
I made a crappy video for discotec but not sure this was well understood.
The traditional model where we try to specify implementations is imho not possible due to the immense complexity of implementation code. By limiting the specification to an API and enforcing this API on the implementation we might have a chance. I think. I did try looking for universities or companies that were willing to work on this but so far I found it immensely difficult to get the formal world and the software engineering world in the same vicinity. They seem to hate each other’s guts.
About the existing testing stuff you can find in Alloy: I looked into this some years ago and it was all very old and stale. However, if you find anything, let me know.
Hm. This could be easier to implement in a lisp than in any other language.
There’s a new property-based testing framework in clojure that involves some kind of modeling. I wonder if this could be a step towards this idea of enumerating edge cases using Alloy.
Here’s the talk and the docs:
Intro to Fugato (by David Nolen) – https://www.youtube.com/watch?v=UBUMzWwm2Gc
Once again, I think you should look at Sarfraz Khurshid’s publications. There was a tool called TestEra, related to testing Java using Alloy.
Thanks for pointing out this tool specifically. I was a bit lost, when I looked at the list of Sarfraz Khurshid’s publications. A lot of work is being done in this direction, apparently.