Eutopia

The KeY Project

The KeY program is a tool for formal specification and verification of object-oriented software. During the summer course of Formal Methods in Software Engineering, I had the oportunity to practice with the tool on verifying first-order predicate logic clauses, dynamic logic problems for Java Card, simple Java programs and loops. The KeY tool also supports specifications written in JML or OCL (I tried JML). The java graphical interface, is pretty simple and easy to use (screenshot).

Start KeY via webstart here and try some examples here. 

As a project started in November 1998 at the University of Karlsruhe and now is also jointly developed by the Chalmers University of Technology in Gothenburg, and the University of Koblenz. It is licensed under the GPL (source). The verifications tool is also supported for C programming language, Hoare Calculus, Hybrid Systems and as an Eclipse plugin. See here for all the available downloads.

Useful links

• wikipedia
• The KeY project homepage
• Summer Academy of University Koblenz
• Sequent calculus
• Java Modeling Language [1] [2]
• Design by contract

Graph Algorithms

The following post is about some graph algorithms that I found interesting (or tricky) the last Spring Semester.

Depth First Search (DFS)

One starts at the root (selecting some node as the root in the graph case) and explores as far as possible along each branch before backtracking.

So the pseudocode should be like this:

• DFS(v : vertex)
• Mark v as Pre-Visited
• For all vertices i adjacent to v that are not Pre-Visited
•  DFS(i)
• Mark v as Post-Visited

Breadth First Search (BFS)

BFS is a graph search algorithm that begins at the root node and explores all the neighboring nodes. Then for each of those nearest nodes, it explores their unexplored neighbor nodes, and so on, until it finds the goal.

• Put the root node on the queue.
• Pull a node from the beginning of the queue and examine it.
  • If the searched element is found in this node, quit the search and return a result.
  • Otherwise push all the (so-far-unexamined) successors (the direct child nodes) of this node into the end of the queue, if there are any.
• If the queue is empty, every node on the graph has been examined -- quit the search and return "not found".
• Repeat from Step 2. 

Useful links: [wikipedia] [boost]
Useful examples/applets: [Breadth First Traversal] [lupihno.de] [T-SQL: BFS Implementation]

Finding Strongly Connected Components in a graph

 The easiest algorithm I find to solve this problem was Kosaraju's algorithm. Given a graph: G, this is how you compute the SCC:

• DFS(G) to compute finishing (post) times for each vertex v 
• Reverse G graph to G^T
• DFS(G^T), but in reverse post (finishing times) order as computed to step 1.
• Now, each time DFS(G^T), calls explore() you simply draw a SCC

More details about the implementation you can find in this blog.

Useful links: [scienceblogs.com/goodmath] [wikipedia] [Explanation and Proof] [SCC kent.edu] [Tarjan's Algorithm]
Useful examples/applets: [(.pdf) cs.huji.ac.il] [(.pdf) SCC (berkeley)]

Finding the shortest route in a graph with Dijkstra's Algorithm

Dijkstra's algorithm, is a graph search algorithm that solves the shortest path problem. A limitation is that the graph cannot contain negative weight edges. This algorithm is also used in routing. So, let us see -a not so strict- step-by-step the way this algorithm works:

• Choose the starting vertex and set its value to zero, for all the other vertexes set their values to infinity.
• Mark the starting (current) vertex as visited.
• Update distance on the vertexes that can be immediately reached from the current vertex.
• Update the current vertex to the unvisited vertex that can be reached by the shortest path from the starting vertex.
• Repeat the lat 3 steps until every vertex is examined.
  

Useful links: [wikipedia]
Useful examples/applets: [ceid.patras.gr] [unf.edu] [dgp.toronto.edu]

Finding the shortest route in a graph with negative edge weights: Bellman-Ford Algorithm

The Bellman–Ford algorithm, sometimes referred to as the Label Correcting Algorithm, computes single-source shortest paths in a weighted digraph (where some of the edge weights may be negative). Dijkstra's algorithm solves the same problem with a lower running time, but requires edge weights to be non-negative. Thus, Bellman–Ford is usually used only when there are negative edge weights.

Why use such a thing?

According to Robert Sedgewick, "Negative weights are not merely a mathematical curiosity; [...] [they] arise in a natural way when we reduce other problems to shortest-paths problems," and he gives the specific example of a reduction from the NP-complete Hamilton-path problem. If a graph contains a cycle of total negative weight then arbitrarily low weights are achievable and so there's no solution; Bellman-Ford detects this case.

Implementation here.

Useful applet: [links.math.rpi.edu]

Finding the Minimum Spanning Tree with the Kruskal's Algorithm

This algorithm is used in graph theory for finding the minimum weight spanning tree (or MST) of a connected weighted graph. Let's see how the algorithm works with the following pseudocode:

• Start with a forest F of trees, where each tree is a vertex of our graph.
• Use a set S which contains all the edges of the graph
• While S is not empty:
• Fetch the lightest edge (the edge with the minimum weight)
• if that edge connects two different trees, then add it to the forest, combining two trees into a single tree.
• else discard it (example, when creating a cycle)
• Return the MST

Finding the Minimum Spanning Tree with the Prim's Run

 Known also as the DJP algorithm, the Jarník algorithm, or the Prim-Jarník algorithm.

• Prim(v : vertex)
• Start from vertex v and connect it with the vertex that uses the minimum edge.
• Repeat until connecting all vertices to the tree:
• Fetch the lightest edge that connects with the existing tree
• If no cycle created, add that edge to the tree.
• Return the MST

Useful links: [wikipedia] [mathematical programming]
Useful examples/applets: [ceid.patras.gr]

For finding the MST try also the Borůvka's_algorithm

-- comments disabled due to spamming --