静态分析

差别

这里会显示出您选择的修订版和当前版本之间的差别。

到此差别页面的链接

--- 静态分析 [2023/08/25 22:22] – cyh
+++ 静态分析 [2023/08/25 22:43] (当前版本) – cyh
@@ 行 1: / 行 1: @@
 ====== 静态分析 ======
-===== 导言与例子 =====
+===== 导言 =====
 理论上来说，静态分析问题是不可判定的（undecidable）；实际上，可以通过过度近似（over-approximation）来得到准确的单边答案，也就是可以保证假阴性和假阳性不会同时出现。
@@ 行 9: / 行 9: @@
 $R$ 是不可判定的，因此无法通过静态分析确定程序是否有问题。但是可以通过计算 $R$ 的超集来“过度近似” $R$。这样，对于发现的问题，可能会出现假阳性；但如果没发现问题，可以确定肯定没有问题。
+===== 抽象解释(Abstract Interpretation) =====
+抽象解释是一种静态分析技术，它把程序内的值用**抽象**的描述符表示，并使用抽象的模拟器来**解释**运行程序。
+两个函数：
+  * $\gamma()$ 将抽象的描述符具体化
+  * $\alpha()$ 将具体的值抽象化
+对于一个具体的值 $c$，我们有：$\gamma(\alpha(c))\supseteq \{c\}$，这就是“过度近似”。
+例子：
+对于函数 $f(x,y) = (16y+3)\cdot(2x+1)$，是否存在自变量 $x, y$ 使得函数的输出值为 $51$ 或者 $10$？
+我们可以将这里的值抽象为 $\{E,O,?\}$ 中的一个值，分别表示偶数、奇数与未知奇偶。基于这样的抽象，我们可以定义抽象运算规则：
+抽象加法：
+<code>
+#+|	?	E	O
+--+-----------------------
+? |	?	?	?
+E |	?	E	O
+O |	?	O	E
+</code>
+抽象乘法：
+<code>
+#*|	?	E	O
+--+-----------------------
+? |	?	E	?
+E |	E	E	E
+O |	?	E	O
+</code>
+定义抽象运算后，自变量 $x, y$ 被抽象为 $?$，在经过抽象解释之后，我们可以得到 $f(x,y)=O$ 肯定是奇数。因此该函数的值不可能为 $10$，有可能是 $51$。
 {{tag>计算机科学}}

静态分析.1693002150.txt.gz · 最后更改: 2023/08/25 22:22 由 cyh