⚠: 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 raiseswith gotos, program constructs can't boil down to a particular construct like

`while`

-loop

good fit for reachability problem: all the intermediate program states are exposed as semantics

A state $s \in 𝕊$: a pair $(l, m)$ of a program label $l$ and the machine state $m$

define the set 𝕊 of states between which a single-step transition relation $\hookrightarrow$ is to be defined

define the $s \hookrightarrow s^\prime$ relation between states $s, s^\prime \in 𝕊$, and let $Step$ be its natural powerset lifted version: $Step(X) = \{s^\prime | s \hookrightarrow s^\prime, s \in X \}$

given a program of the language with its set $I \subseteq 𝕊$, let $F(X) = I \cup Step(X)$

the concrete semantics, defined as the set of all the reachable states of the program, is the least fixpoint of the continuous function $F$: $\text{lfp} F = \cup_{i \ge 0} F^i(\emptyset)$

Definition: Semantic Domain and Semantic Function

*concrete semantic function*: $F: 𝒫(𝕊) \rightarrow 𝒫(𝕊)$*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 versions:

$I^{\#}$

$\cup^{\#}$

$Step^{\#}$

$𝕊^{\#}$:

*abstract domain*$F^{\#}: 𝕊^{\#} \rightarrow 𝕊^{\#}$:

*abstract semantic function*

*CPO (complete partial order)*: a partial orderhas a least element:

*bottom*$\bot$such that each totally ordered subset has a least upper bound

This is the one Julia's abstract interpretation uses.

© Shuhei Kadowaki. Last modified: 2022-07-24. Website built with Franklin.jl and the Julia programming language.