capital letters to low, and Turing awards

2019-10-18 11:10:38 +08:00 · 2019-10-18 11:10:38 +08:00 · fc9cda8808
parent e19543664a
commit fc9cda8808
4 changed files with 11 additions and 74 deletions
--- a/.DS_Store
+++ b/.DS_Store
--- a/Ch1-2-ProgrammingLanguage.tex
+++ b/Ch1-2-ProgrammingLanguage.tex
@ -76,7 +76,7 @@

 信息技术的应用逐渐从专业领域扩展到广阔的商业领域信息化。COBOL语言的出现标志着商业化的事务处理如金融、财会有了强有力的语言技术支持。该时期计算系统往往是大型机或小型机服务器。COBOL拥有庞大的用户群，据称积累了超过2000亿行遗产代码\footnote{http://cobolcowboys.com/cobol-today/}。由于商业计算的多样性，一台大型机往往需要运行多种类型的软件，甚至同时并发地运行不同软件。这一时期开始，管理不同类型软件的操作系统得以发展。C语言可以直接处理系统资源，尤其适合系统软件开发。相比之下，同样是过程式语言的PASCAL语言则是由程序设计语言理论研究者设计的更加安全和规范的语言。数据库查询语言SQL是较早出现的领域专用语言。它不具有完整的程序设计语言功能，但可看成是针对关系数据库应用的编程模型。

-随着商用计算而来的是软件大规模化。1960年代末出现了一系列旨在有效控制大规模软件开发过程复杂性的程序设计思想。面向对象的思想及其第一个语言Simula 67试图对不同程序模块访问共享变量的方式进行限制，使得程序更加具有模块组装特性。Dijkstra提出避免使用GOTO语句的结构化程序设计思想~\cite{dijkstra1968go}，对程序的控制流进行限制。
+随着商用计算而来的是软件大规模化。1960年代末出现了一系列旨在有效控制大规模软件开发过程复杂性的程序设计思想。面向对象的思想及其第一个语言Simula 67试图对不同程序模块访问共享变量的方式进行限制，使得程序更加具有模块组装特性。Edsger W. Dijkstra提出避免使用GOTO语句的结构化程序设计思想~\cite{dijkstra1968go}，对程序的控制流进行限制。

 \begin{itemize}
 	\item 人工智能
@ -210,7 +210,7 @@ Floyd-Hoare逻辑中，程序与断言是分离的，而且也无法表达活性
 \vspace{5pt}
 不同的形式语义有各自特点与适用范围。学者们试图在这些语义的基础上构建一个统一的理论。
 %软件工程界认识到数学可以为程序正确性保证提供技术基础。
-相应的出现了一些程序设计理论框架。例如，八十年代初，唐稚松提出以时序逻辑作为软件开发过程的统一基础，并着手建立XYZ系统~\cite{Tang2002}。Goguen 和Burstall提出了一种抽象模型理论，以实现不同形式逻辑基础上的各种形式化方法的理论统一、技术和工具的集成与使用~\cite{Goguen92}。Hoare和何积丰提出了统一程序设计理论框架UTP，提供了在一种程序(如串行程序)语义模型理论基础上构建扩展程序(如并发)的语义理论，从而保证原来的理论在扩展的理论中能够重用~\cite{hoare1998unifying}。
+相应的出现了一些程序设计理论框架。例如，八十年代初，唐稚松提出以时序逻辑作为软件开发过程的统一基础，并着手建立XYZ系统~\cite{Tang2002}。Joseph A. Goguen 和Rod M. Burstall提出了一种抽象模型理论，以实现不同形式逻辑基础上的各种形式化方法的理论统一、技术和工具的集成与使用~\cite{Goguen92}。 C.A.R. Hoare和何积丰提出了统一程序设计理论框架UTP，提供了在一种程序(如串行程序)语义模型理论基础上构建扩展程序(如并发)的语义理论，从而保证原来的理论在扩展的理论中能够重用~\cite{hoare1998unifying}。

 \section{程序正确性构造}
 基于形式语义，我们可以确保程序的正确性，有两类方法，一类是先编写程序，再{\bf{验证}}它的正确性  ；另一种是编写构造即正确（correctness-by-construction）的程序，包括程序{\bf{综合}}与{\bf{精化}}，%程序的正确性分析存在不同的方法
@ -246,7 +246,8 @@ Floyd-Hoare逻辑中，程序与断言是分离的，而且也无法表达活性
 	\item 软件模型检验
 \end{itemize}

-由Edmund M. Clarke、E. Allen Emerson和Joseph Sifakis提出的模型检验\index{模型检验}方法通过自动遍历系统模型的有穷状态空间，来检验系统的语义模型与其性质规约之间的满足关系。软件系统属于无穷状态系统，即使状态有穷，其状态空间规模通常远超当前计算机可处理的范围。在硬件系统模型检验取得巨大成功的时候，软件模型检验所面临严俊的挑战。对于无穷状态系统，符号化可达性分析可能不终止。软件模型检验的核心问题是如何建立可检验规模的软件模型(抽象)。一种方法是采用上近似(over-approximation或下近似(under-approximation)对模型进行抽象，另一种方法是使用限界模型检验，将模型空间爆炸涉及的参数(例如循环次数、并发数等)限制在一定范围内，验证系统模型在此深度内是否满足系统规约。在软件模型检验中，利用静态分析、符号执行等方法抽取程序模型，以及基于路径的模型检验等静态和动态结合的方法，也是有效提高模型检验扩展性的重要途径。近年来，将模型检验与定理证明有效地结合也是一个有前景的研究方向。
+%由Edmund M. Clarke、E. Allen Emerson和Joseph Sifakis提出的
+模型检验\index{模型检验}方法通过自动遍历系统模型的有穷状态空间，来检验系统的语义模型与其性质规约之间的满足关系。软件系统属于无穷状态系统，即使状态有穷，其状态空间规模通常远超当前计算机可处理的范围。在硬件系统模型检验取得巨大成功的时候，软件模型检验所面临严俊的挑战。对于无穷状态系统，符号化可达性分析可能不终止。软件模型检验的核心问题是如何建立可检验规模的软件模型(抽象)。一种方法是采用上近似(over-approximation或下近似(under-approximation)对模型进行抽象，另一种方法是使用限界模型检验，将模型空间爆炸涉及的参数(例如循环次数、并发数等)限制在一定范围内，验证系统模型在此深度内是否满足系统规约。在软件模型检验中，利用静态分析、符号执行等方法抽取程序模型，以及基于路径的模型检验等静态和动态结合的方法，也是有效提高模型检验扩展性的重要途径。近年来，将模型检验与定理证明有效地结合也是一个有前景的研究方向。

 \subsection{程序的自动综合}
 按照某种形式规约表达的用户意图，程序综合\index{程序综合}能够使用指定的编程语言自动生成符合规约的程序代码。程序综成器通常在程序空间上执行某种形式的搜索，以生成与各种类型一致的程序约束(例如输入输出示例，演示，自然语言，部分程序和断言)。程序综合是编程理论中最核心的问题之一~\cite{pnueli1989synthesis}。早期的想法是通过组合子问题生成带有证明的、可解释的实现。一个分支是使用定理证明器首先证明用户提供的规约，再使用这个证明提取相应的程序逻辑。而另一个较为流行的方法是从一个高层规约开始，不断的进行转换，直到实现目标程序。近期的程序综合方法中，用户提供规约的同时，还可以提供目标程序的语法。这样使得基于语法结构进行的综合过程更加高效，得到的程序的可解释性更高。
@ -256,7 +257,7 @@ Floyd-Hoare逻辑中，程序与断言是分离的，而且也无法表达活性

 \section{小结}
 开发软件，离不开程序设计语言。本章简要介绍了程序设计语言的发展历史与现状，着重介绍了若干典型的程序设计语言。
-本章还介绍了基本的程序理论，特别是几类形式语义。它们有助于清晰地表达程序的含义，保障程序的正确性。  
+本章还介绍了基本的程序理论，特别是几类形式语义。它们有助于清晰地表达程序的含义，保障程序的正确性。 正是由于在程序设计语言和相关理论领域的先驱工作，目前已经有20位左右的研究人员获得了“计算机界的诺贝尔奖”--图灵奖。
 	
 %\section{参考文献}  
 %	
--- a/Ch2-2-SoftwareTheory.tex
+++ b/Ch2-2-SoftwareTheory.tex
@ -45,7 +45,7 @@
 首先，如何准确表示复杂系统的规约。系统的规约一般通过逻辑公式、集合论等来描述对系统安全性、可靠性、正确性等各方面的需求。系统规约要解决的主要问题是，将各种非形式化表述中使用的关键概念和性质，采用简洁直观又容易被用来推理验证的数学和逻辑语言进行描述。


-随着系统复杂性的增加和系统应用场景的多样化，使得需要描述的性质变得更加复杂。例如，信息物理系统除了关心功能正确性，还关心非功能相关的性质，包括实时、空间位置等时空特性；机器学习算法和系统的正确性和安全性的研究目前仍处于起步阶段，即便非形式的定义和刻画这些性质仍然是开放性问题，其中一些已经被大家所接受的重要性质，如鲁棒性（Robustness），其性质刻画与经典的程序功能正确性刻画显著不同。在并发系统中，除了线性一致性（linearizability）这种经典的对并发对象的功能正确性的刻画以外，人们还提出了各种新型的量化松弛算法，它们部分放松了线性一致性的要求，但仍然能够提供一定的正确性保证。这些放松后的保证该如何进行形式化的刻画，是目前面临的关键挑战。与之类似，为了解决云计算中分布式多拷贝数据的一致性问题，并在一致性、可用性、以及系统性能方面取得平衡，人们提出了各种不同强度的数据一致性，包括最终一致性、因果一致性、顺序一致性以及各种变体，还包括多种数据一致性相结合的算法和系统，这些不同的一致性的形式化规约是当前研究的热点问题。在信息安全领域，很多安全特性不是描述程序一次运行的性质，而是要刻画程序多次运行之间的关系，如信息流安全中经典的非干扰性（non-Interference），这一类性质往往被称为“超安全性质”（hyper-properties），其规约也和经典的功能正确性有所不同。
+随着系统复杂性的增加和系统应用场景的多样化，使得需要描述的性质变得更加复杂。例如，信息物理系统除了关心功能正确性，还关心非功能相关的性质，包括实时、空间位置等时空特性；机器学习算法和系统的正确性和安全性的研究目前仍处于起步阶段，即便非形式的定义和刻画这些性质仍然是开放性问题，其中一些已经被大家所接受的重要性质，如鲁棒性（Robustness），其性质刻画与经典的程序功能正确性刻画显著不同。在并发系统中，除了线性一致性（linearizability）这种经典的对并发对象的功能正确性的刻画以外，人们还提出了各种新型的量化松弛算法，它们部分放松了线性一致性的要求，但仍然能够提供一定的正确性保证。这些放松后的保证该如何进行形式化的刻画，是目前面临的关键挑战。与之类似，为了解决云计算中分布式多拷贝数据的一致性问题，并在一致性、可用性、以及系统性能方面取得平衡，人们提出了各种不同强度的数据一致性，包括最终一致性、因果一致性、顺序一致性以及各种变体，还包括多种数据一致性相结合的算法和系统，这些不同的一致性的形式化规约是当前研究的热点问题。在信息安全领域，很多安全特性不是描述程序一次运行的性质，而是要刻画程序多次运行之间的关系，如信息流安全中经典的非干扰性（non-interference），这一类性质往往被称为“超安全性质”（hyper-properties），其规约也和经典的功能正确性有所不同。


 其次，如何形式化表示复杂软件系统。安全攸关领域的很多系统往往可看成是信息物理系统在复杂环境中的运行，不仅兼有离散事件与连续的状态变化，同时计算与控制过程共存。由于系统的非确定性，或克服复杂性而进行的简化，很多都具有概率与随机行为。例如，由于风对飞行器运动的影响，网络控制的系统中消息的丢失及其他随机事件。因此，对随机混成系统的建模、分析与验证是非常困难的。为了实现随机混成系统的分析，可以通过添加概率或随机性对混成自动机进行扩展。然后对随机混成系统的验证转化成通过概率模型检验或统计模型检验进行可达性分析。但是，现有的基于随机混成系统的可达性分析方法仍存在很多不足。
@ -129,17 +129,17 @@

 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工具。它基于若干技术的结合，通过统一接口集成多种求解器和技术来对软件系统进行验证，从而得到更好的性能和可伸缩性。
+在缓解状态空间爆炸的方法方面，反例制导的抽象精化方法（Counter-Example Guided Abstraction Refinement，CEGAR）是当前复杂系统模型检验的主要手段之一。同时，基于插值（interpolant）来对抽象谓词进行精化、有界模型检验（Bounded Model Checking，BMC）也是主流的研究方向。目前相关方向的工作主要集中于如何对代码中各种数据结构如数组、位向量、堆等进一步提供编码机制，如何对给定深度内行为空间进行有效编码及剪枝等来提升可验证系统规模，并提高验证效率等。此外，通过多技术深度融合来进行代码验证是近年来的重要趋势之一。如将抽象解释（abstract interpretation）与模型检验相结合，将插值技术与SMT结合等等。其中最具有代表性的工作为CPAChecker工具。它基于若干技术的结合，通过统一接口集成多种求解器和技术来对软件系统进行验证，从而得到更好的性能和可伸缩性。

 混成系统的可达集计算是制约混成系统验证的主要问题。
 简单混成系统的验证可以通过时间自动机、多速率自动机等实现。基于决策过程的Tarski代数的方法可以计算特定线性混成系统的可达集计算。HYTECH模型检验工具是第一个实现线性混成系统的精确符号化可达性分析工具，用的是基于多面体（polyhedral）计算的方法。而CHECKMATE、d/dt工具使用多面体方法计算线性混成系统可达集的上近似。除此以外，还可以通过惰性定理证明方法分析线性或非线性混成系统的限界可达性问题，混成系统的分析还可以采用基于网格或谓词抽象的连续动力学特性的离散化等技术。
-能够避免可达集计算的演绎推理方法，被越来越多的用于复杂混成系统的验证，其核心是用来描述与推理系统属性的规范逻辑的表达能力。例如，Platzer等人提出的Differential (algebraic) dynamic logic可用于大部分混成系统的建模与自动化推理。
+能够避免可达集计算的演绎推理方法，被越来越多的用于复杂混成系统的验证，其核心是用来描述与推理系统属性的规范逻辑的表达能力。例如，Platzer等人提出的differential (algebraic) dynamic logic可用于大部分混成系统的建模与自动化推理。

 5)面向复杂系统的统计模型检验方法
 为了避免穷举复杂系统状态而产生的空间爆炸问题，
@ -156,7 +156,7 @@
 新型体系结构下内存模型的形式化定义是软件理论研究的领域之一。片上多核／众核处理器已成为计算机体系结构发展的主流。传统的顺序一致性（sequential consistency）模型虽然符合程序设计的直觉，但已不能满足编译优化、处理器性能提升等多方面的需要。目前主流的多核处理器如x86、ARM和Power等所实现的内存模型都放松了对一致性的要求，允许同一线程对不同地址的读写访问可以乱序执行。在程序设计语言层面，如C11/C++11、Java等，也直接定义了内存模型，支持基于共享内存的多线程程序设计，为编译优化、虚拟机性能提升等提供必要基础。但目前，处理器及程序设计语言层面的内存模型仍缺乏严格的形式化定义，使并发程序设计及验证变得更加困难。已有的语义有x86-TSO内存模型的操作语义、Power内存模型的公理语义。但如何严格刻画不同处理器、程序设计语言的内存模型，仍有待进一步研究。


-多处理器架构的并发程序可线性化问题是新型体系架构下的另一个研究内容。可线性化是多处理器并发程序设计的一种正确性条件，沿袭了顺序式程序设计的惯性，但可能会由于顺序瓶颈（Sequential bottleneck）制约并发软件的性能和可扩展性。近年来提出的准可线性化（Quasi-Linearizability）及更一般的量化松弛框架允许放松可线性化标准所要求的严格顺序规约（如放松并发队列的FIFO顺序），以适应多核平台性能优化的灵活性。可线性化问题对有界多并发线程而言是可判定的，但对无界多并发线程而言已经是不可判定的。在理论方面，已证明准可线性化问题对有界多并发线程而言是不可判定的；一般而言，弱内存模型可线性化在无界多调用/返回操作的情况下是不可判定的，但在有界多调用/返回操作的情况下是可判定的，因此可以采用静态方法来验证限界条件下并发数据结构实现的弱内存模型可线性化问题。
+多处理器架构的并发程序可线性化问题是新型体系架构下的另一个研究内容。可线性化是多处理器并发程序设计的一种正确性条件，沿袭了顺序式程序设计的惯性，但可能会由于顺序瓶颈（sequential bottleneck）制约并发软件的性能和可扩展性。近年来提出的准可线性化（quasi-linearizability）及更一般的量化松弛框架允许放松可线性化标准所要求的严格顺序规约（如放松并发队列的FIFO顺序），以适应多核平台性能优化的灵活性。可线性化问题对有界多并发线程而言是可判定的，但对无界多并发线程而言已经是不可判定的。在理论方面，已证明准可线性化问题对有界多并发线程而言是不可判定的；一般而言，弱内存模型可线性化在无界多调用/返回操作的情况下是不可判定的，但在有界多调用/返回操作的情况下是可判定的，因此可以采用静态方法来验证限界条件下并发数据结构实现的弱内存模型可线性化问题。


 近年来，高性能计算机的峰值计算能力不断提高。但相关软件的发展还难以跟上。如何保证这类软件的可靠性，更是一个尚未解决的难题。目前，虽然有少量研究，但不能用于大规模并行程序的验证。
--- a/references.bib
+++ b/references.bib
@ -1,66 +1,3 @@
-@inproceedings{Liskov:1974:PAD:800233.807045,
- author = {Liskov, Barbara and Zilles, Stephen},
- title = {Programming with Abstract Data Types},
- booktitle = {Proceedings of the ACM SIGPLAN Symposium on Very High Level Languages},
- year = {1974},
- location = {Santa Monica, California, USA},
- pages = {50--59},
- numpages = {10},
- url = {http://doi.acm.org/10.1145/800233.807045},
- doi = {10.1145/800233.807045},
- acmid = {807045},
- publisher = {ACM},
- address = {New York, NY, USA},
-} 
-
-@article{Floyd:1979:PP:359138.359140,
- author = {Floyd, Robert W.},
- title = {The Paradigms of Programming},
- journal = {Commun. ACM},
- issue_date = {Aug. 1979},
- volume = {22},
- number = {8},
- month = aug,
- year = {1979},
- issn = {0001-0782},
- pages = {455--460},
- numpages = {6},
- url = {http://doi.acm.org/10.1145/359138.359140},
- doi = {10.1145/359138.359140},
- acmid = {359140},
- publisher = {ACM},
- address = {New York, NY, USA},
-} 
-
-@article{Humphrey:2002:SUP:513126.513132,
- author = {Humphrey, Watts S.},
- title = {Software Unbundling: A Personal Perspective},
- journal = {IEEE Ann. Hist. Comput.},
- issue_date = {January 2002},
- volume = {24},
- number = {1},
- month = jan,
- year = {2002},
- issn = {1058-6180},
- pages = {59--63},
- numpages = {5},
- url = {http://dx.doi.org/10.1109/85.988582},
- doi = {10.1109/85.988582},
- acmid = {513132},
- publisher = {IEEE Educational Activities Department},
- address = {Piscataway, NJ, USA},
-} 
-
-
-@book{Simon:1996:SA:237774,
- author = {Simon, Herbert A.},
- title = {The Sciences of the Artificial (3rd Ed.)},
- year = {1996},
- isbn = {0-262-69191-4},
- publisher = {MIT Press},
- address = {Cambridge, MA, USA},
-} 
-
@article{Huang2018,
  title     = {Safety and Trustworthiness of Deep Neural Networks: {A} Survey},
  author = {Xiaowei Huang and Daniel Kroening and Wenjie Ruan and James Sharp and Youcheng Sun and Emese Thamo and Min Wu and Xinping Yi},
@ -122,7 +59,7 @@

@article{dijkstra1968go,
  title={Go to statement considered harmful},
-  author={Dijkstra, Edsger W},
+  author={Dijkstra, Edsger W.},
  journal={Communications of the ACM},
  volume={11},
  number={3},
@ -240,4 +177,3 @@
  year={1989},
  organization={ACM}
 }
-