目录
8 关系: 伽罗瓦连接，克纳斯特－塔斯基定理，稀疏有條件的常數傳播，靜態程序分析，计算机逻辑，Polyspace，指称语义，海森堡bug。
伽罗瓦连接
在数学中，特别是在序理论中，伽罗瓦连接是在两个偏序集（"poset"）之间的特殊的对应。伽罗瓦连接一般化了伽罗瓦理论中在子群和子域之间的对应。它们用于各种数学理论和编程理论中。 伽罗瓦连接要弱于在涉及到的两个偏序集之间的同构，但是所有的伽罗瓦连接都引发特定在两个子偏序集之间的同构。.
查看 抽象释义和伽罗瓦连接
克纳斯特－塔斯基定理
在数学领域序理论和格理论中，Knaster–Tarski 定理，得名于 Bronisław Knaster 和阿尔弗雷德·塔斯基，它声称: 这个定理的一种逆命题由 Anne C. Davis 证明了: 如果所有次序保持函数 f: L → L 有不动点，则 L 是完全格。.
稀疏有條件的常數傳播
在電腦科學的領域，稀疏有條件的常數傳播（sparse conditional constant propagation）是一個优化的技術，常用在以静态单赋值形式（SSA）進行最佳化的編譯器，它可以移除程式中一些無用的程式碼以及進行常數傳播。然而，它比起死碼刪除以及常數傳播更加的強大。 這個演算法在SSA中藉由實現程式碼的抽象释义來運作。在實現抽象釋義的過程中，它使用常數的格（Lattice）以及在全域環境對應SSA變數到這個格的數值，演算法的關鍵在於它如何處理分支指令的詮釋，當意外發生，分支的狀態盡可能評估最佳的方式，使綁定變數的抽象數值更加的精確。在需要數值要絕對精確的案例之下，抽象執行可以決定分支的方向。如果數值不是常數，或是一個變數在為定義的狀態，那麼兩個分支的方向必須都保留。 完成後的抽象表現，指令不會到達被標注為死碼的程式區段，SSA變數在常數會使用到的地方可能會以內連（inline）的方式實現。.
靜態程序分析
態程序分析（Static program analysis）是指在不執行计算机程序的條件下，進行程序分析的方法。有些程序分析需要在程序執行時才能進行，這種程序分析稱為。大部份的靜態程序分析的對象是針對特定版本的源代码，也有些靜態程序分析的對象是目标代码。靜態程序分析一詞多半是指配合靜態程序分析工具進行的分析，人工進行的分析一般稱為或代码审查。 靜態程序分析的複雜程度依所使用的工具而異，簡單的只考慮個別语句及声明的行為，複雜的可以分析程序的完整源代码。不同靜態程序分析技术对分析得到的資訊的用途也有所不同，簡單的可以是高亮标识可能存在的代碼錯誤（如lint），複雜的可以是形式化方法，也就是用數學的方式證明程式的某些行為符合其設計规约。 軟體度量和反向工程可以視為一種靜態程序分析的方式。在實務上，在定義所謂的軟體品質指標（software quality objectives）後，軟體度量的推導及程序分析常一起進行，在開發嵌入式系統時常會用這種方式進行。 靜態程序分析的商業用途可以用來驗證安全關鍵電腦系統中的軟體，並指出可能有计算机安全隐患的程式碼，這類的應用越來越多。例如以下的產業已確定用靜態程序分析作為提昇複雜軟體品質的方法：.
查看 抽象释义和靜態程序分析
计算机逻辑
计算机逻辑描述应用于计算机科学和人工智能的逻辑。它包括：.
查看 抽象释义和计算机逻辑
Polyspace
Polyspace是靜態程序分析的工具，利用抽象释义的方式進行大規模的分析，可以偵測C語言、C++或是Ada程式的原始碼中，是否有特定類型的執行期錯誤，或是證明沒有這類的錯誤。此工具也可以檢查原始碼是否符合特定的代碼標準。.
指称语义
在计算机科学中，指称语义（Denotational semantics）是通过构造表达其语义的(叫做指称(denotation)或意义的)数学对象来形式化计算机系统的语义的一种方法。编程语言的形式语义的其他方法包括公理语义和操作语义。指称语义方式最初开发来处理一个单一计算机程序定义的系统。后来领域扩展到了由多于一个程序构成的系统，比如网络和并发系统。 指称语义起源于 克里斯托弗·斯特雷奇 和 Dana Scott 在1960年代的工作。在 Strachey 和 Scott 最初开发的时候，指称语义把计算机程序的指称(意义)解释为映射输入到输出的函数。后来证明对于允许包含递归定义的函数和数据结构，这样的元素的程序的指称(意义)定义太受限制了。为了解决这个困难，Scott 介入了基于域的指称语义的一般性方法。后来的研究者介入了基于幂域的方法，来解决并发系统的语义的问题。 粗略的说，指称语义关注找到代表程序所做所为的数学对象。这种对象的搜集叫做域。例如，程序(或程序段)可以被偏函数，或演员事件图想定，或用环境和系统之间的博弈表示: 它们都是域的一般性例子。 指称语义的一个重要原则是“语义应当是复合性的”: 程序段的指称应当建立自它的子段的指称。最简单的例子是: “3 + 4”的意义确定自“3”、“4”和“+”的意义。 指称语义最初被开发为把函数式和顺序式程序建模为映射输入到输出的数学函数的框架。本文第一节描述在这个框架内开发的指称语义。后续章节处理多态、并发等问题。.
查看 抽象释义和指称语义
海森堡bug
在程序设计术语中，海森堡bug（heisenbug）是指在尝试研究它时似乎会消失或者改变行为的bug（程序错误）。该词汇是物理学家维尔纳·海森堡名字的双关语，他最先断言了量子力学的观察者效应——观察系统的行为不可避免地将改变其状态。电子学中的传统用语则是，指连接一个到设备将改变其行为。 类似的词语有玻尔bug（bohrbug）、曼德博bug（mandelbug）和薛定谔bug（schrödinbug），它们偶尔被用于指代其他类型的非寻常软件缺陷，但通常以开玩笑的心态使用。.
查看 抽象释义和海森堡bug