more memo:

- add a link to the paper
- explain the difference from the example in the paper
- better display of `IsDefined`

dataflow.jl

@@ -84,8 +84,7 @@ show(io::IO, ::BotElement) = print(io, "⊥")
 
 # Part 3: dataflow analysis
 
-# Note: the paper uses U+1D56E MATHEMATICAL BOLD FRAKTUR CAPITAL C for this
-typealias AbstractValue Dict{Symbol,LatticeElement}
+# Note: the paper (https://api.semanticscholar.org/CorpusID:28519618) uses U+1D56E MATHEMATICAL BOLD FRAKTUR CAPITAL C for this
 const AbstractValue = Dict{Symbol,LatticeElement}
 
 # Here we extend lattices of values to lattices of mappings of variables
@@ -98,6 +97,10 @@ const AbstractValue = Dict{Symbol,LatticeElement}
 <=(X::AbstractValue, Y::AbstractValue) = X⊓Y == X
 <(X::AbstractValue, Y::AbstractValue)  = X<=Y && X!=Y
 
+# Note: we solve an existential data-flow problem below, so:
+# - initialize states with `⊥` instead of `⊤`
+# - use `!<=` instead of `!<=` to check whether or not the instruction makes a change
+# - use `⊔` instead of `⊓` to update states
 function max_fixed_point(P::Program, a₁::AbstractValue, eval) where {Program<:AbstractVector{Stmt}}
     n = length(P)
     bot = AbstractValue( v => ⊥ for v in keys(a₁) )
@@ -146,6 +149,7 @@ end
 struct IsDefined <: LatticeElement
     is::Bool
 end
+show(io::IO, isdef::IsDefined) = print(io, isdef.is ? "defined" : "undefined")
 
 const undef = IsDefined(false)
 const def   = IsDefined(true)