This page provides a detailed explanation for several interesting examples. The research papers listed on the documentation page present several other examples. Finally, the source code for many more examples can be found inside the examples module under the project documentation section.

graph k-coloring problem

Graph coloring is a well-known problem in graph theory. For this particular example, the goal is to find a way of coloring the nodes of a graph, using at most k different colors, such that no two adjacent nodes share the same color.

To represent graphs is Java, we'll use a set of nodes and a set of edges. Nodes and edges are represented as separate classes. A node can be assigned an arbitrary integer label, whereas an edge simply holds pointers to source and destination nodes and a cost.

To solve this problem, we simply define an instance method (namely color) that takes the number of colors k and annotate it with a specification which declaratively and formally states what the effects of the method should be, i.e. what the heap should look like in the post-state, and not how to arrive at that heap.

In order to assign colors to nodes, we could have used the Node.label field. Instead, however, we decided to explicitly return the mapping between nodes and colors by returning a new instance of the Java Map class, just to illustrate the usage of Java maps and how the creation of new objects can be specified.

For each supported Java collection class, we have defined several specification fields to model its abstract state. For instance, for Java sets, spec field named elts refers to elements of the set. Similarly, elts for maps refers to map entries (which are of type K -> V). For maps, two extra fields are defined, keys and values, that respectively resolve to map keys and map values. A fuller description of specification fields for Java collections can be found on this page.

The @FreshObjects annotation is used to specify that one instance of java.util.Map<Node, Integer> should be created and added to the heap. Since that instance is going to be the only instance of that type, which is the same as the return type of the method, the solver will have to assign that instance to the method's return value. We want the solver to compute the content of that map, so we must explicitly state that the content of the map (return.elts) is modifiable by using the @Modifies annotation. To constrain the content of the map, we use the @Ensures annotation to specify the post-condition. In this case, we say that the set of keys of the return map (return.keys) must be exactly equal to the set of nodes of this graph (because we want to assign a color to every node). The keys of the return map must all be between 1 and k, which is asserted in the second line of the post-condition. To prevent the adjacent nodes from having the same color, we specify that for all edges, the end nodes must be assigned different colors. Finally, since Squander by default encodes only integers that found on the heap, we have to explicitly tell Squander to use all integers, because we want all integers from 1 to k to be included.

class Graph {
  class Node {
    public final int label;
    public Node(int label) { this.label = label; }
  }
  
  class Edge {
    public final Node src, dest;
    public final int cost;
    public Edge(Node src, Node dest, int cost) {
        this.src = src;
        this.dest = dest;
        this.cost = cost;
    
  }
  
  private Set<Node> nodes = new LinkedHashSet<Node>();
  private Set<Edge> edges = new LinkedHashSet<Edge>();
    
  @Ensures({
      "return.keys = this.nodes.elts"
      "all c : return.vals | c > 0 && c <= k",
      "all e : this.edges.elts | return.elts[e.src] != return.elts[e.dst]"
  })
  @Modifies("return.elts")
  @Options(ensureAllInts=true)
  @FreshObjects(cls = Map.class, typeParams={Node.class, Integer.class}, num = 1)
  public Map<Node, Integer> color(int k) {
      return Squander.exe(this, k);
  }
}

travelling salesman problem

In this version of the Travelling Salesman Problem (TSP), our goal is to find a path (sequence of edges) in the graph that starts from the given startNode node, visits all nodes in the graph and returns to the starting node, whose cost is less than the given maxCost number. We'll use the same classes to represent graphs as in the previous example.

One way to formally specify this problem is shown below. We decided that the tsp method returns a sequence of edges to represent the path (alternatively it could return a sequence of nodes). The post-condition for the tsp method ensures the following:

  • the resulting edges are chosen only from the set of graph edges
  • the resulting edges cover all nodes
  • the number of the resulting edges is equal to the number of nodes (because we start and finish in the same node)
  • the resulting edges are connected
  • the first and the last node on the path is equal to the given start node
  • the cost is less than or equal to the given max cost

@Ensures( {
    "return[int] in this.edges.elts",
    "return[int].(src + dst) = this.nodes.elts",
    "return.length = #this.nodes.elts",
    "all i : int | i >= 0 && i < return.length - 1 => return[i].dst = return[i+1].src",
    "startNode = return[0].src && startNode = return[return.length - 1].dst"
    "(sum i : int | return[i].cost) <= maxCost"
})
@Modifies( { "return.length""return.elems" })
@FreshObjects(cls = Edge[].class, num = 1)
@Options(ensureAllInts = true)
public Edge[] tsp(Node startNode, int maxCost) {
    return Squander.exe(this, startNode, maxCost);
}