[sriram_malhar]

Alloy is a specification language. To verify the specification, the alloy analyser (a model checker) has to artificially create some number of instances and simulate it.

Prolog is an executable language. You, the user, give it a database, and it searches for solutions that satisfies constraints. It doesn't create the basic facts on its own.

There exists a compiler from imperative alloy to prolog to make this transition.

[yesenadam]

Hmm well, not all Prolog uses fit the 'give it a database' model..(In fact I can't think of any Prolog programs I've seen that do fit it) e.g. I was tried the the finite domain solver in Gnu Prolog[0] recently, I wanted arrangements of about 15 shapes that obeyed certain constraints, the program was 6 very short lines! I didn't tell it anything except the constraints.

But yeah, alloy and alloy* sound fascinating, I must investigate further, thank you.

[0]http://www.gprolog.org/manual/html_node/gprolog054.html

[sriram_malhar]

You are right. Constraint solving in general is a specific area that does not require a knowledge base; instead it is a search for a solution from the specified domain that fits all the specified constraints. Here there is considerable overlap between prolog, alloy and z3.

However, most general prolog programming has the same requirements placed on other executable languages, to transform, store and communicate data. Alloy is not the tool for this aspect.