在计算机科学中,抽象释义是基于在有序集合特别是格上的单调函数,计算机程序的语义的可靠逼近理论。它可以被看作对计算机程序的部分执行,获取关于它的语义信息(比如,控制结构、信息流)而不进行所有计算。
| 此条目没有列出任何参考或来源。 (2014年10月8日) |
它的主要具体应用是形式静态分析,关于计算机程序的可能执行的信息的自动提取;比如这种分析有两个主要用途:
- 在编译器内部,分析程序来确定特定优化或变换是否是可适用的;
- 针对缺陷类的程序的调试甚至校验。
抽象释义是 Patrick Cousot 和 Radhia Cousot 所形式化的。