“加入量子计算”

Ch1-2-ProgrammingLanguage.tex

@@ -1,7 +1,7 @@
 % !TEX root =  main.tex
-\section{引言}
+\section{概述}
-	
+%概念的界定，怎么展开	
-软件工程师在开发软件系统时，不可避免地要用到某种程序设计语言。顾名思义，程序设计语言\index{程序设计语言}是程序员用来描述程序行为的语言。一般来说，每种程序设计语言往往具有某种应用背景、所属的语言范式以及鲜明的特征。在计算机科学领域，曾出现过数百种程序设计语言。近几年，TIOBE、IEEE 等给出了目前常用的程序设计语言，排名居于前列的包括：Java、C、Python、C++、C\#、JavaScript、PHP等。Sebesta~\cite{sebesta2012concepts}从高级语言机制的设计角度对程序设计语言进行了深入细致的介绍和比较。大多数新程序设计语言的创建都受以前语言概念的启发，而新出现的程序设计语言使程序员的工作变得更加简单。
+软件工程师在开发软件系统时，不可避免地要用到某种程序设计语言。顾名思义，程序设计语言\index{程序设计语言}是程序员用来描述程序行为的语言。一般来说，每种程序设计语言往往具有某种应用背景、所属的语言范型以及鲜明的特征。程序理论作为程序设计语言的基础，不仅可以用于描述程序设计语言的语法、语义，还可以支撑程序的正确性构造。在计算机科学领域，曾出现过数百种程序设计语言。近几年，TIOBE、IEEE 等给出了目前常用的程序设计语言，排名居于前列的包括：Java、C、Python、C++、C\#、JavaScript、PHP等。Sebesta~\cite{sebesta2012concepts}从高级语言机制的设计角度对程序设计语言进行了深入细致的介绍和比较。大多数新程序设计语言的创建都受以前语言概念的启发，而新出现的程序设计语言往往通过规则的简化，使程序员的工作变得更加简单。
 
 %程序设计语言的定义可分为语法、语义等方面。语义表示程序的含义，由静态语义和动态语义组成。静态语义指程序编译时可以确定的语法成分的含义；建立在转换/迁移系统上的动态语义则描述程序如何执行。
 	
@@ -9,11 +9,11 @@
 
 在计算机发展的早期，人们往往是用二进制(0/1序列)给计算机发指令。这显然很不方便。后来，逐渐出现了汇编语言\index{汇编语言}以及各种高级语言。一般来说，提高软件开发本身的效率与质量需要更抽象更高级的程序设计语言；而提高现实计算机硬件系统的利用率和执行效率，则需要使用较低级的程序设计语言，这样程序可以更直接地控制硬件资源。较通用的程序设计语言适用于广泛的应用领域和应用场景，可吸引大量的语言使用者，积累充足的遗产代码，便于培训与推广共享资源；但高度通用的语言设计上难以兼顾开发效率与执行效率。很多针对特定应用领域的程序设计语言更容易通过合适的语言机制同时改善软件开发与执行的效率。多样化的编程接口具有程序设计语言功能，但缺乏相应的编程框架甚至程序库等。这类接口反映了相应的编程模型的特点，实质上起到了程序设计语言的作用。
 
-程序设计语言的发展因计算机系统发展的驱动和行业应用需求发展的推动。不同语言不同程度地受这些因素推动。但从程序设计语言发展历史角度看，应用需求的影响明显处于主导地位。新出现的程序设计语言通常是应对新兴应用或者新兴计算机体系结构的需要。
+程序设计语言的发展因计算机系统发展的驱动和行业应用需求发展的推动，不同语言不同程度地受这些因素推动。新出现的程序设计语言通常是应对新兴应用或者新兴计算机体系结构的需要。但从程序设计语言发展历史角度看，应用需求的影响明显处于主导地位。
 
 \subsection{语言的设计、实现及生命期}
 \subsubsection{设计}
-一般说来，程序语言的设计应该遵守以下原则\footnote{http://people.cs.aau.dk/~bt/DAT5E07/PrgLDesign.pdf}：
+一般说来，程序语言的设计应该遵守以下原则\footnote{http://people.cs.aau.dk/$\sim$bt/DAT5E07/PrgLDesign.pdf}：
 \begin{itemize}
 \item 可读性：能够很容易的理解；
 \item 可写性：能够清晰、准确地表达计算意图；
@@ -32,7 +32,7 @@
 
 \subsubsection{实现}
 
-语言的传统实现方式分为从高级语言\index{高级语言}到机器代码\index{机器代码}的静态编译与直接对高级语言程序解释执行\index{解释执行}两种方式。如果存在中间语言，在不同层次分别可能采用不同方式混合实现，如避免在运行时的编译性能消耗和内存消耗的运行前编译(Ahead of Time，简称为AOT)与根据当前硬件情况实时编译生成机器指令的运行时编译\index{运行时编译}(Just-in-time，简称为JIT)。编译技术仍然是语言实现的关键技术。一方面，类型检查等静态程序分析\index{静态程序分析}均在编译阶段实施；另一方面，代码生成过程中的优化技术是对程序员屏蔽硬件复杂性的主要手段。
+语言的传统实现方式分为从高级语言\index{高级语言}到机器代码\index{机器代码}的静态编译与直接对高级语言程序解释执行\index{解释执行}两种方式。如果存在中间语言，在不同层次可能分别采用不同方式混合实现，如避免在运行时的编译性能消耗和内存消耗的运行前编译(Ahead of Time，简称为AOT)与根据当前硬件情况实时编译生成机器指令的运行时编译\index{运行时编译}(Just-in-time，简称为JIT)。编译技术仍然是语言实现的关键技术。一方面，类型检查等静态程序分析\index{静态程序分析}均在编译阶段实施；另一方面，代码生成过程中的优化技术是对程序员屏蔽硬件复杂性的主要手段。
 
 近年来，随着计算机系统结构\index{计算机系统结构}的多样化和复杂化，程序设计语言出现了许多新的形式。例如，并行编程模型\index{并行编程模型}OpenMP使用预编译制导语句插在C或Fortran的代码中，描述了多线程并行。尽管OpenMP本身不具有完整的独立语法，但因为反映了与串行C语言不同的共享变量式并行编程模型，我们也可以称之为新的“语言”或者至少是新的“语言机制”。
 
@@ -42,7 +42,7 @@
 
 \begin{figure}[htbp]
 	\centering	
-	\includegraphics[width=0.80\textwidth]{fig1-2/2-1.png}
+	\includegraphics[width=0.95\textwidth]{fig1-2/2-1.png}
 	\caption{常见程序设计语言的发展脉络
 	\label{fig:2-1}}
 \end{figure}
@@ -53,10 +53,10 @@
 	\item 机器语言\index{机器语言}：由二进制0、1代码指令构成，不同的处理器具有不同的指令系统。由于机器语言难编写和维护，人们已很少直接使用这种语言。
 	\item 汇编语言\index{汇编语言}：汇编语言指令可以直接访问系统接口。由汇编程序翻译成的机器语言程序效率高。但同样难以使用与维护。
 	\item 高级语言：它是面向用户的，独立于计算机种类与结构。因此易学易用，通用性强，应用广泛。图\ref{fig:2-1}给出了常见高级程序设计语言的发展脉络\footnote{https://exploring-data.com/vis/programming-languages-influence-network/}，其中箭头指向的程序设计语言借鉴了前驱的设计思想。
-	\item 非过程化语言\index{非过程化语言}：使用这种语言编码时只需说明“做什么”，不需描述算法细节。数据库查询语言是其中的一种，用户可以对数据库中的信息进行复杂的操作。
+	\item 声明式语言\index{非过程化语言}：使用这种语言编码时只需说明“做什么”，不需描述算法细节。数据库查询语言是其中的一种，用户可以对数据库中的信息进行复杂的操作。
 \end{enumerate}
 
-在程序设计语言发展最初阶段，程序设计语言按照主要编程范式\index{编程范式}，可以被归类为过程式、面向对象、函数式~\cite{hu2015functional}等。随着C++、C\#等语言的出现，传统分类之间的界限逐渐变得模糊。现代的编程语言往往具有若干种类编程语言的元素，这就是所谓的多范式编程语言。而多范式程序设计语言\index{多范式程序设计语言}也是一个越来越明显的趋势。
+在程序设计语言发展最初阶段，程序设计语言按照主要编程范型\index{编程范型}，可以被归类为过程式、面向对象、函数式~\cite{hu2015functional}等。随着C++、C\#等语言的出现，传统分类之间的界限逐渐变得模糊。现代的编程语言往往具有若干种类编程语言的元素，这就是所谓的多范型编程语言。而多范型程序设计语言\index{多范型程序设计语言}也是一个越来越明显的趋势。
 
 一个成功的程序设计语言从探索到推广、接受和最终成为行业标准往往经历以下四个阶段：第一阶段，新兴应用与系统的软件开发在早期开发过程只能采用已有的程序设计语言配以一定的软件工程方法；第二阶段，为提高软件生产率，多种语言工具开始出现；第三阶段，行业标准的形成有助于积累遗产代码资源和培训与推广资源；第四阶段，随着大量遗产代码开始积累，行业商业模式成型，倾向于使用成熟的程序设计语言。分析程序设计语言所处的发展阶段有助于我们了解甚至预测其发展规律。
 
@@ -64,25 +64,26 @@
 
 \begin{figure}[htbp]
 	\centering	
-	\includegraphics[width=0.80\textwidth]{fig1-2/2-2.png}
+	\includegraphics[width=0.99\textwidth]{fig1-2/2-2.png}
 	\caption{程序设计语言的发展及分类}
 	\label{fig:2-2}
 \end{figure}
 
-这里以多个有代表性的语言为例，分析其应用背景、设计特点与发展规律，从而展现程序设计语言发展的历史与现状。按照程序设计语言的类型与应用，图\ref{fig:2-2}给出了以时间为主线的不同类别语言的发展过程与分类关系。从不同角度来看，一种程序设计语言既可能属于系统编程语言，又是面向对象语言。从发展过程来看，一种语言在发展过程中会不断进行扩充，融入不同的范式，进而趋近于多范式语言。本节主要以应用驱动来组织。计算机产业的发展往往是新的产业应用从已有的应用模式中成长出来而不是取而代之。新语言的出现往往标志着信息技术在新的应用领域的扩张。
+%这里以多个有代表性的语言为例，分析其应用背景、设计特点与发展规律，从而展现程序设计语言发展的历史与现状。
+按照程序设计语言的类型与应用，图\ref{fig:2-2}给出了以时间为主线的不同类别语言的发展过程与分类关系。从不同角度来看，一种程序设计语言既可能属于系统编程语言，又是面向对象语言。从发展过程来看，一种语言在发展过程中会不断进行扩充，融入不同的范型，进而趋近于多范型语言。计算机产业的发展往往是新的产业应用从已有的应用模式中成长出来而不是取而代之。新语言的出现往往标志着信息技术在新的应用领域的扩张。本节主要以应用驱动来组织。
 	
 \begin{itemize}
-	\item 科学与工程计算
+	\item 科学与工程计算(1954$\sim$)
 \end{itemize}	
 
 早期计算机系统硬件结构简单，软件专用性强，主要用于核反应计算、密码破译这样专业性强的科学与工程计算领域，直接服务对象往往是政府与军工。由John Backus主导实现的Fortran语言标志着具有完整工具链的程序设计语言出现。Fortran语言符合典型的过程式语言的特征，由从事系统结构和系统软件的研究人员设计，采取编译的方式实现，反映了程序设计与计算机系统之间的紧密联系。尽管串行的科学计算软件开发方法已成熟，积累的大量遗产代码保证了Fortran这样的语言在其适用领域仍然具有生命力。
 
-早期语言的准确语义往往依赖于编译器的实现，针对特定体系结构由编译器的开发者设计。1950年代末期出现了一些由计算机逻辑理论与程序语义研究者设计和实现的程序设计语言，如ALGOL和LISP语言。此后出现的大量函数式语言如Haskell、ML往往具有清楚而简洁的数学表示，设计出发点上更多地考虑如何优美地表示计算，但由于缺乏工业级应用的针对性以及性能上对常见体系结构的适配性，其接受范围受到限制。
+早期语言的准确语义往往依赖于编译器的实现，针对特定体系结构由编译器的开发者设计。上世纪五十年代末期出现了一些由计算机逻辑理论与程序语义研究者设计和实现的程序设计语言，如ALGOL和LISP语言。上世纪七十年代后出现的大量函数式语言如ML、Haskell往往具有清楚而简洁的数学表示，设计出发点上更多地考虑如何优美地表示计算，但由于缺乏工业级应用的针对性以及性能上对常见体系结构的适配性，其接受范围受到限制。
 
 科学与工程性质的计算，尤其是高性能计算往往与计算机体系结构密切相关，发展了多种形式的编程接口。OpenMP是共享内存的并行计算所常用的编程接口。其特点是在C或Fortran中插入指导语句，希望不改变原有串行程序语义的条件下利用共享存储器的多线程并行加速计算。MPI是跨平台的消息传递通讯程序库，完全不增加额外的语法机制。图形处理器语言CUDA在C基础上扩展了一些语法机制，用以区分在CPU、GPU上运行的程序片段，作出不同的编译。并行程序设计模型一直是程序设计理论研究的一个重点 。
 
 \begin{itemize}
-	\item 商用计算
+	\item 商用计算(1960$\sim$)
 \end{itemize}
 
 信息技术的应用逐渐从专业领域扩展到广阔的商业领域信息化。COBOL语言的出现标志着商业化的事务处理如金融、财会有了强有力的语言技术支持。该时期计算系统往往是大型机或小型机服务器。COBOL拥有庞大的用户群，据称积累了超过2000亿行遗产代码\footnote{http://cobolcowboys.com/cobol-today/}。由于商业计算的多样性，一台大型机往往需要运行多种类型的软件，甚至同时并发地运行不同软件。这一时期开始，管理不同类型软件的操作系统得以发展。C语言可以直接处理系统资源，尤其适合系统软件开发。相比之下，同样是过程式语言\index{过程式语言}的PASCAL语言则是由程序设计语言理论研究者设计的更加安全和规范的语言。数据库查询语言\index{数据库查询语言}SQL是较早出现的领域专用语言。它不具有完整的程序设计语言功能，但可看成是针对关系数据库\index{关系数据库}应用的编程模型。
@@ -90,25 +91,25 @@
 随着商用计算而来的是软件大规模化。1960年代末出现了一系列旨在有效控制大规模软件开发过程复杂性的程序设计思想。面向对象的思想及其第一个语言Simula 67试图对不同程序模块访问共享变量的方式进行限制，使得程序更加具有模块组装特性。Edsger W. Dijkstra提出避免使用GOTO语句的结构化程序设计\index{结构化程序设计}思想~\cite{dijkstra1968go}，对程序的控制流进行限制。
 
 \begin{itemize}
-	\item 人工智能
+	\item 人工智能(1960$\sim$)
 \end{itemize}
 
-\index{人工智能}自诞生以来，广受关注。在该领域也出现了若干专用语言。人工智能有符号主义、连接主义等流派。
+人工智能\index{人工智能}自诞生以来，广受关注。在该领域也出现了若干专用语言。例如，基于λ演算的函数式编程语言LISP，具有对符号表达式的支持、交互式环境和可扩展性等特性，曾大量用于人工智能系统的开发。人工智能有符号主义、连接主义等流派。
 
 符号主义就是以符号逻辑系统\index{符号逻辑系统}为基础来表示知识。二十世纪七十年代，Robert Kowalski 等人提出了逻辑可以作为程序设计语言的基本思想，把逻辑和计算这两个截然不同的概念统一在一起。这就是逻辑程序设计(Logic Programming)，而Prolog语言就是典型的逻辑程序设计语言。对经典的逻辑程序设计语言，可以进行各种扩充。例如，将状态转移的控制机制引入到时序逻辑系统的XYZ/E是世界上第一个可执行的时序逻辑程序设计语言~\cite{Tang2002}。
 
 连接主义的代表是试图模拟人脑的人工神经网络。近十年来，深度学习显示出了强大的学习能力和广泛的应用前景。TensorFlow、PyTorch等工具针对深度神经网络学习算法的特点，利用高级语言展开生成神经网络结构然后以高性能方式运行学习算法。这些多样的领域特定语言工具不具备完整的通用程序设计语言功能，但十分适合特定的应用场景。
 
 \begin{itemize}
-	\item 个人计算与系统编程
+	\item 个人计算与系统编程(1981$\sim$)
 \end{itemize}
 
 在摩尔定律背景下，计算机硬件系统的价格不断下降，个人使用计算机的情形越来越普遍。随个人计算而来的是软件的多样化，应用形式从事务处理和业务处理扩展到教育与娱乐。软件的开发与销售形式从硬件捆绑式发展到专业软件企业发行软件拷贝的销售形式。软件开发团队与人员的数目大量增加。C 语言是一种通用的、面向过程式的计算机程序设计语言。计算机系统设计以及应用程序编写是C语言应用的主要领域。 C++是C语言的面向对象扩展，又增加了泛型编程机制，更适合大中型程序的开发。
 
-作为一种新的多范式语言，Rust不仅能够提供友好的编译器和清晰的错误提示信息，而且速度快、内存利用率高，同时具有丰富的类型系统保证内存安全和线程安全。目前从初创公司到大型企业，已有很多公司都在使用 Rust，应用非常广泛。
+作为一种新的多范型语言，Rust不仅能够提供友好的编译器和清晰的错误提示信息，而且速度快、内存利用率高，同时具有丰富的类型系统保证内存安全和线程安全。目前从初创公司到大型企业，已有很多公司都在使用 Rust，应用非常广泛。
 
 \begin{itemize}
-	\item Web服务与移动计算
+	\item Web服务与移动计算(1990$\sim$)
 \end{itemize}
 
 伴随互联网的出现，Web服务软件一改拷贝销售形式，直接通过互联网向终端用户提供服务。其服务形式多样，方式多变。服务的反应速度往往受限于互联网的带宽与延迟，而不是计算的速度。因此，客户端与服务器端交互程序设计语言重点关注软件的开发效率，而不是程序的性能。典型的支持此类应用的脚本语言有JavaScript、PHP等。
@@ -116,7 +117,7 @@
 1990年代后智能手机的出现与普及将计算拓展到个人随身携带的新模式。一些为Web服务设计的语言仍然适用，但新的应用形式也带来了新的挑战。许多项目需要同时以网页、平板以及智能手机形式提供服务。由于应用需求与服务逻辑的易变性，软件的任何更新希望在不同平台上一致地更新。它们不仅需要支持复杂的功能，还需要解决跨平台、跨设备、跨操作系统兼容可移植的难题。
 
 \begin{itemize}
-	\item 大数据分析与处理
+	\item 大数据分析与处理(2004$\sim$)
 \end{itemize}
 
 平台系统的大规模数据分析与处理需求，首先来自于互联网的搜索服务。其特点是大量采集的数据需要多台服务器的集群通过并行计算高速处理。分布式并行计算带来了性能优化与可靠性的挑战。但是，在平台建设期无法预知随时可能出现的各种数据分析需求。应用开发人员需要随时针对应用需求快速、灵活地编程，而不必为系统级的性能与可靠性问题所困扰。
@@ -128,25 +129,28 @@
 %基本的Map与Reduce命令还不能涵盖一般的并行计算步骤的数据依赖关系。
 
 \begin{itemize}
-	\item 互联网金融
+	\item 互联网金融(2009$\sim$)
 \end{itemize}
 
 以软件为核心的互联网金融指的是以互联网为载体的金融服务形式，而并非仅仅将互联网作为连接客户的信息系统。开源软件技术主导的金融服务形式始于2009年出现的第一个数字货币--比特币。数字货币以去中心化共识的区块链记账技术为基础，提供类似法定货币的金融功能，具有特殊的金融服务属性。以太坊数字货币扩展了记账技术，支持区块链中记录完整的程序并以可验证的方式执行这样的程序：合同即是程序，程序即是合同。这就是所谓的智能合约(Smart Contract)。Solidity是目前最流行的合约编程语言。Solidity语法类似于JavaScript，支持继承、类和复杂的用户定义类型，通过编译的方式生成以太坊虚拟机中的代码。
 
-\vspace{10pt}
-\noindent{\bf{展望}}
 
 
-在计算机发展的不同阶段，为了应对一些典型应用，各种不同的程序设计语言应运而生。现阶段，多范式、函数式程序设计语言逐渐成为主流，如Java、C++及新出现的程序设计语言；第二，虽然如JavaScript、Python等语言强调动态类型安全（编译器能够对查询执行语法正确性检查），新出现的语言重新强调静态类型安全（不使用编译器不能保证安全的语言功能）；第三，新出现的语言语法更加简洁，并更加重视语言的可扩充性；同时，轻量级并发程序设计变得越来越普及。
-
 \section{程序理论}
-程序设计语言都具有语法和语义。语义表示程序的含义。程序理论涵盖程序设计语言的设计、实现，以及程序正确性的分析方法等。本节将介绍程序设计语言的语法与语义基础，并给出描述程序设计规范的形式化方法。其中，形式语言是用数学方法研究程序设计语言的语法，研究语言的组成规则。类型理论\index{类型理论}可以帮助完善程序设计本身，帮助运行系统检查程序中的语义错误。形式语义\index{形式语义}是\index{程序设计理论}的组成部分，以数学为工具，利用符号和公式，精确地定义和解释计算机程序设计语言的语义。而形式规约\index{形式规约}将事物的状态和行为用数学符号形式化描述，为编写计算机程序和验证程序的正确性提供依据。
+程序设计语言都具有语法和语义。语义表示程序的含义。程序理论涵盖程序设计语言的设计、实现，以及程序正确性的分析方法等。本节将介绍程序设计语言的语法与语义基础，并给出描述程序设计规范的形式化方法，如图\ref{fig:1-2-4}所示。其中，形式语言是用数学方法研究程序设计语言的语法，研究语言的组成规则。类型理论\index{类型理论}可以帮助完善程序设计本身，帮助运行系统检查程序中的语义错误。形式语义\index{形式语义}是程序设计理论\index{程序设计理论}的组成部分，以数学为工具，利用符号和公式，精确地定义和解释计算机程序设计语言的语义。而形式规约\index{形式规约}将事物的状态和行为用数学符号形式化描述，为编写计算机程序和验证程序的正确性提供依据。
+
+\begin{figure}[htbp]
+	\centering	
+	\includegraphics[width=0.99\textwidth]{fig1-2/2-4.png}
+	\caption{程序设计语言的发展及分类}
+	\label{fig:1-2-4}
+\end{figure}
 
 \subsection{程序设计语言的词法与语法}
-程序设计语言都有自己的词法和语法，而词法和语法的定义是一系列规则的集合，这些规则的基础就是形式语言。文法\index{文法}是形式语言中十分重要的基本概念，是描述语言的语法结构的一组形式规则。文法有四种分类，其中最常用的为正则语言\index{正则语言}和上下文无关语言\index{上下文无关语言}。正则语言可以用正规式定义，上下文无关语言可以用上下文无关文法(元素和规则的集合)定义。程序设计语言中的大多数算术表达式可用上下文无关文法\index{上下文无关文法}生成。正则语言是最简单的语言类，是上下文无关语言类的一个真子类。对程序设计语言编写的程序进行分析和处理(编译)时，需要判断对应的句子是否合法，可以通过对应语言的自动机进行判断。自动机是语言的另一种表示方法。其中，正则语言可以转换成有限状态自动机\index{有限状态自动机}、上下文无关语言可转换成下推自动机\index{下推自动机}表示，反之亦然。针对某种特定输入的一系列有限的规则，对不同的输入的元素，自动机依据自身的状态会做出不同的响应，最后达到某种特定的状态。
+程序设计语言都有自己的词法和语法，而词法和语法的定义是一系列规则的集合，这些规则的基础就是形式语言。文法\index{文法}是形式语言中十分重要的基本概念，是描述语言的语法结构的一组形式规则。文法有四种分类，其中最常用的为正则语言\index{正则语言}和上下文无关语言\index{上下文无关语言}。正则语言可以用正规式定义，上下文无关语言可以用上下文无关文法(元素和规则的集合)定义。程序设计语言中的大多数算术表达式可用上下文无关文法\index{上下文无关文法}生成。正则语言是最简单的语言类，是上下文无关语言类的一个真子类。对程序设计语言编写的程序进行分析和处理(编译)时，需要判断对应的句子是否合法，可以通过对应语言的自动机进行判断。自动机是语言的另一种表示方法。其中，正则语言可以转换成有限状态自动机\index{有限状态自动机}、上下文无关语言可转换成下推自动机\index{下推自动机}表示，反之亦然。针对某种特定输入的一系列有限的规则，对不同的输入元素，自动机依据自身的状态会做出不同的响应，最后达到某种特定的状态。
 
 \subsection{程序设计语言的类型系统}
-在很多程序设计语言中，变量与数据是带类型的；而类型之间有一定的关联。人们在研究程序设计语言理论时，可以借鉴类型论\index{类型论}(Type theory, 也称“类型理论”)来研究程序设计语言的类型系统\index{类型系统}。类型论是数理逻辑中的一个分支，其中的马丁洛夫类型理论用规则来刻画类型及行为，是程序构造的形式理论。类型理论\index{类型理论}研究的是程序设计语言的类型系统，用于定义如何将编程语言中的数值和表达式等短语归类为许多不同的类型，如何操作这些类型，这些类型如何互相作用。类型通过预测程序部件的某些执行行为来协调这些部件间的交互。在类型化的程序设计语言中，语言构造分为引入和消去两种形式。类型的引入形式确定该类型的值或范式，而消去形式则确定如何操作该类型的值以形成另一种（可能是相同的）类型的计算。例如，可以使用类型系统中的归纳类型定义如自然数、表、树等数据结构\index{数据结构}；使用多态类型处理程序的特定型与参数型这些不同的输入类型；使用记录类型定义一组记录的命名类型等；自然数类型的引入形式是自然数，消去形式是加法和乘法等。
+在很多程序设计语言中，变量与数据是带类型的；而类型之间有一定的关联。人们在研究程序设计语言理论时，可以借鉴类型论\index{类型论}(Type theory, 也称“类型理论”)来研究程序设计语言的类型系统\index{类型系统}。类型论是数理逻辑中的一个分支，其中的马丁洛夫类型理论用规则来刻画类型及行为，是程序构造的形式理论。类型理论\index{类型理论}研究的是程序设计语言的类型系统，用于定义如何将编程语言中的数值和表达式等短语归类为许多不同的类型，如何操作这些类型，这些类型如何互相作用。类型通过预测程序部件的某些执行行为来协调这些部件间的交互。在类型化的程序设计语言中，语言构造分为引入和消去两种形式。类型的引入形式确定该类型的值或范型，而消去形式则确定如何操作该类型的值以形成另一种（可能是相同的）类型的计算。例如，可以使用类型系统中的归纳类型定义如自然数、表、树等数据结构\index{数据结构}；使用多态类型处理程序的特定型与参数型这些不同的输入类型；使用记录类型定义一组记录的命名类型等；自然数类型的引入形式是自然数，消去形式是加法和乘法等。
 
 \subsection{程序的语义}
 给定一个程序，如何判断它是否正确？这是很早以前人们就关注的问题。简单来说，如果一个程序恰当地实现了设计者与用户的意图，它就是正确的。严格意义上，程序的正确性~\cite{turing1989checking}需要数学证明，不仅需要形式描述设计者与用户的意图，而且要形式描述程序的含义，并推导程序的行为满足设计者与用户的意图。程序含义的形式化描述就是形式语义学。基于形式语义，不仅可以构建描述程序含义的基础，还可以用于验证程序的正确性。
@@ -186,7 +190,7 @@
 %若条件语句if(y==1) then x=1; else x=2; 的前置断言为\{y==1\}，则该语句执行后，后置断言为\{x==1\}。
 在该形式系统中可以直接进行程序性质的规约和验证。程序逻辑的表达能力、可靠性、完备性以及可判定性都可归结为数理逻辑上的元性质，程序逻辑的解释模型通常就是程序设计语言的指称语义或操作语义。
 常见的公理语义有基于一阶逻辑\index{一阶逻辑}扩展的Floyd-Hoare 逻辑\index{Floyd-Hoare 逻辑}~\cite{Hoare1969}、谓词转换器(Predicate Transformer)等。其中，
-Floyd-Hoare 逻辑最初是面向串行程序\index{串行程序}的，并扩展至并发程序、实时系统\index{实时系统}、混成系统甚至量子系统\index{量子系统}等。针对指针程序\index{指针程序}和面向对象程序，产生了分离逻辑及其变种，从而把Floyd-Hoare 逻辑的应用推进到实际的程序验证\index{程序验证}。公理语义在形式验证中的应用是比较多的。
+Floyd-Hoare 逻辑最初是面向串行程序\index{串行程序}的，并扩展至并发程序、实时系统\index{实时系统}、混成系统甚至量子系统\index{量子系统}等。针对指针程序\index{指针程序}和面向对象程序，产生了分离逻辑及其变种，从而把Floyd-Hoare 逻辑的应用推进到实际的程序验证\index{程序验证}。公理语义在形式验证中应用比较多。
 
 \begin{itemize}
 	\item 代数语义
@@ -204,7 +208,7 @@ Floyd-Hoare 逻辑最初是面向串行程序\index{串行程序}的，并扩展
 
 
 
-\subsection{程序的规范}
+\subsection{程序的规约}
 %基于程序逻辑系统的性质规约刻画了所期望的系统行为，这些性质是通过逻辑公式来描述的。
 
 直接使用程序设计语言及其语义，难以描述和证明软件从需求文档到程序代码的开发过程各阶段创建的不同抽象层次的制品及其正确性。针对这一问题，人们开始研究高层抽象的形式规约语言的设计。形式规约语言\index{形式规约语言}是指由严格的递归语法规则所定义的语言，满足语法规则的句子称为合式或良构(Well-formed)规约。
@@ -219,7 +223,8 @@ Floyd-Hoare逻辑中，程序与断言是分离的，而且也无法表达活性
 %形式规约可以自顶向下逐步精化形成软件开发的规约序列，在足够的实现细节完成后，可以通过代码自动生成得到程序。以形式规约语言为基础的形式化开发方法，有VDM、Z、Event-B、RAISE、CafeOBJ、TLA、SOFL等。
 
 %20世纪七十年代后，
-\vspace{5pt}
+%\vspace{5pt}
+\subsection{程序设计理论框架}
 不同的形式语义有各自特点与适用范围。学者们试图在这些语义的基础上构建一个统一的理论。
 %软件工程界认识到数学可以为程序正确性保证提供技术基础。
 相应的出现了一些程序设计理论框架。例如，八十年代初，唐稚松提出以时序逻辑作为软件开发过程的统一基础，并着手建立XYZ系统\index{XYZ系统}~\cite{Tang2002}。Joseph A. Goguen 和Rod M. Burstall提出了一种抽象模型理论，以实现不同形式逻辑基础上的各种形式化方法的理论统一、技术和工具的集成与使用~\cite{Goguen92}。 C.A.R. Hoare和何积丰提出了统一程序设计理论框架UTP，提供了在一种程序(如串行程序)语义模型理论基础上构建扩展程序(如并发)的语义理论，从而保证原来的理论在扩展的理论中能够重用~\cite{hoare1998unifying}。
@@ -259,7 +264,7 @@ Floyd-Hoare逻辑中，程序与断言是分离的，而且也无法表达活性
 \end{itemize}
 
 %由Edmund M. Clarke、E. Allen Emerson和Joseph Sifakis提出的
-模型检验\index{模型检验}方法通过自动遍历系统模型的有穷状态空间，来检验系统的语义模型与其性质规约之间的满足关系。软件系统属于无穷状态系统，即使状态有穷，其状态空间规模通常远超当前计算机可处理的范围。在硬件系统模型检验取得巨大成功的时候，软件模型检验所面临严峻的挑战。对于无穷状态系统，符号化可达性分析可能不终止。软件模型检验的核心问题是如何建立可检验规模的软件模型(抽象)。一种方法是采用上近似(Over-approximation或下近似(Under-approximation)对模型进行抽象，另一种方法是使用限界模型检验，将模型空间爆炸涉及的参数(例如循环次数、并发数等)限制在一定范围内，验证系统模型在此深度内是否满足系统规约。在软件模型检验中，利用静态分析、符号执行\index{符号执行}等方法抽取程序模型，以及基于路径的模型检验等静态和动态结合的方法，也是有效提高模型检验扩展性的重要途径。近年来，将模型检验与定理证明有效地结合也是一个有前景的研究方向。
+模型检验\index{模型检验}方法通过自动遍历系统模型的有穷状态空间，来检验系统的语义模型与其性质规约之间的满足关系。软件系统属于无穷状态系统，即使状态有穷，其状态空间规模通常远超当前计算机可处理的范围。在硬件系统模型检验取得巨大成功的时候，软件模型检验所面临严峻的挑战。对于无穷状态系统，符号化可达性分析可能不终止。软件模型检验的核心问题是如何建立可检验规模的软件模型(抽象)。一种方法是采用上近似(Over-approximation或下近似(Under-approximation)对模型进行抽象，另一种方法是使用限界模型检验，将模型空间爆炸涉及的参数(例如循环次数、并发数等)限制在一定范围内，验证系统模型在此深度内是否满足系统规约。在软件模型检验中，利用静态分析、符号执行\index{符号执行}等方法抽取程序模型，以及基于路径的模型检验等静态和动态结合的方法，也是有效提高模型检验扩展性的重要途径。%近年来，将模型检验与定理证明有效地结合也是一个有前景的研究方向。
 
 \subsection{程序的自动综合}
 按照某种形式规约表达的用户意图，程序综合\index{程序综合}能够使用指定的编程语言自动生成符合规约的程序代码。程序综成器通常在程序空间上执行某种形式的搜索，以生成与各种类型一致的程序约束(例如输入输出示例，演示，自然语言，部分程序和断言)。程序综合是编程理论中最核心的问题之一~\cite{pnueli1989synthesis}。早期的想法是通过组合子问题生成带有证明的、可解释的实现。一个分支是使用定理证明器首先证明用户提供的规约，再使用这个证明提取相应的程序逻辑。而另一个较为流行的方法是从一个高层规约开始，不断的进行转换，直到实现目标程序。近期的程序综合方法中，用户提供规约的同时，还可以提供目标程序的语法。这样使得基于语法结构进行的综合过程更加高效，得到的程序的可解释性更高。
@@ -267,9 +272,11 @@ Floyd-Hoare逻辑中，程序与断言是分离的，而且也无法表达活性
 \subsection{程序的精化}
 程序精化\index{程序精化}是将抽象（高级）形式规范可验证地转换为具体（低级）可执行程序的过程，是通过逐步细化分阶段完成。精化（Refinement）是一种数学表示法和若干规则的集合，它对Dijkstra的卫式命令语言进行扩充，通过结合规约语句、精化规则和语言本身，从程序规约推导出命令式程序。程序精化(程序规约转换成可执行代码)可分为数据精化和算法精化两种，形式化将程序逐步转换为更加便于实现的形式：数据精化把抽象的数据结构转换为可以高效实现的形式；算法精化将程序逐步转换为更加便于实现的代码形式。
 
-\section{结束语}
+\section{本章小结}
-开发软件，离不开程序设计语言。本章简要介绍了程序设计语言的发展历史与现状，着重介绍了若干典型的程序设计语言。
+开发软件，离不开程序设计语言。
-本章还介绍了基本的程序理论，特别是几类形式语义。它们有助于清晰地表达程序的含义，保障程序的正确性。 正是由于在程序设计语言和相关理论领域的先驱工作，目前已经有20位左右的研究人员获得了“计算机界的诺贝尔奖”--图灵奖。
+在计算机发展的不同阶段，为了应对一些典型应用，各种不同的程序设计语言应运而生。
+第一，现阶段，多范型、函数式程序设计语言逐渐成为主流，如Java、C++及新出现的程序设计语言；第二，虽然如JavaScript、Python等语言强调动态类型安全（编译器能够对查询执行语法正确性检查），新出现的语言重新强调静态类型安全（不使用编译器不能保证安全的语言功能）；第三，新出现的语言语法更加简洁，并更加重视语言的可扩充性；同时，轻量级并发程序设计变得越来越普及。同时，为了适应软件的新形态，程序理论也取得了长足的进步。首先，随着新领域的涌现，出现了新的计算模型与语义，例如，描述量子程序设计的理论模型；其次，程序规约的形式随着需求的发展日益复杂；再次，待验证程序的类型表现出多元化特征，从简单的串行程序到并发、分布式；最后，可验证程序规模日益增加，从简单的驱动程序，到编译器，甚至是操作系统层次。
+正是由于在程序设计语言和相关理论领域的先驱工作，目前已经有23位研究人员获得了图灵奖。
 	
 %\section{参考文献}
 %	

Ch2-2-SoftwareTheory.tex

@@ -19,7 +19,7 @@
 
 
 \section{重大挑战问题}
-在新的时代背景下，特别是在人机物融合的大环境下，软件理论遇到了新的挑战。具体包括：如何应对大规模的数据与计算(§\ref{sec:st-complexity})；如何保证复杂软件系统的正确性、可靠性、安全性(§\ref{sec:st-reliability})；针对新型计算机的硬件架构与新的计算平台，如何建立其理论分析基础(§\ref{sec:st-architecture})。
+在新的时代背景下，特别是在人机物融合的大环境下，软件理论遇到了新的挑战。具体包括：如何应对大规模的数据与计算(§\ref{sec:st-complexity})；如何保证复杂软件系统的正确性、可靠性、安全性(§\ref{sec:st-reliability})；针对新型计算机的硬件架构与新的计算平台，如何建立其理论分析基础(§\ref{sec:st-architecture})；如何分析、编译新型计算模型下的程序并保证它的正确性(§\ref{sec:st-quantum})。
 
 
 \subsection{面向数据科学的算法与计算复杂性理论}\label{sec:st-complexity}
@@ -75,9 +75,16 @@
 
 最后，新型计算平台引发了分布式系统数据一致性分析的挑战。云计算平台中，为了提高系统的可用性，往往采用地理上分布的多拷贝数据，这也使得系统开发需要面对数据一致性、可用性和对网络分割的容忍性这三者不可兼得的经典问题（即所谓的CAP定理），需要在三者中做出取舍，取得合理折中。考虑到强数据一致性（串行一致性）的实现对效率影响较大，实际系统中往往根据业务特点来适当放松对一致性的保证，这样带来的结果是：一方面系统中可能多种一致性并存，另一方面应用级程序员在使用弱一致性数据的时候，难以保证程序业务的正确性。如何在编程语言和模型中既支持多种一致性，又能简化编程负担，并且对程序的可靠性和正确性给出指导原则和分析验证技术，是当前研究的热点。
 
+\subsection{新型计算模型下的计算复杂性理论与程序正确性保证}\label{sec:st-quantum}
+量子硬件设计与制造技术的飞速发展，人们乐观的预测多于一百个量子比特的特定用途的量子计算机有望在5-10 年内实现。量子计算拟充分利用量子力学的两大特性——量子叠加与量子纠缠——来获得潜在的比传统计算性能上的大幅度提升，从而有可能使用量子计算模型来解决经典计算模型中无法高效计算的问题，特别是一些经典困难问题，例如Shor提出的量子整数分解算法可以高效地求解大整数的质因数分解问题，Grover提出的量子搜索算法可以开平方根量级的加速无序数组的查找问题。
 
+量子软件与算法领域最核心的挑战问题仍然是：量子软件与算法能否比经典软件算法在效率上有本质的提升？如果可以提升，那在哪些问题上可以有提升？最多可以提升多大量级？即能否从数学上完全刻画出量子计算能够有效加速的范围及其加速的极限。这对于我们更加深刻的理解计算的本质，特别是计算困难性的起源有着重要的科学意义。同时它还有助于加深我们对于量子力学本质的认识，以及在宏观尺度下量子效应的展示。
+
+另一个重要的挑战是量子软件和程序该如何进行验证。虽然量子程序的分析与形式化验证领域已经取得了一些可喜的进展，但目前的研究还非常零散，很多问题甚至还不清楚如何准确定义。对于整数分解问题，因其属于NP复杂性类，其结果可以有效地经典验证，但是对一个超出经典计算能力的量子程序，如何才能验证其正确性？例如最近谷歌宣称的“量子优越性”实验。量子密码协议，特别是量子密钥分发协议从理论上具有比经典协议更好的安全性保障，但如何才能够使用经典的方式来验证所设计的量子密码协议的正确性？
+
+%第三个重要的挑战是如何进行量子的编译和电路优化。谷歌等公司已经能制造出53-70物理比特的量子芯片，量子计算的发展目前正在进入到含噪中尺度量子系统时代 (NISQ, Noisy Intermediate-Scale Quantum Computing)。目前的量子纠错方法或者纠错成本过高（需要约100：1的纠错比特开销），或者所需要的物理比特的质量要求过高（需要门正确率阈值超过3个9以上）。如何能够通过电路的优化和软件编译的优化使得在NISQ系统上真正运行一个有意义的量子软件和算法？
 \section{主要研究内容}
-软件理论的研究与软件应用的需求、承载软件的架构、平台息息相关。如图\ref{fig:2-2-1}所示，软件理论支撑了软件应用构建的整个过程；同时，软件应用构建过程中的问题推动了软件理论的深入研究。为了应对人机物融合环境下对软件理论的诸多挑战，需要开展多方面的研究工作。首先，为了支持有效的大数据处理，需要研究针对性的算法(§\ref{sec:stc-complexity})；其次，为了保证复杂系统的可靠性，需要围绕着规约、建模、分析与验证等环节，从系统特征、行为的描述与可靠性保证方法进行研究(§\ref{sec:stc-reliability})；其次，为了支持新的处理器结构与计算平台上的程序设计，需要构建相应的理论(§\ref{sec:stc-architecture})；最后，为了提高新型软件的可靠性，需要研究新型软件的特点，从而给出相应的分析方法(§\ref{sec:stc-newsoftware})。
+软件理论的研究与软件应用的需求、承载软件的架构、平台息息相关。如图\ref{fig:2-2-1}所示，软件理论支撑了软件应用构建的整个过程；同时，软件应用构建过程中的问题推动了软件理论的深入研究。为了应对人机物融合环境下对软件理论的诸多挑战，需要开展多方面的研究工作。首先，为了支持有效的大数据处理，需要研究针对性的算法(§\ref{sec:stc-complexity})；其次，为了保证复杂系统的可靠性，需要围绕着规约、建模、分析与验证等环节，从系统特征、行为的描述与可靠性保证方法进行研究(§\ref{sec:stc-reliability})；为了支持新的处理器结构与计算平台、新型计算模型上的程序设计，需要构建相应的理论(§\ref{sec:stc-architecture}, §\ref{sec:stc-quantum})；最后，为了提高新型软件的可靠性，需要研究新型软件的特点，从而给出相应的分析方法(§\ref{sec:stc-newsoftware})。
 \begin{figure}[htbp]
 	\centering	
 	\includegraphics[width=0.80\textwidth]{fig2-2/2-1.png}
@@ -93,94 +100,82 @@
 \subsection{形式化方法的理论研究}\label{sec:stc-reliability}
 一般来说，形式化方法的理论研究内容主要涉及规约、建模、分析与验证方法。其中，规约与建模是系统正确性、可靠性分析的基础，而分析与验证方法是保证系统正确性、可靠性的手段。
 
-\begin{itemize}
+%\begin{itemize}
-	\item 形式规约
+%	\item 形式规约
-\end{itemize}
+%\end{itemize}
 
 %形式规约可以分为基于模型的方法与基于代数的方法。基于模型的方法有VDM、Z、B、CSP等。基于代数的方法有Lotos、Larch、LTL等。
-为了验证不同的系统，研究人员对经典时序逻辑如LTL、CTL和CTL*等做了各种扩展上，包括博弈扩展、概率扩展、实时扩展、量子扩展等。
+形式规约的主要研究内容包括：对经典逻辑的各种扩展以及表达能力、相关判定问题复杂度的研究；面向不同领域规约的扩展以及相关判定算法；针对新的复杂系统特征的形式规约的扩展研究。
-这些扩展在模型检验的问题复杂度高，而且有的判定问题仍未解决。
+%为了验证不同的系统，研究人员对经典时序逻辑如LTL、CTL和CTL*等做了各种扩展上，包括博弈扩展、概率扩展、实时扩展、量子扩展等。
-%时序逻辑的概率扩展主要包括PCTL、PCTL*等。对于离散马尔可夫链模型，PCTL的模型检验问题可在多项式时间内完成，而LTL和PCTL*的模型检验问题仍是PSPACE-完全的。时序逻辑的实时扩展，包括MTL和TCTL。MTL的可满足性问题和针对时间自动机的模型检验问题在连续时间上是不可判定的，在离散时间上是EXPSPACE-完全的。时序逻辑的量子扩展主要包括QCTL、QCTL*等。QCTL在量子马尔可夫链上的验证可在多项式时间内完成；同样，该逻辑的可满足性的判定问题目前仍然没有解决。
+%这些扩展在模型检验的问题复杂度高，而且有的判定问题仍未解决。
-另外，时序逻辑的“超性质”是基于计算机安全背景的扩展，主要包括HyperLTL、HyperCTL*等。
+%%时序逻辑的概率扩展主要包括PCTL、PCTL*等。对于离散马尔可夫链模型，PCTL的模型检验问题可在多项式时间内完成，而LTL和PCTL*的模型检验问题仍是PSPACE-完全的。时序逻辑的实时扩展，包括MTL和TCTL。MTL的可满足性问题和针对时间自动机的模型检验问题在连续时间上是不可判定的，在离散时间上是EXPSPACE-完全的。时序逻辑的量子扩展主要包括QCTL、QCTL*等。QCTL在量子马尔可夫链上的验证可在多项式时间内完成；同样，该逻辑的可满足性的判定问题目前仍然没有解决。
-%HyperLTL的模型检验算法在最坏情况下是非初等可判定的，同时
+%另外，时序逻辑的“超性质”是基于计算机安全背景的扩展，主要包括HyperLTL、HyperCTL*等。
-这两种逻辑的可满足性问题也是非初等可判定的，但对于其某些特定片段却存在较为高效的算法。%除了基于时序逻辑形式规约的研究进展，还出现了%同步语言Quartz、描述动态自适应系统的RLEAX等系统规约。此外，
+%%HyperLTL的模型检验算法在最坏情况下是非初等可判定的，同时
-%基于本体论的网络本体语言(web ontology language)用于机器人、航天领域的形式规约描述系统需求。
+%这两种逻辑的可满足性问题也是非初等可判定的，但对于其某些特定片段却存在较为高效的算法。%除了基于时序逻辑形式规约的研究进展，还出现了%同步语言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，随机混成程序。
+
+
+%刻画无穷状态系统有随机、参数化等模型，除了使用相应的分析工具如INFANY、JKind等，还可以统一在进程重写系统(Process Rewrite System, PRS)中进行分析。
+%
+%最近，深度神经网络的健壮性分析是研究热点之一。神经网络的结构常被表示为一组在整数域或实数域上的线性算术方程组与激活函数对应的非线性方程组的集合。然而已有的线性优化算法或者SMT求解器不擅于直接求解非线性方程。比较普遍的方法是根据具体的非线性方程，对线性优化算法或SMT求解器进行扩展，以便验证神经网络的安全性，或找到对抗干扰实例。
+
+%\begin{itemize}
+%	\item 形式分析与验证方法
+%\end{itemize}
+%
+%
+%软件系统的分析与验证的核心问题与挑战是如何缓解大规模复杂系统验证过程中的状态空间爆炸问题，并提高分析的精度与效率。
+
+形式分析与验证方法主要包括符号执行、抽象解释、定理证明、模型检验等，从不同方法与角度提高分析验证系统的精度与规模。
 \begin{itemize}
-	\item 形式建模方法
+\item 基于符号执行的程序分析方法研究集中在增加可分析问题类型、提高可行性、可分析程序规模与算法效率这些方面。在可行性方面的研究基本都是在分析的精确性、可靠性、建模工作量以及可扩展性之间进行权衡和折中。提高可分析程序规模方面的研究包括设立特定的搜索策略、约束输入范围减少程序的路径空间、优化路径条件、或面向特征的高效编码等。面向新的分析需求，也有一些新的符号执行技术出现，其中比较有代表性的是概率符号执行技术。符号执行技术与其他技术之间的紧密融合，以提高分析的效果，也是目前新的发展趋势，包括与模型检验、抽象解释\index{抽象解释}、模糊测试\index{模糊测试}、随机测试\index{随机测试}等的一些技术结合，以提高程序的覆盖率或缺陷发现效率。
+
+\item 基于抽象解释的形式验证主要包括提高抽象精度与可行性方面的研究。提高抽象解释分析精度的方法包括结合符号化方法来提高分析精度，利用SMT求解器、插值等技术来计算程序语句迁移函数的最佳抽象；提高抽象域的非线性表达能力。提高抽象解释可行性方面的研究工作包括复杂数据结构如数组内容、数值与形态混合程序自动分析的支持；不同谱系目标程序如多线程程序、中断驱动型程序、概率程序的支持；活性性质如时序性质、终止性分析的支持。
+
+\item 基于演绎推理的定理证明研究可以分成两部分：交互式定理证明（Interactive Theorem proving）和自动推理（Automated Theorem proving）。%交互式定理证明最常用的两个证明辅助工具是Coq和Isabelle。Lean是一个最新的证明辅助工具，其中的一个设计重点是允许更有效的证明策略的实现，从而提高证明的自动化程度。
+自动定理证明的基础包括SMT（Satisfiability Modulo Theories）和归结(Resolution)。SMT的研究包括如何将已有的算法框架与理论求解有效结合，如何采用多种策略加速求解过程，如理论预处理，选择分支，理论推导，理论冲突分析和引理学习等。 基于定理证明的研究主要围绕如何支撑构造即正确的系统软件开发。
+
+\item 基于模型检验的形式验证研究包括使用抽象或符号化等方法减少验证过程中遍历的状态空间规模、计算混成系统的可达集等。在缓解状态空间爆炸的研究包括反例制导的抽象精化方法（Counter-Example Guided Abstraction Refinement，CEGAR）、基于插值（Interpolant）来对抽象谓词进行精化、有界模型检验（Bounded Model Checking，BMC）、如何对代码中各种数据结构如数组、位向量、堆等进一步提供编码机制，如何对给定深度内行为空间进行有效编码及剪枝等来提升可验证系统规模，并提高验证效率、如何通过多技术深度融合来进行代码验证、如何将抽象解释（Abstract Interpretation）与模型检验相结合、如何将插值技术与SMT结合等等。
+混成系统的可达集计算包括使用基于决策过程的Tarski代数方法、基于多面体（Polyhedral）的计算、通过惰性定理证明方法分析线性或非线性混成系统的限界可达性问题、采用基于网格或谓词抽象的连续动力学特性的离散化等技术。
+
+\item 面向复杂系统的统计模型检验研究内容包括功能与非功能规约的形式化表示、涵盖功能与非功能规约的统一模型、统计模型检测算法的改进、确认正确(Verified)的工具实现、不同领域的应用等。
+
+\item  面向复杂系统的运行时验证研究包括如何降低监测对系统的开销、如何实现对实时系统的监测、如何对新型软件如基于学习的系统的监测等。
 \end{itemize}
 
-形式建模方法用于精确地刻画计算机软硬件系统的行为。如何以数学的形式描述日益复杂的系统结构与行为，用于系统正确性分析，是形式建模研究的核心问题之一。在一些安全关键领域，为了描述和验证系统的安全性，既需要描述离散的机器指令，又需要描述系统所处环境的连续特性。通常，使用混成自动机刻画这类系统。然而，与状态机类似，混成自动机缺乏对结构的描述。因此，出现了很多辅助复杂系统模块化表示的方法。例如，支持混成行为的层次化规范的环境SHIFT、PTOLEMY，描述并发混成行为的I/O自动机、CHARON，描述混成行为的规范HCSP(Hybrid CSP)、描述基于逻辑与组合分析的混成Hoare逻辑HHL(Hybrid Hoare logic)等。工业界常使用Simulink/Stateflow环境实现复杂系统的建模，但它缺乏统一的形式语义。为了对复杂系统的建模，人们还提出了组合建模方法，如HMODEST，随机混成程序。
-
-
-刻画无穷状态系统有随机、参数化等模型，除了使用相应的分析工具如INFANY、JKind等，还可以统一在进程重写系统(Process Rewrite System, PRS)中进行分析。
-
-最近，深度神经网络的健壮性分析是研究热点之一。神经网络的结构常被表示为一组在整数域或实数域上的线性算术方程组与激活函数对应的非线性方程组的集合。然而已有的线性优化算法或者SMT求解器不擅于直接求解非线性方程。比较普遍的方法是根据具体的非线性方程，对线性优化算法或SMT求解器进行扩展，以便验证神经网络的安全性，或找到对抗干扰实例。
-
-\begin{itemize}
-	\item 形式分析与验证方法
-\end{itemize}
-
-
-软件系统的分析与验证的核心问题与挑战是如何缓解大规模复杂系统验证过程中的状态空间爆炸问题，并提高分析的精度与效率。形式分析与验证方法主要包括符号执行、抽象解释、定理证明、模型检验等，从不同方法与角度提高分析验证系统的精度与规模。
-
-1)基于符号执行的程序分析方法
-
-符号执行提供了一种系统性遍历程序路径空间的手段。目前的研究集中在增加可分析问题类型、提高可分析程序规模与算法效率这些方面。提高可伸缩性方面的研究包括设立特定的搜索策略、约束输入范围减少程序的路径空间、优化路径条件、或面向特征的高效编码提高可伸缩性。在可行性方面的研究基本都是在分析的精确性、可靠性、建模工作量以及可扩展性之间进行权衡和折中。面向新的分析需求，也有一些新的符号执行技术出现，其中比较有代表性的是概率符号执行技术。符号执行技术与其他技术之间的紧密融合，以提高分析的效果，也是目前新的发展趋势，包括与模型检验、抽象解释\index{抽象解释}、模糊测试\index{模糊测试}、随机测试\index{随机测试}等的一些技术结合，以提高程序的覆盖率或缺陷发现效率。
-
-2)基于抽象解释的形式验证方法
-
-抽象解释理论为程序分析的设计和构建提供了一个通用的框架，并从理论上保证了所构建的程序分析的终止性和可靠性。抽象解释的核心问题是提高抽象的精度。为提高抽象解释分析精度，可以结合符号化方法来提高分析精度，利用SMT求解器、插值等技术来计算程序语句迁移函数的最佳抽象；也可以提高抽象域的非线性表达能力。如何有效降低存储开销和提高计算效率，是提高抽象解释可扩展性需要考虑的主要问题。在提高抽象解释的可行性方面，研究工作包括复杂数据结构如数组内容、数值与形态混合程序自动分析的支持；不同谱系目标程序如多线程程序、中断驱动型程序、概率程序的支持；活性性质如时序性质、终止性分析的支持。
-
-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规范，以及表明该程序满足规范的证明。
-
-4)基于模型检验的形式验证方法
-
-模型检验方法的基础是状态空间的遍历。一方面，状态空间爆炸问题是大规模复杂系统模型检验方法的主要瓶颈。这方面的研究集中在怎样使用抽象或符号化等方法，减少验证过程中遍历的状态空间规模。另一方面，复杂系统中连续状态变化导致的系统可达集计算方法也相当复杂。该方面的研究主要集中在如何计算混成系统的可达集。
-
-在缓解状态空间爆炸的方法方面，反例制导的抽象精化方法（Counter-Example Guided Abstraction Refinement，CEGAR）是当前复杂系统模型检验的主要手段之一。同时，基于插值（Interpolant）来对抽象谓词进行精化、有界模型检验（Bounded Model Checking，BMC）也是主流的研究方向。目前相关方向的工作主要集中于如何对代码中各种数据结构如数组、位向量、堆等进一步提供编码机制，如何对给定深度内行为空间进行有效编码及剪枝等来提升可验证系统规模，并提高验证效率等。此外，通过多技术深度融合来进行代码验证是近年来的重要趋势之一。如将抽象解释（Abstract Interpretation）与模型检验相结合，将插值技术与SMT结合等等。其中最具有代表性的工作为CPAChecker工具。它基于若干技术的结合，通过统一接口集成多种求解器和技术来对软件系统进行验证，从而得到更好的性能和可伸缩性。
-
-混成系统的可达集计算是制约混成系统验证的主要问题。
-简单混成系统的验证可以通过时间自动机、多速率自动机等实现。基于决策过程的Tarski代数的方法可以计算特定线性混成系统的可达集计算。HYTECH模型检验工具是第一个实现线性混成系统的精确符号化可达性分析工具，用的是基于多面体（Polyhedral）计算的方法。而CHECKMATE、d/dt工具使用多面体方法计算线性混成系统可达集的上近似。除此以外，还可以通过惰性定理证明方法分析线性或非线性混成系统的限界可达性问题，混成系统的分析还可以采用基于网格或谓词抽象的连续动力学特性的离散化等技术。
-能够避免可达集计算的演绎推理方法，被越来越多的用于复杂混成系统的验证，其核心是用来描述与推理系统属性的规范逻辑的表达能力。例如，微分动态逻辑（Differential Dynamic Logic，DDL）可用于大部分混成系统的建模与自动化推理。
-
-5)面向复杂系统的统计模型检验方法
-
-为了避免穷举复杂系统状态而产生的空间爆炸问题，
-统计模型检验方法通过有限多次的执行对系统进行模拟，并使用假设检验来推断这些样本是否提供满足或违反规范的统计证据。虽然基于仿真的解决方案并不能保证正确的结果，但可以限制发生错误的概率。而且，基于模拟的方法比基于搜索的精确方法使用的计算资源要小得多。
-
-6)面向复杂系统的运行时验证方法
-
-与基于模型的系统静态验证方法不同，运行时验证方法在系统运行过程中监测系统的异常，避免系统出现难以恢复的故障。它的基本思想是将形式化描述的规范转换成监测器，插桩在实际的系统中，观测系统行为是否出现异常。目前，可监测的范围既可以是形式描述的规范，也可以是抽象出来的系统行为，不仅可以对传统的软件进行监测，也可以对基于学习的软件进行监测。为了降低监测行为对系统的开销，还出现了硬件形式的监测器，实现对实时系统的监测。
-
 
 \subsection{新型体系结构和计算平台下的程序理论}\label{sec:stc-architecture}
 为了应对新涌现的体系结构与计算平台，软件与程序理论主要研究运行于新体系架构程序的语义、可靠性保证等问题。
-
+研究内容包括：新型体系结构下支持编译优化、多线程程序设计、与虚拟机性能提升的内存模型的形式化定义；多处理器架构的并发程序可线性化问题、可线性化在有界与无界并发线程操作中的可判定性问题、大规模并行程序的验证等。
-
+%新型体系结构下内存模型的形式化定义是软件理论研究的领域之一。片上多核／众核处理器已成为计算机体系结构发展的主流。传统的顺序一致性（Sequential Consistency）模型虽然符合程序设计的直觉，但已不能满足编译优化、处理器性能提升等多方面的需要。目前主流的多核处理器如x86、ARM和Power等所实现的内存模型都放松了对一致性的要求，允许同一线程对不同地址的读写访问可以乱序执行。在程序设计语言层面，如C11/C++11、Java等，也直接定义了内存模型，支持基于共享内存的多线程程序设计，为编译优化、虚拟机性能提升等提供必要基础。但目前，处理器及程序设计语言层面的内存模型仍缺乏严格的形式化定义，使并发程序设计及验证变得更加困难。已有的语义有x86-TSO内存模型的操作语义、Power内存模型的公理语义。但如何严格刻画不同处理器、程序设计语言的内存模型，仍有待进一步研究。
-新型体系结构下内存模型的形式化定义是软件理论研究的领域之一。片上多核／众核处理器已成为计算机体系结构发展的主流。传统的顺序一致性（Sequential Consistency）模型虽然符合程序设计的直觉，但已不能满足编译优化、处理器性能提升等多方面的需要。目前主流的多核处理器如x86、ARM和Power等所实现的内存模型都放松了对一致性的要求，允许同一线程对不同地址的读写访问可以乱序执行。在程序设计语言层面，如C11/C++11、Java等，也直接定义了内存模型，支持基于共享内存的多线程程序设计，为编译优化、虚拟机性能提升等提供必要基础。但目前，处理器及程序设计语言层面的内存模型仍缺乏严格的形式化定义，使并发程序设计及验证变得更加困难。已有的语义有x86-TSO内存模型的操作语义、Power内存模型的公理语义。但如何严格刻画不同处理器、程序设计语言的内存模型，仍有待进一步研究。
+%
-
+%
-
+%多处理器架构的并发程序可线性化问题是新型体系架构下的另一个研究内容。可线性化是多处理器并发程序设计的一种正确性条件，沿袭了顺序式程序设计的惯性，但可能会由于顺序瓶颈（Sequential Bottleneck）制约并发软件的性能和可扩展性。近年来提出的准可线性化（Quasi-linearizability）及更一般的量化松弛框架允许放松可线性化标准所要求的严格顺序规约（如放松并发队列的FIFO顺序），以适应多核平台性能优化的灵活性。可线性化问题对有界多并发线程而言是可判定的，但对无界多并发线程而言已经是不可判定的。在理论方面，已证明准可线性化问题对有界多并发线程而言是不可判定的；一般而言，弱内存模型可线性化在无界多调用/返回操作的情况下是不可判定的，但在有界多调用/返回操作的情况下是可判定的，因此可以采用静态方法来验证限界条件下并发数据结构实现的弱内存模型可线性化问题。
-多处理器架构的并发程序可线性化问题是新型体系架构下的另一个研究内容。可线性化是多处理器并发程序设计的一种正确性条件，沿袭了顺序式程序设计的惯性，但可能会由于顺序瓶颈（Sequential Bottleneck）制约并发软件的性能和可扩展性。近年来提出的准可线性化（Quasi-linearizability）及更一般的量化松弛框架允许放松可线性化标准所要求的严格顺序规约（如放松并发队列的FIFO顺序），以适应多核平台性能优化的灵活性。可线性化问题对有界多并发线程而言是可判定的，但对无界多并发线程而言已经是不可判定的。在理论方面，已证明准可线性化问题对有界多并发线程而言是不可判定的；一般而言，弱内存模型可线性化在无界多调用/返回操作的情况下是不可判定的，但在有界多调用/返回操作的情况下是可判定的，因此可以采用静态方法来验证限界条件下并发数据结构实现的弱内存模型可线性化问题。
+%
-
+%
-
+%近年来，高性能计算机的峰值计算能力不断提高。但相关软件的发展还难以跟上。如何保证这类软件的可靠性，更是一个尚未解决的难题。目前，虽然有少量研究，但不能用于大规模并行程序的验证。
-近年来，高性能计算机的峰值计算能力不断提高。但相关软件的发展还难以跟上。如何保证这类软件的可靠性，更是一个尚未解决的难题。目前，虽然有少量研究，但不能用于大规模并行程序的验证。
+\subsection{新型计算模型下的算法复杂性理论与程序分析方法}\label{sec:stc-quantum}
-
+针对量子计算模型下的挑战性问题，具体研究内容如下：量子程序设计与验证、量子密码协议设计与验证、量子复杂性下界问题等。量子程序设计与验证的研究包括量子程序设计模型和基本指令集；适用于量子计算的程序逻辑；量子程序不变式生成问题；量子程序的模型检验问题；并行与分布式量子程序设计技术等。量子密码协议设计与验证的研究包括抗量子攻击的经典密码协议，量子随机数生成，量子密码协议验证，量子纠错与编码等。量子复杂性下界研究包括图灵机模型下量子与经典复杂性类的（神谕）区分；量子通信复杂性协议下界；量子判定树模型复杂性下界；量子计算的交互式验证等。
 
 \subsection{新型软件及应用的处理与分析方法}\label{sec:stc-newsoftware}
 对于近年来新出现的各种软件及应用，核心问题是在提高系统效率的同时，如何保证系统的可靠性。基于学习的系统是近期出现的主流新型软件之一。根据不同的系统需求，有不同的研究方法。
+主要研究内容包括如何使用梯度下降优化、模型与噪音的优化等方法快速攻击系统并产生对抗样本；如何使用对抗训练、防御蒸馏等方法有效防御对基于学习系统的攻击；如何以形式化分析为基础提供该类系统的可靠性、鲁棒性等保证，如对部分系统进行验证、将语义作为训练内容增加系统可解释性、根据网络结构特点构建输出的监测器。
 
-
+%一类研究围绕着如何攻击与防御人工智能系统。基于学习的模型极易受到噪音的影响，输入中的一点噪音就会改变输出结果。因此对抗样本是不可避免的。在实际系统中，对抗样本攻击的成功率非常高。如何快速地寻找对抗样本，进行攻击，是个重要的研究问题。它本质是一个优化问题，通常可以利用梯度下降优化的方法得到较好的解。目前较新的方法将模型与噪声都转变成优化目标项，而输出限制条件转换成损失函数，值域限制被转换成了平滑截断函数的变量，这样优化器可以通过直接优化目标函数，得到对抗样本。除了对抗样本的寻找，另一个方向是如何进行防御，如对抗训练、防御蒸馏等。有研究表明，即使在有防御蒸馏保护的前提下，仍可以通过转移学习生成有效的对抗样本。
-一类研究围绕着如何攻击与防御人工智能系统。基于学习的模型极易受到噪音的影响，输入中的一点噪音就会改变输出结果。因此对抗样本是不可避免的。在实际系统中，对抗样本攻击的成功率非常高。如何快速地寻找对抗样本，进行攻击，是个重要的研究问题。它本质是一个优化问题，通常可以利用梯度下降优化的方法得到较好的解。目前较新的方法将模型与噪声都转变成优化目标项，而输出限制条件转换成损失函数，值域限制被转换成了平滑截断函数的变量，这样优化器可以通过直接优化目标函数，得到对抗样本。除了对抗样本的寻找，另一个方向是如何进行防御，如对抗训练、防御蒸馏等。有研究表明，即使在有防御蒸馏保护的前提下，仍可以通过转移学习生成有效的对抗样本。
+%
-
+%
-
+%另一类研究以形式化分析为基础，提供该类系统的可靠性、鲁棒性等保证。基于神经网络的智能系统结构\index{智能系统结构}复杂，神经元结点数众多。如何验证这类系统的正确性、分析其可靠性，是一个挑战性的问题。基于抽象的方法大大提高了可处理的神经元个数。由于实际系统的输入具有不确定性，针对确定的神经网络结构判断系统对每个输入的鲁棒性难以推广，目前缺乏对实际系统可用的验证方法。一种可行的方法是对接近输出的中间层进行验证。或者，针对神经网络的可解释性问题，把语义作为训练内容，与现有的系统结合，增加网络的可解释性。另一种可行的方法是根据系统训练过程中网络结构特点，构建输出的监测器。在使用中若某个输入导致了异常的网络内部结构，则该输入可能未在训练集范围内，输出结果不一定可靠。
-另一类研究以形式化分析为基础，提供该类系统的可靠性、鲁棒性等保证。基于神经网络的智能系统结构\index{智能系统结构}复杂，神经元结点数众多。如何验证这类系统的正确性、分析其可靠性，是一个挑战性的问题。基于抽象的方法大大提高了可处理的神经元个数。由于实际系统的输入具有不确定性，针对确定的神经网络结构判断系统对每个输入的鲁棒性难以推广，目前缺乏对实际系统可用的验证方法。一种可行的方法是对接近输出的中间层进行验证。或者，针对神经网络的可解释性问题，把语义作为训练内容，与现有的系统结合，增加网络的可解释性。另一种可行的方法是根据系统训练过程中网络结构特点，构建输出的监测器。在使用中若某个输入导致了异常的网络内部结构，则该输入可能未在训练集范围内，输出结果不一定可靠。
 
 \section{本章小结}
 计算机软硬件的飞速发展以及不同领域需求的日益复杂，催生出各种实际问题，为软件的设计与开发带来巨大的机遇与挑战。作为软件学科基础的理论与方法也需要与时俱进；我们需要不断探索解决这些挑战性问题的新途径。软件理论依赖于各种数学手段；反过来，软件及理论的发展也可能给数学研究带来新的问题。