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

"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);

}