Alloy
The Alloy language can be used to describe structures based on a collection of constraints. This created Alloy model can then be analyzed by the Alloy Analyzer, a solver that finds concrete structures that satisfy the constraints defined in the Alloy model. The analysis can be used to generate sample structures or to check properties of these structures by trying to generate counterexamples. Alloy is based on the Z specification language and Tarski’s relational calculus.