improvements w.r.t various comments

Ch1-2-ProgrammingLanguage.tex

@@ -1,7 +1,7 @@
 % !TEX root =  main_ios.tex
 \section{引言} 
 	
-软件工程师在开发软件系统时，不可避免地要用到某种程序设计语言。顾名思义，程序设计语言\index{程序设计语言}是程序员用来描述程序行为的语言。一般来说，每种程序设计语言往往具有某种应用背景、所属的语言范式以及鲜明的特征。在计算机科学领域，曾出现过数百种程序设计语言。TIOBE给出目前常用程序设计语言的流行度排序，从高到低有：Java、C、Python、C++、C\#、JavaScript、PHP等\footnote{https://exploring-data.com/vis/programming-languages-influence-network/}。Sebesta~\cite{sebesta2012concepts}从高级语言机制的设计角度对程序设计语言进行了深入细致的介绍和比较。大多数新程序设计语言的创建都受以前语言概念的启发。较旧的语言仍然是新语言的坚实基础，而新出现的程序设计语言使程序员的工作变得更加简单。
+软件工程师在开发软件系统时，不可避免地要用到某种程序设计语言。顾名思义，程序设计语言\index{程序设计语言}是程序员用来描述程序行为的语言。一般来说，每种程序设计语言往往具有某种应用背景、所属的语言范式以及鲜明的特征。在计算机科学领域，曾出现过数百种程序设计语言。近几年，TIOBE、IEEE 等给出了目前常用的程序设计语言，排名居于前列的包括：Java、C、Python、C++、C\#、JavaScript、PHP等。Sebesta~\cite{sebesta2012concepts}从高级语言机制的设计角度对程序设计语言进行了深入细致的介绍和比较。大多数新程序设计语言的创建都受以前语言概念的启发。较旧的语言仍然是新语言的坚实基础，而新出现的程序设计语言使程序员的工作变得更加简单。
 
 %程序设计语言的定义可分为语法、语义等方面。语义表示程序的含义，由静态语义和动态语义组成。静态语义指程序编译时可以确定的语法成分的含义；建立在转换/迁移系统上的动态语义则描述程序如何执行。
 	
@@ -61,7 +61,7 @@
 这里以多个有代表性的典型语言为例，分析其应用背景、设计特点与发展规律，从而展现程序语言发展的历史与现状。按照程序语言的类型与应用，图\ref{fig:2-2}给出了以时间为主线的不同类别语言的发展过程与分类关系。从不同角度来看，一种程序语言既可能属于系统编程语言，又是面向对象语言。从发展过程来看，一种语言在发展过程中会不断进行扩充，融入不同的范式，进而趋近于多范式语言。本节主要以应用驱动来组织。计算机产业的发展往往是新的产业应用从已有的应用模式中成长出来而不是取而代之。新语言的出现往往标志着信息技术在新的应用领域的扩张。
 	
 \begin{itemize}
-	\item 科学与工程计算(1954$\sim$) 
+	\item 科学与工程计算
 \end{itemize}	
 
 早期计算机系统硬件结构简单，软件专用性强，主要用于核反应计算、密码破译这样专业性强的科学与工程计算领域，直接服务对象往往是政府与军工。1956年发布的Fortran语言标志着具有完整工具链的程序设计语言出现。Fortran语言符合典型的过程式语言的特征，由从事系统结构和系统软件的研究人员设计，采取编译的方式实现，反映了程序设计与计算机系统之间的紧密联系。尽管串行的科学计算软件开发方法已成熟，积累的大量遗产代码保证了Fortran这样的语言在其适用领域仍然具有生命力。
@@ -71,7 +71,7 @@
 科学与工程性质的计算，尤其是高性能计算往往与计算机体系结构密切相关，发展了多种形式的编程接口。OpenMP是共享内存的并行计算所常用的编程接口。其特点是在C或Fortran中插入指导语句，希望不改变原有串行程序语义的条件下利用共享存储器的多线程并行加速计算。MPI是跨平台的消息传递通讯程序库，完全不增加额外的语法机制。图形处理器语言CUDA在C基础上扩展了一些语法机制，用以区分在CPU、GPU上运行的程序片段，作出不同的编译。并行程序设计模型一直是程序设计理论研究的一个重点 。
 
 \begin{itemize}
-	\item 商用计算(1960$\sim$) 
+	\item 商用计算
 \end{itemize}
 
 信息技术的应用逐渐从专业领域扩展到广阔的商业领域信息化。COBOL语言的出现标志着商业化的事务处理如金融、财会有了强有力的语言技术支持。该时期计算系统往往是大型机或小型机服务器。COBOL拥有庞大的用户群，据称积累了超过2000亿行遗产代码\footnote{http://cobolcowboys.com/cobol-today/}。由于商业计算的多样性，一台大型机往往需要运行多种类型的软件，甚至同时并发地运行不同软件。这一时期开始，管理不同类型软件的操作系统得以发展。C语言可以直接处理系统资源，尤其适合系统软件开发。相比之下，同样是过程式语言的PASCAL语言则是由程序设计语言理论研究者设计的更加安全和规范的语言。数据库查询语言SQL是较早出现的领域专用语言。它不具有完整的程序设计语言功能，但可看成是针对关系数据库应用的编程模型。
@@ -79,7 +79,7 @@
 随着商用计算而来的是软件大规模化。1960年代末出现了一系列旨在有效控制大规模软件开发过程复杂性的程序设计思想。面向对象的思想及其第一个语言Simula 67试图对不同程序模块访问共享变量的方式进行限制，使得程序更加具有模块组装特性。Dijkstra提出避免使用GOTO语句的结构化程序设计思想~\cite{dijkstra1968go}，对程序的控制流进行限制。
 
 \begin{itemize}
-	\item 人工智能(1960$\sim$) 
+	\item 人工智能
 \end{itemize}
 
 人工智能自诞生以来，广受关注。在该领域也出现了若干专用语言。人工智能有符号主义、连接主义等流派。
@@ -89,7 +89,7 @@
 连接主义的代表是试图模拟人脑的人工神经网络。近十年来，深度学习显示出了强大的学习能力和广泛的应用前景。TensorFlow、PyTorch等工具针对深度神经网络学习算法的特点，利用高级语言展开生成神经网络结构然后以高性能方式运行学习算法。这些多样的领域特定语言工具不具备完整的通用程序设计语言功能，但十分适合特定的应用场景。
 
 \begin{itemize}
-	\item 个人计算与系统编程(1981$\sim$) 
+	\item 个人计算与系统编程
 \end{itemize}
 
 在摩尔定律背景下，计算机硬件系统的价格不断下降，个人使用计算机的情形越来越普遍。随个人计算而来的是软件的多样化，应用形式从事务处理和业务处理扩展到教育与娱乐。软件的开发与销售形式从硬件捆绑式发展到专业软件企业发行软件拷贝的销售形式。软件开发团队与人员的数目大量增加。C++是C语言的面向对象扩展，逐渐成为实施传统软件工程的主流语言。
@@ -97,7 +97,7 @@
 作为一种新的多范式语言，Rust不仅能够提供友好的编译器和清晰的错误提示信息，而且速度快、内存利用率高，同时具有丰富的类型系统保证内存安全和线程安全。目前从初创公司到大型企业，已有很多公司都在使用 Rust，应用非常广泛。
 
 \begin{itemize}
-	\item Web服务与移动计算(1990$\sim$) 
+	\item Web服务与移动计算
 \end{itemize}
 
 伴随互联网的出现，Web服务软件一改拷贝销售形式，直接通过互联网向终端用户提供服务。其服务形式多样，方式多变。服务的反应速度往往受限于互联网的带宽与延迟，而不是计算的速度。因此，客户端与服务器端交互程序设计语言重点关注软件的开发效率，而不是程序的性能。典型的支持此类应用的脚本语言如JavaScript、PHP已然形成工业标准。
@@ -105,7 +105,7 @@
 1990年代后智能手机的出现与普及将计算拓展到个人随身携带的新模式。一些为Web服务设计的语言仍然适用，但新的应用形式也带来了新的挑战。许多项目需要同时以网页、平板以及智能手机形式提供服务。由于应用需求与服务逻辑的易变性，软件的任何更新希望在不同平台上一致地更新。针对这些挑战，出现了新的语言如HTML5。它们不仅需要支持复杂的功能，还需要解决跨平台、跨设备、跨操作系统兼容可移植的难题。
 
 \begin{itemize}
-	\item 大数据分析与处理(2004$\sim$) 
+	\item 大数据分析与处理
 \end{itemize}
 
 平台系统的大规模数据分析与处理需求，首先来自于互联网的搜索服务。其特点是大量采集的数据需要多台服务器的集群通过并行计算高速处理。分布式并行计算带来了性能优化与可靠性的挑战。但是，在平台建设期无法预知随时可能出现的各种数据分析需求。应用开发人员需要随时针对应用需求快速、灵活地编程，而不必为系统级的性能与可靠性问题所困扰。
@@ -117,12 +117,15 @@
 基本的Map与Reduce命令还不能涵盖一般的并行计算步骤的数据依赖关系。
 
 \begin{itemize}
-	\item 互联网金融(2009$\sim$) 
+	\item 互联网金融
 \end{itemize}
 
 以软件为核心的互联网金融指的是以互联网为载体的金融服务形式，而并非仅仅将互联网作为连接客户的信息系统。开源软件技术主导的金融服务形式始于2009年出现的第一个数字货币--比特币。数字货币以去中心化共识的区块链记账技术为基础，提供类似法定货币的金融功能，具有特殊的金融服务属性。以太坊数字货币扩展了记账技术，支持区块链中记录完整的程序并以可验证的方式执行这样的程序：合同即是程序，程序即是合同。这就是所谓的智能合约(smart contract)。Solidity是目前最流行的合约编程语言。Solidity语法类似于JavaScript，支持继承、类和复杂的用户定义类型，通过编译的方式生成以太坊虚拟机中的代码。
 
 \vspace{10pt}
+\noindent{\bf{展望}}
+
+
 在计算机发展的不同阶段，为了应对一些典型应用，各种不同的程序设计语言应运而生。现阶段，多范式、函数式程序设计语言逐渐成为主流，如Java、C++及新出现的程序设计语言；第二，虽然如JavaScript、Python等语言强调动态类型安全（编译器能够对查询执行语法正确性检查），新出现的语言重新强调静态类型安全（不使用编译器不能保证安全的语言功能）；第三，新出现的语言语法更加简洁，并更加重视语言的可扩充性；同时，轻量级并发程序设计变得越来越普及。
 
 \section{程序理论}

Ch2-2-SoftwareTheory.tex

@@ -96,29 +96,32 @@
 	\item 形式规约
 \end{itemize}
 
-形式规约可以分为基于模型的方法与基于代数的方法。基于模型的方法有VDM、Z、B、CSP等。基于代数的方法有Lotos、Larch、LTL等。近些年来，针对串行程序的形式规约语言的进展集中在分离逻辑方面。除了针对分离逻辑的研究工作，为了验证不同的系统，研究人员对经典时序逻辑如LTL、CTL和CTL*等做了各种扩展上，包括博弈扩展、概率扩展、实时扩展、量子扩展等。时序逻辑的概率扩展主要包括PCTL、PCTL*等。对于离散马尔可夫链模型，PCTL的模型检验问题可在多项式时间内完成，而LTL和PCTL*的模型检验问题仍是PSPACE-完全的。时序逻辑的实时扩展，包括MTL和TCTL。MTL的可满足性问题和针对时间自动机的模型检验问题在连续时间上是不可判定的，在离散时间上是EXPSPACE-完全的。时序逻辑的量子扩展主要包括QCTL、QCTL*等。QCTL在量子马尔可夫链上的验证可在多项式时间内完成；同样，该逻辑的可满足性的判定问题目前仍然没有解决。另外，时序逻辑的“超性质”是基于计算机安全背景的扩展，主要包括HyperLTL、HyperCTL*等。HyperLTL的模型检验算法在最坏情况下是非初等可判定的，同时这两种逻辑的可满足性问题也是非初等可判定的，但对于其某些特定片段却存在较为高效的算法。除了基于时序逻辑形式规约的研究进展，还出现了同步语言Quartz、描述动态自适应系统的RLEAX等描述系统规约。此外，基于本体论的网络本体语言(web ontology language)也用于描述机器人、航天领域的形式规约描述系统需求。从整体来看，新的、更为复杂的系统特征推动了多种形式规约的提出及扩展研究。
+%形式规约可以分为基于模型的方法与基于代数的方法。基于模型的方法有VDM、Z、B、CSP等。基于代数的方法有Lotos、Larch、LTL等。
+从整体来看，新的、更为复杂的系统特征推动了多种形式规约的提出及扩展研究。但是，形式规约的表达能力越强，模型检验问题的复杂度就越高，甚至变得不可判定。如何在可判定的情况下，增加形式规约的表达能力，提高判定算法的效率，是该项研究的核心问题。
+
+近些年来，针对串行程序的形式规约语言的进展集中在分离逻辑方面。除了针对分离逻辑的研究工作，为了验证不同的系统，研究人员对经典时序逻辑如LTL、CTL和CTL*等做了各种扩展上，包括博弈扩展、概率扩展、实时扩展、量子扩展等。时序逻辑的概率扩展主要包括PCTL、PCTL*等。对于离散马尔可夫链模型，PCTL的模型检验问题可在多项式时间内完成，而LTL和PCTL*的模型检验问题仍是PSPACE-完全的。时序逻辑的实时扩展，包括MTL和TCTL。MTL的可满足性问题和针对时间自动机的模型检验问题在连续时间上是不可判定的，在离散时间上是EXPSPACE-完全的。时序逻辑的量子扩展主要包括QCTL、QCTL*等。QCTL在量子马尔可夫链上的验证可在多项式时间内完成；同样，该逻辑的可满足性的判定问题目前仍然没有解决。另外，时序逻辑的“超性质”是基于计算机安全背景的扩展，主要包括HyperLTL、HyperCTL*等。HyperLTL的模型检验算法在最坏情况下是非初等可判定的，同时这两种逻辑的可满足性问题也是非初等可判定的，但对于其某些特定片段却存在较为高效的算法。除了基于时序逻辑形式规约的研究进展，还出现了%同步语言Quartz、描述动态自适应系统的RLEAX等系统规约。此外，
+基于本体论的网络本体语言(web ontology language)用于机器人、航天领域的形式规约描述系统需求。
 \begin{itemize}
 	\item 形式建模方法
 \end{itemize}
 
-形式建模方法用于精确地刻画计算机软硬件系统的行为。在一些安全关键领域，为了描述和验证系统的安全性，既需要描述离散的机器指令，又需要描述系统所处环境的连续特性。通常，使用混成自动机进行刻画。然而，与状态机类似，混成自动机缺乏对结构的描述。因此，出现了很多辅助复杂系统模块化表示的方法。例如，支持混成行为的层次化规范的环境SHIFT、PTOLEMY，描述并发混成行为的I/O自动机、CHARON，描述混成行为的规范HCSP(hybrid CSP)、描述基于逻辑与组合分析的混成Hoare逻辑HHL(hybrid Hoare logic)等。工业界常使用Simulink/Stateflow环境实现复杂系统的建模，但它缺乏统一的形式语义。为了对复杂系统的建模，人们还提出了组合建模方法，如HMODEST，随机混成程序。
+形式建模方法用于精确地刻画计算机软硬件系统的行为。如何以数学的形式描述日益复杂的系统结构与行为，用于系统正确性分析，是形式建模研究的核心问题之一。在一些安全关键领域，为了描述和验证系统的安全性，既需要描述离散的机器指令，又需要描述系统所处环境的连续特性。通常，使用混成自动机进行刻画。然而，与状态机类似，混成自动机缺乏对结构的描述。因此，出现了很多辅助复杂系统模块化表示的方法。例如，支持混成行为的层次化规范的环境SHIFT、PTOLEMY，描述并发混成行为的I/O自动机、CHARON，描述混成行为的规范HCSP(hybrid CSP)、描述基于逻辑与组合分析的混成Hoare逻辑HHL(hybrid Hoare logic)等。工业界常使用Simulink/Stateflow环境实现复杂系统的建模，但它缺乏统一的形式语义。为了对复杂系统的建模，人们还提出了组合建模方法，如HMODEST，随机混成程序。
 
 
 刻画无穷状态系统有随机、参数化等模型，除了使用相应的分析工具如INFANY、JKind等，还可以统一在进程重写系统(Process Rewrite System, PRS)中进行分析。
 
-
-最近，深度神经网络的健壮性分析是研究热点之一。神经网络的结构常被表示为一组在整数域或实数域上的线性算术方程组与激活函数对应的非线性方程组的集合。然而已有的线性优化算法或者SMT求解器不擅于直接求解非线性方程。比较普遍的方法是根据具体的非线性方程，对线性优化算法或SMT求解器进行扩展，验证神经网络的安全性，或找到对抗干扰实例。
+最近，深度神经网络的健壮性分析是研究热点之一。神经网络的结构常被表示为一组在整数域或实数域上的线性算术方程组与激活函数对应的非线性方程组的集合。然而已有的线性优化算法或者SMT求解器不擅于直接求解非线性方程。比较普遍的方法是根据具体的非线性方程，对线性优化算法或SMT求解器进行扩展，以便验证神经网络的安全性，或找到对抗干扰实例。
 
 \begin{itemize}
 	\item 形式分析与验证方法
 \end{itemize}
 
 
-软件系统的分析与验证的核心问题与挑战是如何应对系统的复杂性，缓解状态空间爆炸问题，并提高分析的精度与效率。形式分析与验证方法主要包括符号执行、抽象解释、定理证明、模型检验等，从不同方法与角度提高分析验证系统的精度与规模。
+软件系统的分析与验证的核心问题与挑战是如何缓解大规模复杂系统验证过程中的状态空间爆炸问题，并提高分析的精度与效率。形式分析与验证方法主要包括符号执行、抽象解释、定理证明、模型检验等，从不同方法与角度提高分析验证系统的精度与规模。
 
 1)基于符号执行的程序分析方法
 
-符号执行提供了一种系统性遍历程序路径空间的手段。提高可伸缩性方面的研究包括设立特定的搜索策略、约束输入范围减少程序的路径空间、优化路径条件、或面向特征的高效编码提高可伸缩性。在可行性方面的研究基本都是在分析的精确性、可靠性、建模工作量以及可扩展性之间进行权衡和折中。面向新的分析需求，也有一些新的符号执行技术出现，其中比较有代表性的是概率符号执行技术。符号执行技术与其他技术之间的紧密融合，以提高分析的效果，也是目前新的发展趋势，包括与模型检验、抽象解释、模糊测试、随机测试等的一些技术结合，以提高程序的覆盖率或缺陷发现效率。
+符号执行提供了一种系统性遍历程序路径空间的手段。目前的研究集中在增加可分析问题类型、提高可分析程序规模与算法效率这些方面。提高可伸缩性方面的研究包括设立特定的搜索策略、约束输入范围减少程序的路径空间、优化路径条件、或面向特征的高效编码提高可伸缩性。在可行性方面的研究基本都是在分析的精确性、可靠性、建模工作量以及可扩展性之间进行权衡和折中。面向新的分析需求，也有一些新的符号执行技术出现，其中比较有代表性的是概率符号执行技术。符号执行技术与其他技术之间的紧密融合，以提高分析的效果，也是目前新的发展趋势，包括与模型检验、抽象解释、模糊测试、随机测试等的一些技术结合，以提高程序的覆盖率或缺陷发现效率。
 
 2)基于抽象解释的形式验证方法
 
@@ -126,10 +129,11 @@
 
 3)基于演绎推理的定理证明方法
 
-定理证明的基本思想是将程序满足其形式规约的证明问题转化为一组数学命题的证明。为了提高证明的效率，推广定理证明的应用，定理证明方面的研究可以分成两部分：交互式定理证明（Interactive Theorem Proving）和自动推理（Automated Theorem Proving）。交互式定理证明最常用的两个证明辅助工具是Coq和Isabelle。Lean是一个最新的证明辅助工具，其中的一个设计重点是允许更有效的证明策略的实现。自动定理证明的基础包括SMT（Satisfiability Modulo Theories）和归结(Resolution)。SMT的研究对象是各种领域知识的逻辑组合，经常表达为带等词的一阶逻辑公式。惰性算法是目前主流的SMT求解方法，采用了被称为DPLL（T）的算法框架。为了DPLL求解与理论求解更为有效地结合，理论判定过程一般要设计为增量式的（Incremental）和可回溯的（Backtrackable）。主流SMT求解器还采用多种策略加速求解过程，如理论预处理，选择分支，理论推导，理论冲突分析和引理学习等。此外，基于定理证明的方法也可以支撑构造即正确的系统软件开发，如具有分层规范与公式推导特征的DeepSEA程序能够生成由CompCert编译的C程序、低层的Coq规范，以及表明该程序满足规范的证明。
+定理证明的基本思想是将程序满足其形式规约的证明问题转化为一组数学命题的证明。为了提高证明的效率、增加自动化证明程度、推广定理证明的应用，定理证明方面的研究可以分成两部分：交互式定理证明（Interactive Theorem Proving）和自动推理（Automated Theorem Proving）。交互式定理证明最常用的两个证明辅助工具是Coq和Isabelle。Lean是一个最新的证明辅助工具，其中的一个设计重点是允许更有效的证明策略的实现，从而提高证明的自动化程度。自动定理证明的基础包括SMT（Satisfiability Modulo Theories）和归结(Resolution)。SMT的研究对象是各种领域知识的逻辑组合，经常表达为带等词的一阶逻辑公式。惰性算法是目前主流的SMT求解方法，采用了被称为DPLL（T）的算法框架。为了DPLL求解与理论求解更为有效地结合，理论判定过程一般要设计为增量式的（Incremental）和可回溯的（Backtrackable）。主流SMT求解器还采用多种策略加速求解过程，如理论预处理，选择分支，理论推导，理论冲突分析和引理学习等。此外，基于定理证明的方法也可以支撑构造即正确的系统软件开发，如具有分层规范与公式推导特征的DeepSEA程序能够生成由CompCert编译的C程序、低层的Coq规范，以及表明该程序满足规范的证明。
 
 4)基于模型检验的形式验证方法
 
+模型检验方法的基础是状态空间的遍历。一方面，状态空间爆炸问题是大规模复杂系统模型检验方法的主要瓶颈。另一方面，复杂系统中连续状态变化导致的系统可达集计算方法也相当复杂。
 反例制导的抽象精化方法（Counter-Example Guided Abstraction Refinement，CEGAR）是当前复杂系统模型检验的主要手段之一。同时，基于插值（Interpolant）来对抽象谓词进行精化、有界模型检验（Bounded Model Checking，BMC）也是主流的研究方向。目前相关方向的工作主要集中于如何对代码中各种数据结构如数组、位向量、堆等进一步提供编码机制，如何对给定深度内行为空间进行有效编码及剪枝等来提升可验证系统规模，并提高验证效率等。此外，通过多技术深度融合来进行代码验证是近年来的重要趋势之一。如将抽象解释（Abstract Interpretation）与模型检验相结合，将插值技术与SMT结合等等。其中最具有代表性的工作为CPAChecker工具。它基于若干技术的结合，通过统一接口集成多种求解器和技术来对软件系统进行验证，从而得到更好的性能和可伸缩性。
 
 
@@ -139,12 +143,11 @@
 能够避免可达集计算的演绎推理方法，被越来越多的用于复杂混成系统的验证，其核心是用来描述与推理系统属性的规范逻辑的表达能力。例如，Platzer等人提出的Differential (algebraic) dynamic logic可用于大部分混成系统的建模与自动化推理。
 
 5)面向复杂系统的统计模型检验方法
-
+为了避免穷举复杂系统状态而产生的空间爆炸问题，
 统计模型检验方法通过有限多次的执行对系统进行模拟，并使用假设检验来推断这些样本是否提供满足或违反规范的统计证据。虽然基于仿真的解决方案并不能保证正确的结果，但可以限制发生错误的概率。而且，基于模拟的方法比基于搜索的精确方法使用的计算资源要小得多。
 
 6)面向复杂系统的运行时验证方法
-
-由于可以在系统运行时检测系统是否满足规范或出现异常，运行时验证技术使用的更为广泛。它的基本思想是将形式化描述的规范转换成监测器，插桩在实际的系统中，观测系统行为是否出现异常。目前，可监测的范围既可以是形式描述的规范，也可以是抽象出来的系统行为，不仅可以对传统的软件进行监测，也可以对基于学习的软件进行监测。为了降低监测行为对系统的开销，还出现了硬件形式的监测器，实现对实时系统的监测。
+与基于模型的系统静态验证方法不同，运行时验证方法在系统运行过程中监测系统的异常，避免系统出现故障。它的基本思想是将形式化描述的规范转换成监测器，插桩在实际的系统中，观测系统行为是否出现异常。目前，可监测的范围既可以是形式描述的规范，也可以是抽象出来的系统行为，不仅可以对传统的软件进行监测，也可以对基于学习的软件进行监测。为了降低监测行为对系统的开销，还出现了硬件形式的监测器，实现对实时系统的监测。
 
 
 \subsection{新型体系结构和计算平台下的程序理论}