⚠: this note is very WIP, won't provide you any useful information; just go ahead for the chapter in the book and follow the mathematics, they're very well explained there.
transitional style is generally easier to be defined for complex languages
dynamic jumps: e.g. function calls, exception raises
with gotos, program constructs can't boil down to a particular construct like
good fit for reachability problem: all the intermediate program states are exposed as semantics
A state : a pair of a program label and the machine state
define the set 𝕊 of states between which a single-step transition relation is to be defined
define the relation between states , and let be its natural powerset lifted version:
given a program of the language with its set , let
the concrete semantics, defined as the set of all the reachable states of the program, is the least fixpoint of the continuous function :
concrete semantic function:
concrete semantic domain:
The concrete semantics is not what we implement as a static analyzer; its implementation is rather equivalent to implementing an interpreter that actually runs the programs of the target language.
: abstract domain
: abstract semantic function
CPO (complete partial order): a partial order
has a least element: bottom
such that each totally ordered subset has a least upper bound
This is the one Julia's abstract interpretation uses.