LARA

// specialized to SimpleCFG
import SimpleCFG._
abstract class TransferFunction[L, CFGStatement] { 
  // L is information propagate through CFG nodes
  def apply(node : CFGStatement, x : L) : L
  // if x describes a set of states,
  // then apply(n,x) describes states obtained from x by executing statement n
}
 
class AnalysisAlgoritm[L,CFGStatement]
               (transferFun : TransferFunction[L, CFGStatement],
		lattice : Lattice{type Elem=L},
		cfg : LabDiGraphImp[CFGStatement])
{
  type Vertex = LVertex[CFGStatement] // node of control-flow graph (see LabDiGraph)
  var facts : Map[Vertex, L] = Map[Vertex,L]() // information for each node (program point)
 
    // set all nodes to bottom
  def init = {facts = Map[Vertex,L]().withDefaultValue(lattice.bottom)} 
 
    // set particular node
  def setNodeFact(v : Vertex, fact : L) = {facts = facts.update(v, fact)}
 
  def computeFixpoint : Unit = {
    var change = true 
    while (change) { // iterate until information stabilizes
      change = false
      for (v <- cfg.V) { // process each CFG node
	val oldFact : L = facts(v)   // we had this before
	var newFact : L = oldFact    // start from this
	for (e <- cfg.inEdges(v)) {  // e.v1 -- e.lab --> e.v2
	  val propagated = transferFun(e.lab, facts(e.v1)) // new info from edge
	  newFact = lattice.join(newFact, propagated)      // join new info
	}
	if (newFact != oldFact) 
	  change = true;
	  facts = facts.update(v, newFact)
	}
      }
    }
  }
  def getResult : Map[Vertex,L] = facts
}