CODEWITHSUNDEEP
alloy
Roger Costello
Roger Costello

Reputation: 3209

Traditional software testing versus Alloy instance generation

With traditional software development, tests represent what you meant for the software to say. By executing the tests on the software you see if the software means what you think it means. “This is what I meant to say, did I actually say that?”

Alloy instances show you what you said in the model. You examine the instances and decide if that’s what you meant for the model to say. “This is what you said, is that what you meant to say?”

Do you agree with this distinction between software tests and Alloy instance generation? Is there anything you would add, in the comparison of software tests and Alloy instance generation?

Upvotes: 1

Views: 121

Answers (2)

Loïc Gammaitoni
Loïc Gammaitoni

Reputation: 4171

Yes, you described in your own words the difference between validation (did i build the right thing) and verification (did i build it right).

While "testing" as you named it, is used to verify that the software has been built correctly, Alloy can IMHO be used both for validation and verification, as explained in the following:

Validation: Instance generation from an empty predicate gives you instances conforming to your specification allowing you to have a grasp on what you have specified. You can use the knowledge gained from reviewing those instances to validate your specification. Indeed, those instances will help you answer the question: Are the generated instances mirroring what I meant to specify? (did I build the right thing).

Verification In Alloy , you can also verify that certain property are respected in your specification through the use of assertions. Checking assertions yields possible counter examples whose existence can disprove the compliance of your specification to the violated assertion. If any, the counter-examples generated from checking assertion thus help you answer the question: Did I specify my model correctly w.r.t. my assertions? (did I build it right?).

Upvotes: 2

Taiga Tsutsumi
Taiga Tsutsumi

Reputation: 11

Interesting. I'm using Alloy for representing "test data" (not the software itself). Through this approach I've found that using test data and writing test code is Verification; but specifying test data by formal specification is Validation. When I specifying test data by Alloy, I need to more bigger perspective than that in software testing.

For example, consider the software takes Date data, you must test the software can reject invalid date value. On the other hand when you specifying test data for testing the software by Alloy, you must define data that satisfy the requirement for "Date".

I think that change in those perspective means the difference between Verification and Validation (and the difference between software testing and Alloy instance generation).

Upvotes: 1

Related Questions