根据梅老师批注做的一些小修改
This commit is contained in:
Xiaoxing Ma
parent
54a3dcf47c
commit
1c66ffa577
|
|
@ -147,7 +147,7 @@
|
|||
\begin{enumerate}
|
||||
\item 从存储程序式电子计算机出现到实用高级程序设计语言出现之前为第一阶段（上世纪40年代末到50年代中期）。此阶段计算机处理能力有限，应用领域主要集中于科学计算与工程计算。编制程序所用的工具是低级语言。系统软件仅能提供程序载入等简单功能。程序开发无系统方法，强调编程技巧。
|
||||
%
|
||||
\item 从实用高级程序设计语言出现到软件工程提出之前为第二阶段（上世纪50年代中期到60年代后期）。此阶段计算机处理能力迅速提高；应用领域扩展到商业数据处理等领域。人们开发了操作系统以充分利用系统资源。为了适应大量数据处理问题的需要, 数据库及其管理系统开始出现。FORTRAN、COBOL、ALGOL等高级语言，大大提高了程序设计的效率；但软件的复杂程度迅速提高，研制周期变长， 质量难以保证，出现了所谓软件危机。为此，人们提出结构化程序设计方法，并开始了程序正确性和软件可靠性的理论研究。
|
||||
\item 从实用高级程序设计语言出现到软件工程提出之前为第二阶段（上世纪50年代中期到60年代后期）。此阶段计算机处理能力迅速提高；应用领域扩展到商业数据处理等领域。人们开发了操作系统以充分利用系统资源。为了适应大量数据处理问题的需要, 数据库及其管理系统开始出现。FORTRAN、COBOL、ALGOL等高级语言大大提高了程序设计的效率；但软件的复杂程度迅速提高，研制周期变长， 质量难以保证，出现了所谓软件危机。为此，人们提出结构化程序设计方法，并开始了程序正确性和软件可靠性的理论研究。
|
||||
%
|
||||
\item 从软件工程提出到基于互联网的软件服务广泛使用之前为第三阶段（上世纪60年代后期到90年代后期）。
|
||||
计算机系统的处理能力继续增长，向嵌入式和局域网或基于广域网的企业计算延伸；应用领域扩展到社会生产生活的诸多方面。
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
% !TEX root = main.tex
|
||||
\section{概述}
|
||||
%概念的界定，怎么展开
|
||||
软件工程师在开发软件系统时，不可避免地要用到某种程序设计语言。顾名思义，程序设计语言\index{程序设计语言}是程序员用来描述程序的语言，为程序员表达基于计算的解决方案提供了（通用）抽象设施。一般来说，每种程序设计语言往往具有某种应用背景、所属的语言范式以及各自的个性特征。程序理论作为程序设计语言的基础，提供程序抽象及其之间的推理和构造原理，不仅可以用于描述程序设计语言的语法、语义，还可以支撑程序的正确性构造、指导程序的高效正确的实现。在计算机科学领域，曾出现过数百种程序设计语言。近几年，TIOBE\footnote{https://www.tiobe.com/tiobe-index/}、IEEE\footnote{https://spectrum.ieee.org/computing/software/the-top-programming-languages-2019} 等给出了目前常用的程序设计语言，排名居于前列的包括：Java~\cite{arnold2000java}、C~\cite{kernighan2006c}、Python~\cite{van2011python}、C++~\cite{stroustrup2000c++}、C\#~\cite{hejlsberg2006c}、JavaScript~\cite{crockford2008javascript}、PHP~\cite{lerdorf2002programming}等。大多数程序设计语言的创建都受其之前语言概念的启发，而新出现的程序设计语言提供更强更为自然的抽象设施，使程序员的工作变得更加简单、有效。Sebesta~\cite{sebesta2012concepts}从高级语言机制的设计角度对程序设计语言进行了深入细致的介绍和比较。
|
||||
软件工程师在开发软件系统时，不可避免地要用到某种程序设计语言。顾名思义，程序设计语言\index{程序设计语言}是程序员用来描述程序的语言，为程序员表达基于计算的解决方案提供了（通用）抽象设施。一般来说，每种程序设计语言往往具有某种应用背景、所属的语言范式\todo{前面脚注区分软件范型和语言范式}以及各自的个性特征。程序理论作为程序设计语言的基础，提供程序抽象及其之间的推理和构造原理，不仅可以用于描述程序设计语言的语法、语义，还可以支撑程序的正确性构造、指导程序的高效正确的实现。在计算机科学领域，曾出现过数百种程序设计语言。近几年，TIOBE\footnote{https://www.tiobe.com/tiobe-index/}、IEEE\footnote{https://spectrum.ieee.org/computing/software/the-top-programming-languages-2019} 等给出了目前常用的程序设计语言，排名居于前列的包括：Java~\cite{arnold2000java}、C~\cite{kernighan2006c}、Python~\cite{van2011python}、C++~\cite{stroustrup2000c++}、C\#~\cite{hejlsberg2006c}、JavaScript~\cite{crockford2008javascript}、PHP~\cite{lerdorf2002programming}等。大多数程序设计语言的创建都受其之前语言概念的启发，而新出现的程序设计语言提供更强更为自然的抽象设施，使程序员的工作变得更加简单、有效。Sebesta~\cite{sebesta2012concepts}从高级语言机制的设计角度对程序设计语言进行了深入细致的介绍和比较。
|
||||
|
||||
%程序设计语言的定义可分为语法、语义等方面。语义表示程序的含义，由静态语义和动态语义组成。静态语义指程序编译时可以确定的语法成分的含义；建立在转换/迁移系统上的动态语义则描述程序如何执行。
|
||||
%
|
||||
|
|
@ -26,7 +26,7 @@
|
|||
|
||||
|
||||
通用语言的程序可以像OpenMP那样插入新的语言机制的语句；也可以反过来在大数据处
|
||||
理编程框架MapReduce、Hadoop、Spark新风格的程序中插入通用语言的子程序，不仅简
|
||||
理编程框架MapReduce、Hadoop、Spark等新风格的程序中插入通用语言的子程序，不仅简
|
||||
化了分布式并行数据处理编程，而且允许程序员设计灵活高效的程序用于数据处理；一
|
||||
些编程模型的实现甚至不引入任何新的语法扩展，仅仅以子程序库的形式出现，比如科
|
||||
学计算中广泛使用的MPI由C和Fortran程序库实现，支持多种形式的消息传递通讯。
|
||||
|
|
@ -65,7 +65,7 @@
|
|||
\begin{figure}[htbp]
|
||||
\centering
|
||||
\includegraphics[width=0.99\textwidth]{fig1-2/2-2.png}
|
||||
\caption{程序设计语言的发展及分类}
|
||||
\caption{程序设计语言的发展及分类}\todo{改图，去掉“系统编程语言”中的“语言”}
|
||||
\label{fig:2-2}
|
||||
\end{figure}
|
||||
|
||||
|
|
@ -100,7 +100,7 @@
|
|||
|
||||
符号主义就是以符号逻辑系统\index{符号逻辑系统}为基础来表示知识。二十世纪七十年代，Robert Kowalski 等人提出了逻辑可以作为程序设计语言的基本思想，把逻辑和计算这两个截然不同的概念统一在一起。这就是逻辑程序设计(Logic Programming)，而Prolog语言就是典型的逻辑程序设计语言。对经典的逻辑程序设计语言，可以进行各种扩充。例如，将状态转移的控制机制引入到时序逻辑系统的XYZ/E是世界上第一个可执行的时序逻辑程序设计语言~\cite{Tang2002}。
|
||||
|
||||
连接主义的代表是试图模拟人脑的人工神经网络。近十年来，深度学习显示出了强大的学习能力和广泛的应用前景。TensorFlow、PyTorch等工具针对深度神经网络学习算法的特点，便于高级语言调用相应的接口，搭建神经网络结构然后以高性能方式运行学习算法。这些多样的领域特定语言工具不具备完整的通用程序设计语言功能，但十分适合特定的应用场景。
|
||||
连接主义的代表是试图模拟人脑的人工神经网络。近十年来，深度学习显示出了强大的学习能力和广泛的应用前景。TensorFlow、PyTorch等工具针对深度神经网络学习算法的特点，提供便于高级语言调用相应的接口，搭建神经网络结构然后以高性能方式运行学习算法。这些多样的领域特定语言工具不具备完整的通用程序设计语言功能，但十分适合特定的应用场景。
|
||||
|
||||
\begin{itemize}
|
||||
\item 个人计算与系统编程(1981$\sim$)
|
||||
|
|
@ -275,18 +275,18 @@ Floyd-Hoare逻辑中，程序与断言是分离的，而且也无法表达活性
|
|||
|
||||
近期提出的K框架提供了基于重写的语言~\cite{Rosu15}，用于定义程序设计语言的操作语义。结合K语言语义及相应的逻辑推理过程，可以在统一的框架中分析和验证各种程序设计语言编写的程序。
|
||||
|
||||
目前，形式验证方法已经应用于一些大型软件。例如，微内核操作系统seL4的ARM版本是第一个带有完整的代码级的功能正确性证明的通用操作系统内核，可以应用于金融，医疗，汽车，航空电子设备和国防部门。它的验证使用了Isabelle/HOL定理证明，这意味着通过形式化方法证明了实现(使用C语言编写)是满足其规约的。再如，对编译器的验证，可以保证程序从编写到产生的可执行代码的正确性。适用于C99编程语言的大部分语法的CompCert就是一个经过正式验证的优化编译器，支持PowerPC、ARM、RISC-V、x86和x86-64架构。
|
||||
目前，形式验证方法已经应用于一些大型软件。例如，微内核操作系统seL4的ARM版本是第一个带有完整的代码级的功能正确性证明的通用操作系统内核，可以应用于金融、医疗、汽车、航空电子设备和国防部门。它的验证使用了Isabelle/HOL定理证明，这意味着通过形式化方法证明了实现(使用C语言编写)是满足其规约的。再如，对编译器的验证，可以保证程序从编写到产生的可执行代码的正确性。适用于C99编程语言的大部分语法的CompCert就是一个经过正式验证的优化编译器，支持PowerPC、ARM、RISC-V、x86和x86-64架构。
|
||||
|
||||
|
||||
\begin{itemize}
|
||||
\item 软件模型检验
|
||||
\item 模型检验
|
||||
\end{itemize}
|
||||
|
||||
%由Edmund M. Clarke、E. Allen Emerson和Joseph Sifakis提出的
|
||||
模型检验\index{模型检验}方法通过自动遍历系统模型的有穷状态空间，来检验系统的语义模型与其性质规约之间的满足关系。软件系统属于无穷状态系统，即使状态有穷，其状态空间规模通常远超当前计算机可处理的范围。在硬件系统模型检验取得巨大成功的时候，软件模型检验面临着严峻的挑战。对于无穷状态系统，符号化可达性分析可能不终止。软件模型检验的核心问题是如何建立可检验规模的软件模型(抽象)。一种方法是采用保守近似对模型进行抽象，另一种方法是使用限界模型检验，将模型空间爆炸涉及的参数(例如循环次数、并发数等)限制在一定范围内，验证系统模型在此深度内是否满足系统规约。在软件模型检验中，利用静态分析、符号执行\index{符号执行}等方法抽取程序模型，以及基于路径的模型检验等静态和动态结合的方法，也是有效提高模型检验扩展性的重要途径。%近年来，将模型检验与定理证明有效地结合也是一个有前景的研究方向。
|
||||
|
||||
\subsection{程序的自动综合}
|
||||
按照某种形式规约表达的用户意图，程序综合\index{程序综合}能够使用指定的编程语言自动生成符合规约的程序代码。程序综合器通常在程序空间上执行某种形式的搜索，以生成与各种类型一致的程序约束(例如输入输出示例，演示，自然语言，部分程序和断言)。程序综合是编程理论中最核心的问题之一~\cite{pnueli1989synthesis}。早期的想法是通过组合子问题生成带有证明的、可解释的实现。一个分支是使用定理证明器首先证明用户提供的规约，再使用这个证明提取相应的程序逻辑。而另一个较为流行的方法是从一个高层规约开始，不断的进行转换，直到实现目标程序。近期的程序综合方法中，用户提供规约的同时，还可以提供目标程序的语法框架。这样使得基于语法结构进行的综合过程更加高效，得到的程序的可解释性更高。
|
||||
按照某种形式规约表达的用户意图，程序综合\index{程序综合}能够使用指定的编程语言自动生成符合规约的程序代码。程序综合器通常在程序空间上执行某种形式的搜索，以生成与各种类型一致的程序约束(例如输入输出示例、演示、自然语言、部分程序和断言)。程序综合是编程理论中最核心的问题之一~\cite{pnueli1989synthesis}。早期的想法是通过组合子问题生成带有证明的、可解释的实现。一个分支是使用定理证明器首先证明用户提供的规约，再使用这个证明提取相应的程序逻辑。而另一个较为流行的方法是从一个高层规约开始，不断的进行转换，直到实现目标程序。近期的程序综合方法中，用户提供规约的同时，还可以提供目标程序的语法框架。这样使得基于语法结构进行的综合过程更加高效，得到的程序的可解释性更高。
|
||||
|
||||
\subsection{程序的精化}
|
||||
程序精化\index{程序精化}是将抽象（高级）形式规范可验证地转换为具体（低级）可执行程序的过程，是通过逐步细化分阶段完成。精化（Refinement）是一种数学表示法和若干规则的集合，它对Dijkstra的卫式命令语言进行扩充，通过结合规约语句、精化规则和语言本身，从程序规约推导出命令式程序。程序精化(程序规约转换成可执行代码)可分为数据精化和算法精化两种，将程序逐步转换为更加便于实现的形式：数据精化把抽象的数据结构转换为可以高效实现的形式；算法精化将程序逐步转换为更加便于实现的代码形式。
|
||||
|
|
|
|||
|
|
@ -169,12 +169,19 @@
|
|||
\subsection{新型计算模型下的算法复杂性理论与程序验证方法}\label{sec:stc-quantum}
|
||||
针对量子计算模型下的挑战性问题，具体研究内容如下：量子程序设计与验证、量子密码协议设计与验证、量子复杂性下界问题等。量子程序设计与验证的研究包括量子程序设计模型和基本指令集；适用于量子计算的程序逻辑；量子程序不变式生成问题；量子程序的模型检验问题；并行与分布式量子程序设计技术等。量子密码协议设计与验证的研究包括抗量子攻击的经典密码协议，量子随机数生成，量子密码协议验证，量子纠错与编码等。量子复杂性下界研究包括图灵机模型下量子与经典复杂性类的（神谕）区分；量子通信协议复杂性下界；量子判定树模型复杂性下界；量子计算的交互式验证等。
|
||||
|
||||
\subsection{新型软件及应用的处理与分析方法}\label{sec:stc-newsoftware}
|
||||
\subsection{新型软件及应用的可靠性分析方法}\label{sec:stc-newsoftware}
|
||||
|
||||
对于近年来新出现的各种软件及应用，核心问题是在提高系统效率的同时，如何保证系统的可靠性。基于机器学习的系统是近期出现的主流新型软件之一。
|
||||
对于近年来新出现的各种软件及应用，核心问题是如何在提高系统功效的同时，保证系统的可靠性。基于机器学习的系统是近期出现的主流新型软件之一。
|
||||
%根据不同的系统需求，有不同的研究方法。
|
||||
主要研究内容包括如何快速攻击系统并产生对抗样本；如何有效防御对基于学习系统的攻击；如何以形式化分析为基础提供该类系统的可靠性、鲁棒性等保证。
|
||||
%主要研究内容包括如何快速攻击系统并产生对抗样本；如何有效防御对基于学习系统的攻击；如何以形式化分析为基础提供该类系统的可靠性、鲁棒性等保证。
|
||||
%如对部分系统进行验证、将语义作为训练内容增加系统可解释性、根据网络结构特点构建输出的监测器。
|
||||
基于逻辑演绎的规约-实现一致性是传统软件质量保障的基础。然而机器学习实现的是（不完全）归纳推理，具有内在的不确定性。
|
||||
基于深度神经网络（DNN）模型的统计机器学习近年获得重大进展，但其行为缺乏可解释性。
|
||||
将训练好的DNN模型提供给第三方作为软件部件使用时，其可靠性成为尤为突出的问题。
|
||||
如何建立针对这类软件建立合理、适用的软件可靠性理论框架并给出高效的分析与保障方法，是亟待深入研究的问题。
|
||||
当前针对DNN的对抗样例生产和鲁棒性分析引起广泛关注，
|
||||
但目前报道的进展与其说是解决了问题不如说是展示了问题的严重性和困难性。
|
||||
|
||||
|
||||
%一类研究围绕着如何攻击与防御人工智能系统。基于学习的模型极易受到噪音的影响，输入中的一点噪音就会改变输出结果。因此对抗样本是不可避免的。在实际系统中，对抗样本攻击的成功率非常高。如何快速地寻找对抗样本，进行攻击，是个重要的研究问题。它本质是一个优化问题，通常可以利用梯度下降优化的方法得到较好的解。目前较新的方法将模型与噪声都转变成优化目标项，而输出限制条件转换成损失函数，值域限制被转换成了平滑截断函数的变量，这样优化器可以通过直接优化目标函数，得到对抗样本。除了对抗样本的寻找，另一个方向是如何进行防御，如对抗训练、防御蒸馏等。有研究表明，即使在有防御蒸馏保护的前提下，仍可以通过转移学习生成有效的对抗样本。
|
||||
%
|
||||
|
|
|
|||
|
|
@ -68,7 +68,7 @@
|
|||
|
||||
其次，编译器需要能够高效地处理混成系统\index{混成系统}。现在的软件系统越来越复杂，形成了一个混成的系统，需要既能处理离散的又能处理连续的计算，既能处理确定性（逻辑式）的又能处理概率性的计算，既针对命令式的又针对函数式的程序设计语言，既可静态类型检查又可以动态确认程序满足的性质。为了开发这样的复杂的软件系统，混成语言以及相应编译技术变得非常重要。此外，复杂软件系统可能由不同程序设计语言书写的程序组成。对不同程序设计语言所书写的程序进行高效混成编译，也是一个值得关注的研究问题。
|
||||
\subsection{程序设计语言的安全性保障}\label{2_3_1_5}
|
||||
程序设计语言的安全性，体现在两个方面：程序设计语言自身的安全性设计与其支撑环境（如库、编译器、解释器、运行时等）的安全性保障。程序设计语言的设计者和实现者都在不遗余力的提升程序设计语言的安全性。当前，程序设计语言的安全性方面，还存在以下的重大挑战问题。
|
||||
程序设计语言的安全性（Safety），体现在两个方面：程序设计语言自身的安全性设计与其支撑环境（如库、编译器、解释器、运行时等）的安全性保障。程序设计语言的设计者和实现者都在不遗余力的提升程序设计语言的安全性。当前，程序设计语言的安全性方面，还存在以下的重大挑战问题。
|
||||
|
||||
|
||||
首先，需要建立语言安全性和灵活性、复杂性之间的平衡。程序设计语言的安全性主要体现为程序设计模型中一组机制，保障程序员写出安全的程序。例如，C++支持的RAII（资源获取即初始化）通过栈语义保证对象析构函数的自动调用，解决了内存泄漏问题；类型系统使代码仅能访问被授权可以访问的内存位置；脸书公司推出的智能合约语言Move语言不支持动态分配和循环递归依赖等\cite{ 2019Move}等。然而，语言安全性的提升意味着程序设计灵活性的下降、支撑环境复杂性的提升。为此，在设计一门程序设计语言的同时，需要定义一组通用的或领域/环境相关的安全机制，包括是否支持指针、自动垃圾回收、异常处理，是否支持强类型检查和中间码验证等，一方面允许程序设计人员编写出既功能强大又足够安全的程序，另一方面在静态编译或者动态执行时实现程序的安全性检查。
|
||||
|
|
|
|||
Loading…
Reference in New Issue