Statement simplification separates

• set of side effects (sequence of simple statements)
• computation result (denoted by potentially fresh variable)

Example signature:

  def simp(e : Expr) : Pair[VarName, List[Statement]] = ...

We should have the following (pseudo code) equation:

simp(e1 + e2) =
  val (v1,st1) = simp(e1)
  val (v2,st2) = simp(e2)
  val v3 = getFreshVar
  val st3 = (Assignment(v3 = v1 + v2))
  return (v3, st1 ::: st2 ::: List(st3))

Apply to

x.next.next.prev = y
y = x.next.next
(x = null | x.next == y)

Short-circuit evaluation.

Compiler intermediate representation is sometimes more convenient than source code

• or verification system can repeat the compilation process from source to relations (guarded commands)
• Compiler Construction Course