FORMULA is a tool for analyzing and verifying the properties of DSMLs and DSML transformations. It supports Horn domains and Horn transformations as describe in this paper. FORMULA is not yet available for download but this page shows several examples of the software in action.

A Simple Example with Directed Graphs

A directed graph is a set of vertices and a set of edges of the form (u,w) meaning that there is an edge starting at vertex u and ending on vertex w. We can define the domain of directed graphs with a set of n-ary function symbols and a set of constraints on the Herbrand universe defined by those symbols. We write this in FORMULA as shown on the right. The symbol "!" indicates negation as failure, so the constraints explains that a graph is malformed if there is an edge on a vertex that is not in the vertex set.

path4(X,Y,Z,W) <= path3(X,Y,Z), e(Z,W), !=(W,X), !=(W,Y), !=(Y,Z);

path5(X,Y,Z,W) <= path4(X,Y,Z,U), e(U,W), !=(W,X), !=(W,Y), !=(W,Z), !=(W,U);

path6(X,Y,Z,W) <= path5(X,Y,Z,U), e(U,W), !=(W,X), !=(W,Y), !=(W,Z), !=(W,U);

priv cycle2 dimen 2;
priv cycle3 dimen 3;
priv cycle4 dimen 4;
priv cycle5 dimen 4;
priv cycle6 dimen 4;

cycle2(X,Y) <= e(X,Y), e(Y,X);
cycle3(X,Y,Z) <= path3(X,Y,Z), e(Z,X);
cycle4(X,Y,Z,W) <= path4(X,Y,Z,W), e(W,X);
cycle5(X,Y,Z,W) <= path5(X,Y,Z,W), e(W,X);
cycle6(X,Y,Z,W) <= path6(X,Y,Z,W), e(W,X);

In addition to the basic objects that make up a graph, we also give information about the properties of a graph. In the example on the left we define the notion of a directed paths in a graph. For example, a three-path is list of three vertices u,v,w such that there are directed edges from u to v and then from v to w, such that u,v,w are all distinct. The Horn sentence for path3(X,Y,Z) explains this information. The notation !=(X,Y) means that X and Y are disequalities; they cannot be the same vertex. From the definition of a three-path, we can further build up four, five, and six paths. A (simple) cycle in a graph is path that starts and ends on the same vertex. An n-cycle is a cycle made of n distinct vertices. The statements cycle2, cycle3, ..., define the concept of cycles in a graph.

Given these definitions we can ask FORMULA to try and find a model that satisfies a set of properties. For example, we can try to find a model that is not malformed, has a six cycle through vertices X,Y,Z,W, and also has a five cycle that goes through vertices U,Z,Y,V.

FORMULA will build a rooted search space of possible models. The space is rooted with the properties that we want to prove. Child nodes that are linked together through a small circle indicate an AND-branch. AND-branches require every child branch to be valid in the model. The nodes in the tree that are diamond shaped indicate a universal quantification of constraints. For example, in !malform(Q), Q is not bound to any positive term. Therefore, we interpret Q to hold for every object in the model. If we had written !malform(e(X,Y)), then this constraint would only hold for whatever values that X and Y were filled with. The image on the left shows the search space generated by FORMULA. FORMULA generates GraphViz output so that search spaces can be rendered easily. (Click on the picture for a larger version)

Once FORUMLA has found a solution, it gives the user an opportunity to input reasonable values for variables. If the users does not care about the variables values, then FORMULA will automatically fill them with unique constants. For this example, we entered vertex names v1, v2, ..., vn.

FORMULA returns the solution. FORMULA can also try to minimize this particular solution, or it can search the entire space and find the minimal solution. (A solution is considered smaller if it has fewer variable-free definite clauses.)

This is a picture of the above solution. The six cycle is v1->v3->v2->v7->v9->v4->v1. The five cycle is v6->v8->v5->v9->v7->v6. Vertice v7 and v9 overlap in the cycles and the cycles go in opposite directions, as we required.

On-going Work and Publications