update for Haodan
This commit is contained in:
parent
f22a897e3f
commit
93ba0c3f84
|
|
@ -1,64 +1,83 @@
|
|||
% !TEX root = main.tex
|
||||
\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}从高级语言机制的设计角度对程序设计语言进行了深入细致的介绍和比较。大多数程序设计语言的创建都受其之前语言概念的启发，而新出现的程序设计语言提供更强更为自然的抽象设施，使程序员的工作变得更加简单、有效。
|
||||
|
||||
%程序设计语言的定义可分为语法、语义等方面。语义表示程序的含义，由静态语义和动态语义组成。静态语义指程序编译时可以确定的语法成分的含义；建立在转换/迁移系统上的动态语义则描述程序如何执行。
|
||||
%
|
||||
\section{程序设计语言}
|
||||
|
||||
在计算机发展的早期，人们往往是用二进制(0/1序列)给计算机发指令。这显然很不方便。后来，逐渐出现了汇编语言\index{汇编语言}以及各种高级语言。一般来说，提高软件开发本身的效率与质量需要更抽象更高级的程序设计语言；而提高现实计算机硬件系统的利用率和执行效率，则需要使用较低级的程序设计语言，这样程序可以更直接地控制硬件资源。较通用的程序设计语言适用于广泛的应用领域和应用场景，可吸引大量的语言使用者，积累充足的遗产代码，便于培训与推广共享资源；但高度通用的语言设计上难以兼顾开发效率与执行效率。很多针对特定应用领域的程序设计语言更容易通过合适的语言机制同时改善软件开发与执行的效率。多样化的编程接口具有程序设计语言功能，但缺乏相应的编程框架甚至程序库等。这类接口反映了相应的编程模型的特点，实质上起到了程序设计语言的作用。
|
||||
在计算机发展的早期，人们往往是用二进制(0/1序列)给计算机发指令。这显然很不方便。后来，逐渐出现了汇编语言\index{汇编语言}以及各种高级语言。一般来说，提高软件开发本身的效率与质量需要更符合人类思维的程序设计语言；而提高现实计算机硬件系统的利用率和执行效率，则需要使用较低级的程序设计语言，这样程序可以更直接地控制硬件资源。较通用的程序设计语言适用于广泛的应用领域和应用场景，可吸引大量的语言使用者，积累充足的遗产代码，便于培训与推广共享资源；但高度通用的语言设计上难以兼顾开发效率与执行效率。很多针对特定应用领域的程序设计语言更容易通过合适的语言机制同时改善软件开发与执行的效率。此外，多样化的编程接口常具有部分的程序设计语言功能，反映了相应的编程模型的特点，也可以起到程序设计语言的作用。
|
||||
|
||||
程序设计语言的发展因计算机系统发展的驱动和行业应用需求发展的推动，不同语言不同程度地受这些因素推动。新出现的程序设计语言通常是应对新兴应用或者新兴计算机体系结构的需要。但从程序设计语言发展历史角度看，应用需求的影响明显处于主导地位。
|
||||
程序设计语言的发展往往在不同程度上得到了计算机系统和行业应用需求发展的推动。
|
||||
新出现的程序设计语言通常是应对新兴应用或者新兴计算机体系结构的需要。从程序设计语言发展历史角度看，应用需求的影响明显处于主导地位。
|
||||
|
||||
\subsection{语言的设计、实现及生命期}
|
||||
为了便于使用与推广，程序设计语言的设计与实现通常要遵守一定的规则。同时，不同应用的涌现也推动了多种程序设计语言的提出与发展。
|
||||
|
||||
\subsubsection{设计}
|
||||
一般说来，程序语言的设计应该遵守以下原则\footnote{http://people.cs.aau.dk/$\sim$bt/DAT5E07/PrgLDesign.pdf}：
|
||||
\begin{itemize}
|
||||
\item 可读性：能够很容易的理解；
|
||||
\item 可写性：能够清晰、准确地表达计算意图；
|
||||
\item 可靠性：确保程序不会导致意外；
|
||||
\item 正交性(Orthogonality)：每种语言构造的组合都是合法的；
|
||||
\item 一致性：相似的特点有相似的表示和行为；
|
||||
\item 可维护性：能够很容易发现错误并纠正；
|
||||
\item 通用性：若干结构可以组合成更通用的结构；
|
||||
\item 可扩展性：能够给用户提供加入新结构的机制；
|
||||
\item 标准化性(Standardability)：允许程序在不同机器和系统间的移植；
|
||||
\item 可实现性：能够编写对应的转换器\index{转换器}或解释器\index{解释器}。
|
||||
\item 程序语言的构造方面：
|
||||
\begin{itemize}
|
||||
\item 可读性：能够很容易的理解；
|
||||
\item 可写性：能够清晰、准确地表达计算意图；
|
||||
\item 通用性：若干结构可以组合成更通用的结构；
|
||||
\item 正交性(Orthogonality)：每种语言构造的组合都是合法的；
|
||||
\item 一致性：相似的特点有相似的表示和行为；
|
||||
\end{itemize}
|
||||
\item 程序语言的实现方面：
|
||||
\begin{itemize}
|
||||
\item 可实现性：能够编写对应的转换器\index{转换器}或解释器\index{解释器}；
|
||||
\item 可靠性：确保程序不会导致意外；
|
||||
\item 可维护性：能够很容易发现错误并纠正；
|
||||
\item 可扩展性：能够给用户提供加入新结构的机制；
|
||||
\item 可标准化性(Standardability)：允许程序在不同机器和系统间的移植。
|
||||
\end{itemize}
|
||||
\end{itemize}
|
||||
语言设计在实践中有三个角度：从程序设计语言理论角度出发设计的语言如Pascal、Ocaml、X10等十分关注语言语义的清晰性、灵活性、简洁性，往往直接反映了理论领域的创新成果；从系统软件与体系结构角度出发设计的语言如图形处理器支持的CUDA，关注如何充分利用系统结构的特点来优化性能；从应用角度出发设计的语言如XML、PHP、Julia等关注与目标应用的契合度以及编程的便易性。
|
||||
语言设计是上述几方面原则的综合权衡，在实践中有不同角度，体现不同的侧重点：从程序设计语言理论角度出发设计的语言如Pascal、Ocaml、X10等十分关注语言语义的清晰性、灵活性、简洁性，往往直接反映了理论领域的创新成果；从系统软件与体系结构角度出发设计的语言如图形处理器支持的CUDA，关注如何充分利用系统结构的特点来优化性能；从应用角度出发设计的语言如XML、PHP、Julia等关注与目标应用的契合度以及编程的便易性。
|
||||
|
||||
某些语言如数据库查询语言SQL简洁地表示数据表格间的代数关系\index{代数关系}，大幅简化了对数据库\index{数据库}的查询；深度学习编程框架\index{编程框架}TensorFlow~\cite{abadi2016tensorflow}、PyTorch等辅助编程者方便地生成神经网络结构\index{神经网络结构}并根据学习算法自动生成反向网络。这些语言或框架追求编程简单性，虽然简化了循环和递归这样的图灵可计算性的关键语句，但仍然反映了一定的程序设计模型\index{程序设计模型}。
|
||||
某些语言如数据库查询语言SQL简洁地表示数据表格间的代数关系\index{代数关系}，大幅简化了对数据库\index{数据库}的查询；深度学习编程框架\index{编程框架}TensorFlow~\cite{abadi2016tensorflow}、PyTorch等辅助编程者方便地生成神经网络结构\index{神经网络结构}并根据学习算法自动生成反向神经网络。这些语言或框架追求编程简单性，虽然简化了循环和递归这样的图灵可计算性的关键语句，但仍然反映了一定的程序设计模型\index{程序设计模型}。
|
||||
|
||||
\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语言不同的共享变量式并行编程模型，我们也可以称之为新的“语言”或者至少是新的“语言机制”。
|
||||
|
||||
通用语言的程序可以像OpenMP那样插入新的语言机制的语句，也可以反过来在新风格的程序中插入通用语言的子程序。这一方式在大数据处理编程框架MapReduce、Hadoop、Spark中得以应用，不仅简化了分布式并行数据处理编程，而且允许程序员设计灵活高效的程序用于数据处理。一些编程模型的实现甚至不引入任何新的语法扩展，仅仅以子程序库的形式出现。比如，科学计算中广泛使用的MPI由C和Fortran程序库实现，支持多种形式的消息传递通讯。
|
||||
通用语言的程序可以像OpenMP那样插入新的语言机制的语句；也可以反过来在大数据处
|
||||
理编程框架MapReduce、Hadoop、Spark新风格的程序中插入通用语言的子程序，不仅简
|
||||
化了分布式并行数据处理编程，而且允许程序员设计灵活高效的程序用于数据处理；一
|
||||
些编程模型的实现甚至不引入任何新的语法扩展，仅仅以子程序库的形式出现，比如科
|
||||
学计算中广泛使用的MPI由C和Fortran程序库实现，支持多种形式的消息传递通讯。
|
||||
%近年来，随着计算机系统结构\index{计算机系统结构}的多样化和复杂化，程序设计语言的实现出现了许多新的形式。一种方式是在已有的程序设计语言中加入实现不同功能的语句，构建新的语言机制。例如，并行编程模型\index{并行编程模型}OpenMP使用预编译制导语句插在C或Fortran的代码中，描述了多线程并行。尽管OpenMP本身不具有完整的独立语法，但因为反映了与串行C语言不同的共享变量式并行编程模型，我们也可以称之为新的“语言”或者至少是新的“语言机制”。
|
||||
%\note{本段是不是主要指一些语言采取库的实现方式？建议与实现方式能一致系统的描述}
|
||||
%第二种实现方式是在新风格的程序中插入通用语言的子程序。
|
||||
%%通用语言的程序可以像OpenMP那样插入新的语言机制的语句，也可以反过来在新风格的程序中插入通用语言的子程序。
|
||||
%这一方式在大数据处理编程框架MapReduce、Hadoop、Spark中得以应用，不仅简化了分布式并行数据处理编程，而且允许程序员设计灵活高效的程序用于数据处理。
|
||||
%第三种方式是编程模型的实现不引入任何新的语法扩展，仅仅以子程序库的形式出现。比如，科学计算中广泛使用的MPI由C和Fortran程序库实现，支持多种形式的消息传递通讯。
|
||||
|
||||
\subsubsection{发展}
|
||||
|
||||
\begin{figure}[htbp]
|
||||
\centering
|
||||
\includegraphics[width=0.95\textwidth]{fig1-2/2-1.png}
|
||||
\caption{常见程序设计语言的发展脉络
|
||||
\label{fig:2-1}}
|
||||
\end{figure}
|
||||
%\begin{figure}[htbp]
|
||||
% \centering
|
||||
% \includegraphics[width=0.95\textwidth]{fig1-2/2-1.png}
|
||||
% \caption{常见高级程序设计语言的发展脉络
|
||||
% \label{fig:2-1}}
|
||||
%\end{figure}
|
||||
|
||||
自20世纪60年代以来的发展历程看，程序设计语言的抽象级别显著提高。历史上曾出现过将程序设计语言分为四代的提法：
|
||||
|
||||
\begin{enumerate}[1)]
|
||||
\item 机器语言\index{机器语言}：由二进制0、1代码指令构成，不同的处理器具有不同的指令系统。由于机器语言难编写和维护，人们已很少直接使用这种语言。
|
||||
\item 汇编语言\index{汇编语言}：汇编语言指令可以直接访问系统接口。由汇编程序翻译成的机器语言程序效率高。但同样难以使用与维护。
|
||||
\item 高级语言：它是面向用户的，独立于计算机种类与结构。因此易学易用，通用性强，应用广泛。图\ref{fig:2-1}给出了常见高级程序设计语言的发展脉络\footnote{https://exploring-data.com/vis/programming-languages-influence-network/}，其中箭头指向的程序设计语言借鉴了前驱的设计思想。
|
||||
\item 高级语言：它是面向用户的，独立于计算机种类与结构。因此易学易用，通用性强，应用广泛。%图\ref{fig:2-1}给出了常见高级程序设计语言的发展脉络\footnote{https://exploring-data.com/vis/programming-languages-influence-network/}，其中箭头指向的程序设计语言借鉴了前驱的设计思想。
|
||||
\item 声明式语言\index{非过程化语言}：使用这种语言编码时只需说明“做什么”，不需描述算法细节。数据库查询语言是其中的一种，用户可以对数据库中的信息进行复杂的操作。
|
||||
\end{enumerate}
|
||||
|
||||
在程序设计语言发展最初阶段，程序设计语言按照主要编程范型\index{编程范型}，可以被归类为过程式、面向对象、函数式~\cite{hu2015functional}等。随着C++、C\#等语言的出现，传统分类之间的界限逐渐变得模糊。现代的编程语言往往具有若干种类编程语言的元素，这就是所谓的多范型编程语言。而多范型程序设计语言\index{多范型程序设计语言}也是一个越来越明显的趋势。
|
||||
在程序设计语言发展最初阶段，程序设计语言按照主要编程范式\index{编程范式}，可以被归类为过程式、面向对象、函数式~\cite{hu2015functional}、逻辑式等。随着C++、C\#等语言的出现，传统分类之间的界限逐渐变得模糊。现代的编程语言往往具有若干种类编程语言的元素，这就是所谓的多范式编程语言。而多范式程序设计语言\index{多范式程序设计语言}也是一个越来越明显的趋势。
|
||||
|
||||
%一个成功的程序设计语言从探索到推广、接受和最终成为行业标准往往经历以下四个阶段：第一阶段，在应用与系统的软件开发过程中不断完善；第二阶段，为提高软件生产率，提供方便灵活的开发工具；第三阶段，行业的积累有助于产生相应的遗产代码资源，并推广资源；第四阶段，随着大量遗产代码开始积累，行业标准成型，行业倾向于使用成熟的程序设计语言。分析程序设计语言所处的发展阶段有助于我们了解甚至预测其发展趋势。
|
||||
|
||||
一个成功的程序设计语言从探索到推广、接受和最终成为行业标准往往经历以下四个阶段：第一阶段，新兴应用与系统的软件开发在早期开发过程只能采用已有的程序设计语言配以一定的软件工程方法；第二阶段，为提高软件生产率，多种语言工具开始出现；第三阶段，行业标准的形成有助于积累遗产代码资源和培训与推广资源；第四阶段，随着大量遗产代码开始积累，行业商业模式成型，倾向于使用成熟的程序设计语言。分析程序设计语言所处的发展阶段有助于我们了解甚至预测其发展规律。
|
||||
|
||||
\subsection{应用驱动的程序设计语言发展}
|
||||
|
||||
|
|
@ -70,15 +89,17 @@
|
|||
\end{figure}
|
||||
|
||||
%这里以多个有代表性的语言为例，分析其应用背景、设计特点与发展规律，从而展现程序设计语言发展的历史与现状。
|
||||
按照程序设计语言的类型与应用，图\ref{fig:2-2}给出了以时间为主线的不同类别语言的发展过程与分类关系。从不同角度来看，一种程序设计语言既可能属于系统编程语言，又是面向对象语言。从发展过程来看，一种语言在发展过程中会不断进行扩充，融入不同的范型，进而趋近于多范型语言。计算机产业的发展往往是新的产业应用从已有的应用模式中成长出来而不是取而代之。新语言的出现往往标志着信息技术在新的应用领域的扩张。本节主要以应用驱动来组织。
|
||||
|
||||
按照程序设计语言的类型与应用，图\ref{fig:2-2}给出了以时间为主线的不同类别语言的发展过程与分类关系。从不同角度来看，一种程序设计语言既可能属于系统编程语言，又是面向对象语言。从发展过程来看，一种语言在发展过程中会不断进行扩充，融入不同的范式，进而趋近于多范式语言。计算机产业的发展往往是新的产业应用从已有的应用模式中成长出来而不是取而代之。新语言的出现往往标志着信息技术在新的应用领域的扩张。本节主要以应用驱动来组织。
|
||||
|
||||
|
||||
\begin{itemize}
|
||||
\item 科学与工程计算(1954$\sim$)
|
||||
\end{itemize}
|
||||
\end{itemize}
|
||||
|
||||
|
||||
早期计算机系统硬件结构简单，软件专用性强，主要用于核反应计算、密码破译这样专业性强的科学与工程计算领域，直接服务对象往往是政府与军工。由John Backus主导实现的Fortran语言标志着具有完整工具链的程序设计语言出现。Fortran语言符合典型的过程式语言的特征，由从事系统结构和系统软件的研究人员设计，采取编译的方式实现，反映了程序设计与计算机系统之间的紧密联系。尽管串行的科学计算软件开发方法已成熟，积累的大量遗产代码保证了Fortran这样的语言在其适用领域仍然具有生命力。
|
||||
早期计算机系统硬件结构简单，软件专用性强，主要用于核反应计算、密码破译这样专业性强的科学与工程计算领域，解决数值计算问题，直接服务对象往往是政府与军工。由John Backus主导实现的Fortran语言标志着具有完整工具链的程序设计语言出现。Fortran语言符合典型的过程式语言的特征，由从事系统结构和系统软件的研究人员设计，采取编译的方式实现，反映了程序设计与计算机系统之间的紧密联系。串行的科学计算软件开发方法已成熟，积累的大量遗产代码保证了Fortran这样的语言在其适用领域仍然具有生命力。
|
||||
|
||||
早期语言的准确语义往往依赖于编译器的实现，针对特定体系结构由编译器的开发者设计。上世纪五十年代末期出现了一些由计算机逻辑理论与程序语义研究者设计和实现的程序设计语言，如ALGOL和LISP语言。上世纪七十年代后出现的大量函数式语言如ML、Haskell往往具有清楚而简洁的数学表示，设计出发点上更多地考虑如何优美地表示计算，但由于缺乏工业级应用的针对性以及性能上对常见体系结构的适配性，其接受范围受到限制。
|
||||
早期语言的准确语义往往通过编译器的实现来体现，针对特定体系结构由编译器的开发者设计。上世纪五十年代末期出现了一些由计算机逻辑理论与程序语义研究者设计和实现的程序设计语言，如ALGOL和LISP语言。上世纪七十年代后出现的大量函数式语言如ML、Haskell往往具有清楚而简洁的数学表示，设计出发点上更多地考虑如何优美地表示计算，但由于缺乏工业级应用的针对性以及性能上对常见体系结构的适配性，其应用范围受到限制。
|
||||
|
||||
科学与工程性质的计算，尤其是高性能计算往往与计算机体系结构密切相关，发展了多种形式的编程接口。OpenMP是共享内存的并行计算所常用的编程接口。其特点是在C或Fortran中插入指导语句，希望不改变原有串行程序语义的条件下利用共享存储器的多线程并行加速计算。MPI是跨平台的消息传递通讯程序库，完全不增加额外的语法机制。图形处理器语言CUDA在C基础上扩展了一些语法机制，用以区分在CPU、GPU上运行的程序片段，作出不同的编译。并行程序设计模型一直是程序设计理论研究的一个重点 。
|
||||
|
||||
|
|
@ -86,15 +107,15 @@
|
|||
\item 商用计算(1960$\sim$)
|
||||
\end{itemize}
|
||||
|
||||
信息技术的应用逐渐从专业领域扩展到广阔的商业领域信息化。COBOL语言的出现标志着商业化的事务处理如金融、财会有了强有力的语言技术支持。该时期计算系统往往是大型机或小型机服务器。COBOL拥有庞大的用户群，据称积累了超过2000亿行遗产代码\footnote{http://cobolcowboys.com/cobol-today/}。由于商业计算的多样性，一台大型机往往需要运行多种类型的软件，甚至同时并发地运行不同软件。这一时期开始，管理不同类型软件的操作系统得以发展。C语言可以直接处理系统资源，尤其适合系统软件开发。相比之下，同样是过程式语言\index{过程式语言}的PASCAL语言则是由程序设计语言理论研究者设计的更加安全和规范的语言。数据库查询语言\index{数据库查询语言}SQL是较早出现的领域专用语言。它不具有完整的程序设计语言功能，但可看成是针对关系数据库\index{关系数据库}应用的编程模型。
|
||||
信息技术的应用逐渐从专业领域扩展到广阔的商业领域信息化，相应的程序设计语言需大规模复杂事务的处理能力。COBOL语言的出现标志着商业化的事务处理如金融、财会有了强有力的语言技术支持。该时期计算系统往往是大型机或小型机服务器。COBOL拥有庞大的用户群，据称积累了超过2000亿行遗产代码\footnote{http://cobolcowboys.com/cobol-today/}。由于商业计算的多样性，一台大型机往往需要运行多种类型的软件，甚至同时并发地运行不同软件。这一时期开始，操作系统开始发展，C语言可以直接处理系统资源，尤其适合系统软件开发。相比之下，同样是过程式语言\index{过程式语言}的PASCAL语言则是由程序设计语言理论研究者设计的更加安全和规范的语言。数据库查询语言\index{数据库查询语言}SQL是较早出现的领域专用语言。它不具有完整的程序设计语言功能，但可看成是针对关系数据库\index{关系数据库}应用的编程模型。
|
||||
|
||||
随着商用计算而来的是软件大规模化。1960年代末出现了一系列旨在有效控制大规模软件开发过程复杂性的程序设计思想。面向对象的思想及其第一个语言Simula 67试图对不同程序模块访问共享变量的方式进行限制，使得程序更加具有模块组装特性。Edsger W. Dijkstra提出避免使用GOTO语句的结构化程序设计\index{结构化程序设计}思想~\cite{dijkstra1968go}，对程序的控制流进行限制。
|
||||
随着商用计算而来的是软件大规模化。1960年代末出现了一系列旨在有效控制大规模软件开发过程复杂性的程序设计思想。面向对象的思想及其第一个语言Simula 67试图通过数据封装对不同程序模块访问共享变量的方式进行限制，使得程序更加具有模块组装特性。Edsger W. Dijkstra提出避免使用GOTO语句的结构化程序设计\index{结构化程序设计}思想~\cite{dijkstra1968go}，对程序的控制流进行限制。
|
||||
|
||||
\begin{itemize}
|
||||
\item 人工智能(1960$\sim$)
|
||||
\end{itemize}
|
||||
|
||||
人工智能\index{人工智能}自诞生以来，广受关注。在该领域也出现了若干专用语言。例如，基于λ演算的函数式编程语言LISP，具有对符号表达式的支持、交互式环境和可扩展性等特性，曾大量用于人工智能系统的开发。人工智能有符号主义、连接主义等流派。
|
||||
人工智能\index{人工智能}自诞生以来，广受关注。在该领域也出现了若干专用语言，用于编写程序求解非数值计算、知识处理、推理、规划、决策等具有智能的各种复杂问题。例如，基于$\lambda$演算的函数式编程语言LISP，具有对符号表达式的支持、交互式环境和可扩展性等特性，曾大量用于人工智能系统的开发。人工智能有符号主义、连接主义等流派。
|
||||
|
||||
符号主义就是以符号逻辑系统\index{符号逻辑系统}为基础来表示知识。二十世纪七十年代，Robert Kowalski 等人提出了逻辑可以作为程序设计语言的基本思想，把逻辑和计算这两个截然不同的概念统一在一起。这就是逻辑程序设计(Logic Programming)，而Prolog语言就是典型的逻辑程序设计语言。对经典的逻辑程序设计语言，可以进行各种扩充。例如，将状态转移的控制机制引入到时序逻辑系统的XYZ/E是世界上第一个可执行的时序逻辑程序设计语言~\cite{Tang2002}。
|
||||
|
||||
|
|
@ -104,17 +125,24 @@
|
|||
\item 个人计算与系统编程(1981$\sim$)
|
||||
\end{itemize}
|
||||
|
||||
在摩尔定律背景下，计算机硬件系统的价格不断下降，个人使用计算机的情形越来越普遍。随个人计算而来的是软件的多样化，应用形式从事务处理和业务处理扩展到教育与娱乐。软件的开发与销售形式从硬件捆绑式发展到专业软件企业发行软件拷贝的销售形式。软件开发团队与人员的数目大量增加。C 语言是一种通用的、面向过程式的计算机程序设计语言。计算机系统设计以及应用程序编写是C语言应用的主要领域。 C++是C语言的面向对象扩展，又增加了泛型编程机制，更适合大中型程序的开发。
|
||||
|
||||
作为一种新的多范型语言，Rust不仅能够提供友好的编译器和清晰的错误提示信息，而且速度快、内存利用率高，同时具有丰富的类型系统保证内存安全和线程安全。目前从初创公司到大型企业，已有很多公司都在使用 Rust，应用非常广泛。
|
||||
在摩尔定律背景下，计算机硬件系统的价格不断下降，个人使用计算机的情形越来越普遍。随个人计算而来的是软件的多样化，应用形式从事务处理和业务处理扩展到教育与娱乐。
|
||||
%软件的开发与销售形式从硬件捆绑式发展到专业软件企业发行软件拷贝的销售形式。
|
||||
软件开发团队与人员的数目大量增加。为了便于使用与推广，相应的程序设计语言不仅构成简单，而且功能较全，适应面广。
|
||||
BASIC是在计算机发展史早期应用最为广泛的程序设计语言之一，它结构简单、易于学习、执行方式灵活，很快就普遍流行起来。
|
||||
%C 语言是一种通用的、面向过程式的计算机程序设计语言。计算机系统设计以及应用程序编写是C语言应用的主要领域。
|
||||
C++是C语言的面向对象扩展，又增加了泛型编程机制，更适合大中型程序的开发。
|
||||
|
||||
作为一种新的多范式语言，Rust不仅能够提供友好的编译器和清晰的错误提示信息，而且速度快、内存利用率高，同时具有丰富的类型系统保证内存安全和线程安全。目前从初创公司到大型企业，已有很多公司都在使用 Rust，应用非常广泛。
|
||||
|
||||
\begin{itemize}
|
||||
\item Web服务与移动计算(1990$\sim$)
|
||||
\end{itemize}
|
||||
|
||||
伴随互联网的出现，Web服务软件一改拷贝销售形式，直接通过互联网向终端用户提供服务。其服务形式多样，方式多变。服务的反应速度往往受限于互联网的带宽与延迟，而不是计算的速度。因此，客户端与服务器端交互程序设计语言重点关注软件的开发效率，而不是程序的性能。典型的支持此类应用的脚本语言有JavaScript、PHP等。
|
||||
伴随互联网的出现，Web服务软件一改拷贝销售形式，直接通过互联网向终端用户提供服务。其服务形式多样，方式多变。服务的反应速度往往受限于互联网的带宽与延迟，而不是计算的速度。客户端与服务器端交互程序设计语言重点关注软件的开发效率，而不是程序的性能。典型的支持此类应用的脚本语言有JavaScript、PHP等。
|
||||
|
||||
1990年代后智能手机的出现与普及将计算拓展到个人随身携带的新模式。一些为Web服务设计的语言仍然适用，但新的应用形式也带来了新的挑战。许多项目需要同时以网页、平板以及智能手机形式提供服务。由于应用需求与服务逻辑的易变性，软件的任何更新希望在不同平台上一致地更新。它们不仅需要支持复杂的功能，还需要解决跨平台、跨设备、跨操作系统兼容可移植的难题。
|
||||
Java语言具有平台独立及可移植性等特点，被广泛用于Web应用程序、桌面应用程序和嵌入式系统应用程序的开发。
|
||||
|
||||
\begin{itemize}
|
||||
\item 大数据分析与处理(2004$\sim$)
|
||||
|
|
@ -129,51 +157,57 @@
|
|||
%基本的Map与Reduce命令还不能涵盖一般的并行计算步骤的数据依赖关系。
|
||||
|
||||
\begin{itemize}
|
||||
\item 互联网金融(2009$\sim$)
|
||||
\item 区块链计算(2009$\sim$)
|
||||
\end{itemize}
|
||||
|
||||
以软件为核心的互联网金融指的是以互联网为载体的金融服务形式，而并非仅仅将互联网作为连接客户的信息系统。开源软件技术主导的金融服务形式始于2009年出现的第一个数字货币--比特币。数字货币以去中心化共识的区块链记账技术为基础，提供类似法定货币的金融功能，具有特殊的金融服务属性。以太坊数字货币扩展了记账技术，支持区块链中记录完整的程序并以可验证的方式执行这样的程序：合同即是程序，程序即是合同。这就是所谓的智能合约(Smart Contract)。Solidity是目前最流行的合约编程语言。Solidity语法类似于JavaScript，支持继承、类和复杂的用户定义类型，通过编译的方式生成以太坊虚拟机中的代码。
|
||||
以软件为核心的互联网金融指的是以互联网为载体的金融服务形式，而并非仅仅将互联网作为连接客户的信息系统。开源软件技术主导的金融服务形式始于2009年出现的第一个数字货币--比特币。区块链是比特币的底层技术，是一个去中心化的数据库，具有分布式数据存储、点对点传输、共识机制、加密算法等计算机技术的新型应用模式。数字货币以区块链记账技术为基础，提供类似法定货币的金融功能，具有特殊的金融服务属性。以太坊数字货币扩展了记账技术，支持区块链中记录完整的程序并以可验证的方式执行这样的程序：合同即是程序，程序即是合同。这就是所谓的智能合约(Smart Contract)。Solidity是目前最流行的合约编程语言。Solidity语法类似于JavaScript，支持继承、类和复杂的用户定义类型，通过编译的方式生成以太坊虚拟机中的代码。
|
||||
|
||||
|
||||
|
||||
\section{程序理论}
|
||||
程序设计语言都具有语法和语义。语义表示程序的含义。程序理论涵盖程序设计语言的设计、实现，以及程序正确性的分析方法等。本节将介绍程序设计语言的语法与语义基础，并给出描述程序设计规范的形式化方法，如图\ref{fig:1-2-4}所示。其中，形式语言是用数学方法研究程序设计语言的语法，研究语言的组成规则。类型理论\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{程序设计语言的发展及分类}
|
||||
\caption{程序理论的发展时间线}
|
||||
\label{fig:1-2-4}
|
||||
\end{figure}
|
||||
|
||||
\subsection{程序设计语言的词法与语法}
|
||||
程序设计语言都有自己的词法和语法，而词法和语法的定义是一系列规则的集合，这些规则的基础就是形式语言。文法\index{文法}是形式语言中十分重要的基本概念，是描述语言的语法结构的一组形式规则。文法有四种分类，其中最常用的为正则语言\index{正则语言}和上下文无关语言\index{上下文无关语言}。正则语言可以用正规式定义，上下文无关语言可以用上下文无关文法(元素和规则的集合)定义。程序设计语言中的大多数算术表达式可用上下文无关文法\index{上下文无关文法}生成。正则语言是最简单的语言类，是上下文无关语言类的一个真子类。对程序设计语言编写的程序进行分析和处理(编译)时，需要判断对应的句子是否合法，可以通过对应语言的自动机进行判断。自动机是语言的另一种表示方法。其中，正则语言可以转换成有限状态自动机\index{有限状态自动机}、上下文无关语言可转换成下推自动机\index{下推自动机}表示，反之亦然。针对某种特定输入的一系列有限的规则，对不同的输入元素，自动机依据自身的状态会做出不同的响应，最后达到某种特定的状态。
|
||||
|
||||
\subsection{程序设计语言的语法}
|
||||
|
||||
程序设计语言都有自己的语法，而语法的定义是一系列规则的集合，这些规则的基础就是形式语言，从而保证规则是无二义性的。文法\index{文法}是形式语言中十分重要的基本概念，是描述语言的语法结构的一组形式规则。文法有四种分类，其中最常用的为正则语言\index{正则语言}和上下文无关语言\index{上下文无关语言}。正则语言可以用正规式定义，上下文无关语言可以用上下文无关文法(元素和规则的集合)定义。程序设计语言中的大多数算术表达式可用上下文无关文法\index{上下文无关文法}生成。正则语言是最简单的语言类，是上下文无关语言类的一个真子类。对程序设计语言编写的程序进行分析和处理(编译)时，需要判断对应的句子是否合法，可以通过对应语言的自动机进行判断。自动机是语言的另一种表示方法。其中，正则语言可以转换成有限状态自动机\index{有限状态自动机}、上下文无关语言可转换成下推自动机\index{下推自动机}表示，反之亦然。针对某种特定输入的一系列有限的规则，对不同的输入元素，自动机依据自身的状态会做出不同的响应，最后达到某种特定的状态。
|
||||
|
||||
\subsection{程序设计语言的类型系统}
|
||||
在很多程序设计语言中，变量与数据是带类型的；而类型之间有一定的关联。人们在研究程序设计语言理论时，可以借鉴类型论\index{类型论}(Type theory, 也称“类型理论”)来研究程序设计语言的类型系统\index{类型系统}。类型论是数理逻辑中的一个分支，其中的马丁洛夫类型理论用规则来刻画类型及行为，是程序构造的形式理论。类型理论\index{类型理论}研究的是程序设计语言的类型系统，用于定义如何将编程语言中的数值和表达式等短语归类为许多不同的类型，如何操作这些类型，这些类型如何互相作用。类型通过预测程序部件的某些执行行为来协调这些部件间的交互。在类型化的程序设计语言中，语言构造分为引入和消去两种形式。类型的引入形式确定该类型的值或范型，而消去形式则确定如何操作该类型的值以形成另一种（可能是相同的）类型的计算。例如，可以使用类型系统中的归纳类型定义如自然数、表、树等数据结构\index{数据结构}；使用多态类型处理程序的特定型与参数型这些不同的输入类型；使用记录类型定义一组记录的命名类型等；自然数类型的引入形式是自然数，消去形式是加法和乘法等。
|
||||
|
||||
在很多程序设计语言中，变量与数据是带类型的；而类型之间有一定的关联。人们在研究程序设计语言理论时，可以借鉴类型论\index{类型论}(Type theory, 也称“类型理论”)来研究程序设计语言的类型系统\index{类型系统}。类型论是数理逻辑中的一个分支，其中的马丁洛夫类型理论用规则来刻画类型及行为，是程序构造的形式理论。类型理论\index{类型理论}用于定义如何将编程语言中的数值和表达式等短语归类为许多不同的类型，如何操作这些类型，这些类型如何互相作用。类型通过预测程序部件的某些执行行为来协调这些部件间的交互。在类型化的程序设计语言中，语言构造分为引入和消去两种形式。类型的引入形式确定该类型的值或范式，而消去形式则确定如何操作该类型的值以形成另一种（可能是相同的）类型的计算。例如，
|
||||
%可以使用类型系统中的归纳类型定义如自然数、表、树等数据结构\index{数据结构}；使用多态类型处理程序的特定型与参数型这些不同的输入类型；使用记录类型定义一组记录的命名类型等；
|
||||
自然数类型的引入形式是自然数，消去形式是加法和乘法等。
|
||||
|
||||
\subsection{程序的语义}
|
||||
给定一个程序，如何判断它是否正确？这是很早以前人们就关注的问题。简单来说，如果一个程序恰当地实现了设计者与用户的意图，它就是正确的。严格意义上，程序的正确性~\cite{turing1989checking}需要数学证明，不仅需要形式描述设计者与用户的意图，而且要形式描述程序的含义，并推导程序的行为满足设计者与用户的意图。程序含义的形式化描述就是形式语义学。基于形式语义，不仅可以构建描述程序含义的基础，还可以用于验证程序的正确性。
|
||||
给定一个程序，如何判断它是否正确？这是很早以前人们就关注的问题。简单来说，如果一个程序恰当地实现了设计者与用户的意图，它就是正确的。严格意义上，程序的正确性~\cite{turing1989checking}需要数学证明，不仅需要形式描述设计者与用户的意图，而且要形式描述程序的含义，并推导程序的行为满足设计者与用户的意图。程序含义的形式化描述就是形式语义。基于形式语义，不仅可以构建描述程序含义的基础，还可以用于验证程序的正确性。
|
||||
|
||||
程序设计语言的语法是符号化的，语义是该语言程序所描述的计算或过程。根据语义，程序设计语言的解释器或编译器可以将该语言程序编译成计算机可处理的机器语言程序。在程序设计语言的早期，人们使用自然语言解释语义。这种自然语言解释的语义不精确、有歧义，无法分析和证明程序的正确性。为了提高程序设计语言的可理解性、支持语言标准化、指导语言设计、辅助编译器开发、证明程序的性质和程序之间的等价性，需要对程序设计语言的语义进行抽象，给出严格的定义。为此，人们开始研究使用数学结构定义程序设计语言的语义，并扩展出各类形式规约(Specification)语言~\cite{Wang2019}，形成了形式语义学\index{形式语义学}~\cite{Zhou2018}。
|
||||
程序设计语言的语法是符号化的，语义是该语言程序所描述的计算或过程。根据语义，程序设计语言的解释器或编译器可以将该语言程序编译成计算机可处理的机器语言程序。在程序设计语言的早期，人们使用自然语言解释语义。这种自然语言解释的语义不精确、有歧义，无法分析和证明程序的正确性。为了提高程序设计语言的可理解性、支持语言标准化、指导语言设计、辅助编译器开发、证明程序的性质和程序之间的特定关系，需要对程序设计语言的语义进行建模，给出严格的定义。为此，人们开始研究使用数学结构定义程序设计语言的语义，并扩展出各类形式规约(Specification)语言~\cite{Wang2019}，形成了形式语义学\index{形式语义学}~\cite{Zhou2018}。
|
||||
它的基本方法是用一种元语言将程序加工数据的过程及其结果形式化，从而定义程序的语义。根据所用数学工具和研究重点，形式语义学可分为操作语义、公理语义、代数语义和指称语义四大类。
|
||||
|
||||
\begin{itemize}
|
||||
\item 操作语义
|
||||
\end{itemize}
|
||||
|
||||
操作语义(Operational Semantics)\index{操作语义}使用结构化的归约规则，着重描述程序运行中变量赋值的变化、行为的变迁。它将语言中各个成分翻译成计算机系统中相应的一组操作。目前最为常见的操作语义是标号迁移系统\index{标号迁移系统}(Labeled Transition System，LTS)，将程序执行描述成标号迁移系统，其中的状态是程序执行期间任意时刻观察到的变量取值。迁移规则规定如何从一个状态转换到下一个状态，每条迁移规则对应一个语句，称为标号。一条语句的语义由一组以其为标号的规则定义；标号规则具有组合性，即一个复合语句的规则可以由其成分语句的规则组合而成。例如，针对一个C程序中的循环语句while(x<y) do~\{x++;\}的操作语义为：
|
||||
\lstset{language=C}
|
||||
\begin{lstlisting}
|
||||
loop: if (x>=y) goto out;
|
||||
if (x<y) { x=x+1; goto loop;}
|
||||
out: …
|
||||
\end{lstlisting}
|
||||
其中，loop、out是标号，从loop到loop、loop到out是描述程序执行的迁移系统中的迁移规则。
|
||||
操作语义(Operational Semantics)\index{操作语义}使用结构化的归约规则，着重描述程序运行中变量赋值的变化、行为的变迁。它将语言中各个成分翻译成计算机系统中相应的一组操作。目前最为常见的操作语义是由标号迁移系统\index{标号迁移系统}(Labeled Transition System，LTS)给出，将程序执行描述成标号迁移系统，其中的状态是程序执行期间任意时刻观察到的变量取值。迁移规则规定如何从一个状态转换到下一个状态，每条迁移规则对应一个语句，称为标号。一条语句的语义由一组以其为标号的规则定义；标号规则具有组合性，即一个复合语句的规则可以由其成分语句的规则组合而成。%例如，针对一个C程序中的循环语句while(x<y) do~\{x++;\}的操作语义为：
|
||||
|
||||
%\lstset{language=C}
|
||||
%\begin{lstlisting}
|
||||
% loop: if (x>=y) goto out;
|
||||
% if (x<y) { x=x+1; goto loop;}
|
||||
% out: …
|
||||
%\end{lstlisting}
|
||||
%其中，loop、out是标号，从loop到loop、loop到out是描述程序执行的迁移系统中的状态转换关系。\note{迁移规则？}
|
||||
|
||||
在由操作语义描述的串行程序的语义中，状态是一些简单的数据结构，迁移规则一般都是确定的、离散的，也不需要考虑标号间的通信和同步。为了定义复杂程序的操作语义，例如面向对象程序、并发程序、实时程序、概率程序\index{概率程序}、混成系统\index{混成系统}等，人们对迁移系统进行了各种扩充，或扩充它的状态，或扩充它的迁移关系，亦或两者同时扩充。例如，为了定义面向对象程序，人们对程序状态进行扩充，引入堆和栈等复杂数据结构；为了处理并发程序，人们对标号迁移关系进行扩充，使用标号描述通信和同步；为了描述概率和随机程序\index{随机程序}，允许以给定的概率或者随机选取迁移规则等。
|
||||
|
||||
基于抽象机的操作语义可描述实现方面的执行细节，操作性比较强，适合于语言编译器的开发与编译的优化。操作语义中的状态是显式的、可操作的。因此，在基于状态搜索的模型检验\index{模型检验}方法中，操作语义比较适合描述模型的语义，即状态的变化序列。然而，抽象机上的推理系统比较弱，不易对大规模或无穷状态的系统进行基于演绎推理\index{演绎推理}的形式验证。
|
||||
基于抽象机的操作语义易于描述实现方面的执行细节，操作性比较强，适合于语言编译器的开发与编译的优化。此外，操作语义中的状态是显式的、可操作的。在基于状态搜索的模型检验\index{模型检验}方法中，操作语义比较适合描述模型的语义，即状态的变化序列。然而，抽象机上的推理系统比较弱，不易对大规模或无穷状态的系统进行基于演绎推理\index{演绎推理}的形式验证。
|
||||
|
||||
\begin{itemize}
|
||||
\item 公理语义
|
||||
|
|
@ -181,12 +215,13 @@
|
|||
|
||||
公理语义(Axiomatic Semantics)\index{公理语义}运用数学中的公理化方法给出计算机语言的语义。
|
||||
%程序的语义不仅可以使用操作语义描述，还可以使用形式逻辑来描述。而形式逻辑是公理语义(axiomatic semantics)的基础。公理语义直接使用形式逻辑来描述程序的语义，在已有的形式逻辑系统基础上增加所有程序必须满足的基本命题(程序公理)。
|
||||
动态逻辑\index{动态逻辑}、模态逻辑\index{模态逻辑}、时序逻辑\index{时序逻辑}等可以用来作为定义程序公理语义的形式系统。每个程序的基本语句都有一组公理和推理规则，它们与断言逻辑一起构成程序逻辑的证明系统。例如，
|
||||
对于顺序语句$s_1;s_2$，若其中变量的值在$s_1$执行前满足断言$R$，$s_1$与$s_2$执行完毕后变量的值满足断言$T$，那么可以找到两个语句执行中间结果的断言$Q$，使得若$R$为$s_1$的前置断言，则$Q$为$s_1$的后置断言，而且以$Q$为$s_2$的前置断言，则$T$就是$s_2$的后置断言。这样就可以采用推理规则
|
||||
\[
|
||||
\frac{\{R\}s_1\{Q\}, \{Q\}s_2\{T\}}{\{R\}(s_1;s_2)\{T\}}
|
||||
\]
|
||||
来规定顺序语句的语义。该推理规则表示当横向上方的命题都成立时，则横线下方的命题也成立。
|
||||
动态逻辑\index{动态逻辑}、模态逻辑\index{模态逻辑}、时序逻辑\index{时序逻辑}等可以用来作为定义程序公理语义的形式系统。每个程序的基本语句都有一组公理和推理规则，它们与断言逻辑一起构成程序逻辑的证明系统。
|
||||
|
||||
%例如，对于顺序语句$s_1;s_2$，若其中变量的值在$s_1$执行前满足断言$R$，$s_1$与$s_2$执行完毕后变量的值满足断言$T$，那么可以找到两个语句执行中间结果的断言$Q$，使得若$R$为$s_1$的前置断言，则$Q$为$s_1$的后置断言，而且以$Q$为$s_2$的前置断言，则$T$就是$s_2$的后置断言。这样就可以采用推理规则
|
||||
%\[
|
||||
%\frac{\{R\}s_1\{Q\}, \{Q\}s_2\{T\}}{\{R\}(s_1;s_2)\{T\}}
|
||||
%\]
|
||||
%来规定顺序语句的语义。该推理规则表示当横向上方的命题都成立时，则横线下方的命题也成立。
|
||||
%若条件语句if(y==1) then x=1; else x=2; 的前置断言为\{y==1\}，则该语句执行后，后置断言为\{x==1\}。
|
||||
在该形式系统中可以直接进行程序性质的规约和验证。程序逻辑的表达能力、可靠性、完备性以及可判定性都可归结为数理逻辑上的元性质，程序逻辑的解释模型通常就是程序设计语言的指称语义或操作语义。
|
||||
常见的公理语义有基于一阶逻辑\index{一阶逻辑}扩展的Floyd-Hoare 逻辑\index{Floyd-Hoare 逻辑}~\cite{Hoare1969}、谓词转换器(Predicate Transformer)等。其中，
|
||||
|
|
@ -196,9 +231,9 @@ Floyd-Hoare 逻辑最初是面向串行程序\index{串行程序}的，并扩展
|
|||
\item 代数语义
|
||||
\end{itemize}
|
||||
|
||||
面向对象程序设计语言具有抽象数据类型、多态性等特点。在抽象数据类型的基础上发展起来的代数语义(Algebraic Semantics)\index{代数语义}，用代数方法研究计算机语言的语义。它把程序设计语言形式地定义为满足某种公理体系的抽象代数结构，然后利用这种代数结构的性质来证明用该语言编写的程序的正确性。
|
||||
面向对象程序设计语言具有抽象数据类型、多态性等特点。在抽象数据类型的基础上发展起来的代数语义(Algebraic Semantics)\index{代数语义}，是用代数方法研究计算机语言的语义。它把程序设计语言形式地定义为满足某种公理体系的抽象代数结构，然后利用这种代数结构的性质来证明用该语言编写的程序的正确性。
|
||||
|
||||
抽象数据类型\index{抽象数据类型}将数据对象及对象上的操作封装、数据类型的特性与实现分离，具有模块化和可复用的性质。它与软件开发过程匹配比较自然，因此也可以用于程序的自动构造：首先设计较小的抽象数据类型，然后逐步扩充形成较大的抽象数据类型体系；这个过程中，抽象数据类型间可讨论层次一致和充分完备等性质。
|
||||
抽象数据类型\index{抽象数据类型}将数据对象及对象上的操作封装、数据类型的特性与实现分离，具有模块化和可复用的性质。它与软件开发过程匹配比较自然，多用于程序精化与构造。
|
||||
|
||||
\begin{itemize}
|
||||
\item 指称语义
|
||||
|
|
@ -214,9 +249,9 @@ Floyd-Hoare 逻辑最初是面向串行程序\index{串行程序}的，并扩展
|
|||
直接使用程序设计语言及其语义，难以描述和证明软件从需求文档到程序代码的开发过程各阶段创建的不同抽象层次的制品及其正确性。针对这一问题，人们开始研究高层抽象的形式规约语言的设计。形式规约语言\index{形式规约语言}是指由严格的递归语法规则所定义的语言，满足语法规则的句子称为合式或良构(Well-formed)规约。
|
||||
|
||||
|
||||
|
||||
串行程序设计早期的程序逻辑是Floyd-Hoare逻辑。通过在一阶谓词系统基础上添加关于程序的公理和推理规则，构成了Floyd-Hoare 逻辑的推理系统。类似的规约语言还有Dijkstra 的卫式命令语言(Guarded Command Language)的最弱前置断言演算。然而，早期的基于Floyd-Hoare 逻辑的推理系统无法描述带指针和内存数据结构的程序规约，也无法描述并发程序的规约。分离逻辑是对Floyd-Hoare 逻辑的扩展，以支持带有指针和内存数据结构的程序的验证。分离逻辑最大的特点是对内存和数据结构的抽象描述，能够更方便、更模块化地支持类似C程序的指针程序的验证。它在断言语言中引入方便描述内存使用和分离特性的分离合取和分离蕴含谓词，并在规则中将Floyd-Hoare 逻辑的不变式\index{不变式}(Invariance)规则替换为框架(Frame)规则。
|
||||
并发程序的规约在Floyd-Hoare 逻辑的基础上，引入了行为轨迹的变量或不变式。与分离逻辑类似，并发分离逻辑也支持并发程序验证。后续有大量工作对并发分离逻辑进行扩充，例如将Rely-Guarantee 和并发分离逻辑结合，从而支持细粒度并发或者无锁并发程序的规约和验证。%除了这些针对串行一致性内存模型上的并发程序的程序逻辑外，还有一些工作对并发分离逻辑进行扩展，以支持弱内存模型（如C11）下的并发程序的正确性分析。
|
||||
串行程序设计早期的程序逻辑是Floyd-Hoare逻辑。通过在一阶谓词系统基础上添加关于程序的公理和推理规则，构成了Floyd-Hoare 逻辑的推理系统。类似的规约语言还有Dijkstra 的卫式命令语言(Guarded Command Language)的最弱前置断言演算。然而，早期的基于Floyd-Hoare 逻辑的推理系统无法描述带指针和内存数据结构的程序规约，也无法描述并发程序的规约。分离逻辑是对Floyd-Hoare 逻辑的扩展，以支持带有指针和内存数据结构的程序的验证。
|
||||
%分离逻辑最大的特点是对内存和数据结构的抽象描述，能够更方便、更模块化地支持类似C程序的指针程序的验证。%它在断言语言中引入方便描述内存使用和分离特性的分离合取和分离蕴含谓词，并在规则中将Floyd-Hoare 逻辑的不变式\index{不变式}(Invariance)规则替换为框架(Frame)规则。
|
||||
并发程序的规约在Floyd-Hoare 逻辑的基础上，引入了行为轨迹的变量或不变式。并发分离逻辑也支持并发程序验证。%后续有大量工作对并发分离逻辑进行扩充，例如将Rely-Guarantee 和并发分离逻辑结合，从而支持细粒度并发或者无锁并发程序的规约和验证。%除了这些针对串行一致性内存模型上的并发程序的程序逻辑外，还有一些工作对并发分离逻辑进行扩展，以支持弱内存模型（如C11）下的并发程序的正确性分析。
|
||||
|
||||
Floyd-Hoare逻辑中，程序与断言是分离的，而且也无法表达活性。针对这些不足，相继出现了基于模态逻辑的动态逻辑、基于动态逻辑的模态$\mu$-演算。作为模态$\mu$-演算的真子集，由Amir Pnueli提出的线性时序逻辑(LTL)和 Edmund M. Clarke与E. Allen Emerson提出的计算树逻辑(CTL)是并发系统规约和验证的常用语言。除了这些经典的逻辑，还有用于数理逻辑计算和并发系统正确性验证的动作时序逻辑(TLA)、用于有限序列中命题与一阶逻辑推理的区间时序逻辑(ITL)。为了处理一些非功能性质，还出现了各种扩充，如度量时序逻辑(MTL)、时段演算(DC)等。
|
||||
|
||||
|
|
@ -236,11 +271,11 @@ Floyd-Hoare逻辑中，程序与断言是分离的，而且也无法表达活性
|
|||
\begin{figure}[htbp]
|
||||
\centering
|
||||
\includegraphics[width=0.50\textwidth]{fig1-2/2-3.png}
|
||||
\caption{程序的形式化分析方法
|
||||
\caption{程序的正确性构造方法
|
||||
\label{fig:2-3}}
|
||||
\end{figure}
|
||||
|
||||
\subsection{程序的分析与验证}
|
||||
\subsection{程序验证}
|
||||
定理证明（Theorem Proving）、模型检验（Model Checking）是形式化验证的两种主要方法。%，并逐渐被IT产业界所接受和采纳。例如，形式化验证工具如Z3、SLAM等用于分析软件的正确性；将基于分离逻辑的验证工具Infer用于Android应用的开发过程中；使用SMT求解器去验证Web服务的正确性；使用定理证明辅助工具来验证操作系统内核的正确性和安全性。
|
||||
|
||||
\begin{itemize}
|
||||
|
|
@ -252,9 +287,9 @@ Floyd-Hoare逻辑中，程序与断言是分离的，而且也无法表达活性
|
|||
|
||||
对串行程序进行验证，可以通过一组与程序设计语言语句对应的Floyd-Hoare逻辑公理和规则，将对程序的验证转化为一组数学命题的证明。对这种逻辑进行扩展，可以进一步证明并发程序的正确性。我们可以通过描述并发任务的无干扰性(Non-interference) 、并发任务间接口的抽象，实现并发程序的验证。%另一个方面的工作使用关系型程序逻辑验证两个程序之间的关系，或者一个程序在两种输入下的行为之间的关系。前者可用于程序精化的验证，而后者则可用于信息安全性质，如信息流控制(information flow control)机制的验证。
|
||||
|
||||
基于定理证明的验证工具可以分为两类，即基于自动定理证明器的自动验证和基于人机交互的半自动验证。常见的程序自动证明器(Program Verifier)，如Dafny、Why3、VeriFast、Smallfoot等，大多都基于某种具体的程序逻辑。给定程序及其规约，证明器能够自动决定针对程序的每条语句使用程序逻辑中的何种公理或规则，并产生相应的验证断言作为证明义务。最终，由定理证明器完成对验证断言的证明。目前常见的证明器包括Z3、CVC4、Yices 2等。交互式的半自动验证工具，如Coq和Isabelle/HOL等，利用类型系统和逻辑之间的Curry-Howard同构关系，将构造证明的过程转化为编写程序的过程，而证明的正确性检查也变成了类型检查问题。这种方法的优点在于无需牺牲规约和代码的表达能力，程序规约可以用表达能力很强的逻辑(如在Coq 和Isabelle/HOL 中使用的高阶逻辑)来表示。而且证明自身在机器中有显式表示，其正确性可以被自动检查，因此无需依赖自动定理证明算法的正确性，验证的结论也就更加可信。
|
||||
基于定理证明的验证工具可以分为两类，即基于自动定理证明器的自动验证和基于人机交互的半自动验证。常见的程序自动证明器(Program Verifier)，如Dafny、Why3、VeriFast、Smallfoot等，大多都基于某种具体的程序逻辑。给定程序及其规约，证明器能够自动决定针对程序的每条语句使用程序逻辑中的何种公理或规则，并产生相应的验证断言作为证明义务。最终，由定理证明器完成对验证断言的证明。目前常见的自动证明器包括Z3、CVC4、Yices 2等。交互式的半自动验证工具，如Coq和Isabelle/HOL等，利用类型系统和逻辑之间的Curry-Howard同构关系，将构造证明的过程转化为编写程序的过程，而证明的正确性检查也变成了类型检查问题。这种方法的优点在于无需牺牲规约和代码的表达能力，程序规约可以用表达能力很强的逻辑(如在Coq 和Isabelle/HOL 中使用的高阶逻辑)来表示。而且证明自身在机器中有显式表示，其正确性可以被自动检查，因此无需依赖自动定理证明算法的正确性，验证的结论也就更加可信。
|
||||
|
||||
近期提出的K框架提供了基于重写的语言~\cite{Rosu15}，用于定义编程语言的正式操作语义。K语言的语义是可执行的。结合K语言语义及相应的逻辑推理过程，可以分析和验证各种程序，而无需为语言提供任何其他语言（公理或指称或动态等）语义。
|
||||
近期提出的K框架提供了基于重写的语言~\cite{Rosu15}，用于定义程序设计语言的操作语义。结合K语言语义及相应的逻辑推理过程，可以在统一的框架中分析和验证各种程序设计语言编写的程序。
|
||||
|
||||
目前，形式验证方法已经应用于一些大型软件。例如，微内核操作系统seL4的ARM版本是第一个带有完整代码级的功能正确性证明的通用操作系统内核，可以应用于金融，医疗，汽车，航空电子设备和国防部门。它的验证使用了Isabelle/HOL定理证明，这意味着通过形式化方法证明了实现(用编写C语言)是满足其规约的。再如，对编译器的验证，可以保证程序从编写到产生的可执行代码的正确性。适用于C99编程语言的大部分语法的CompCert就是一个经过正式验证的优化编译器，支持PowerPC、ARM、RISC-V、x86和x86-64架构。
|
||||
|
||||
|
|
@ -264,19 +299,23 @@ Floyd-Hoare逻辑中，程序与断言是分离的，而且也无法表达活性
|
|||
\end{itemize}
|
||||
|
||||
%由Edmund M. Clarke、E. Allen Emerson和Joseph Sifakis提出的
|
||||
模型检验\index{模型检验}方法通过自动遍历系统模型的有穷状态空间，来检验系统的语义模型与其性质规约之间的满足关系。软件系统属于无穷状态系统，即使状态有穷，其状态空间规模通常远超当前计算机可处理的范围。在硬件系统模型检验取得巨大成功的时候，软件模型检验所面临严峻的挑战。对于无穷状态系统，符号化可达性分析可能不终止。软件模型检验的核心问题是如何建立可检验规模的软件模型(抽象)。一种方法是采用上近似(Over-approximation或下近似(Under-approximation)对模型进行抽象，另一种方法是使用限界模型检验，将模型空间爆炸涉及的参数(例如循环次数、并发数等)限制在一定范围内，验证系统模型在此深度内是否满足系统规约。在软件模型检验中，利用静态分析、符号执行\index{符号执行}等方法抽取程序模型，以及基于路径的模型检验等静态和动态结合的方法，也是有效提高模型检验扩展性的重要途径。%近年来，将模型检验与定理证明有效地结合也是一个有前景的研究方向。
|
||||
模型检验\index{模型检验}方法通过自动遍历系统模型的有穷状态空间，来检验系统的语义模型与其性质规约之间的满足关系。软件系统属于无穷状态系统，即使状态有穷，其状态空间规模通常远超当前计算机可处理的范围。在硬件系统模型检验取得巨大成功的时候，软件模型检验所面临严峻的挑战。对于无穷状态系统，符号化可达性分析可能不终止。软件模型检验的核心问题是如何建立可检验规模的软件模型(抽象)。一种方法是采用保守近似对模型进行抽象，另一种方法是使用限界模型检验，将模型空间爆炸涉及的参数(例如循环次数、并发数等)限制在一定范围内，验证系统模型在此深度内是否满足系统规约。在软件模型检验中，利用静态分析、符号执行\index{符号执行}等方法抽取程序模型，以及基于路径的模型检验等静态和动态结合的方法，也是有效提高模型检验扩展性的重要途径。%近年来，将模型检验与定理证明有效地结合也是一个有前景的研究方向。
|
||||
|
||||
\subsection{程序的自动综合}
|
||||
按照某种形式规约表达的用户意图，程序综合\index{程序综合}能够使用指定的编程语言自动生成符合规约的程序代码。程序综成器通常在程序空间上执行某种形式的搜索，以生成与各种类型一致的程序约束(例如输入输出示例，演示，自然语言，部分程序和断言)。程序综合是编程理论中最核心的问题之一~\cite{pnueli1989synthesis}。早期的想法是通过组合子问题生成带有证明的、可解释的实现。一个分支是使用定理证明器首先证明用户提供的规约，再使用这个证明提取相应的程序逻辑。而另一个较为流行的方法是从一个高层规约开始，不断的进行转换，直到实现目标程序。近期的程序综合方法中，用户提供规约的同时，还可以提供目标程序的语法。这样使得基于语法结构进行的综合过程更加高效，得到的程序的可解释性更高。
|
||||
按照某种形式规约表达的用户意图，程序综合\index{程序综合}能够使用指定的编程语言自动生成符合规约的程序代码。程序综成器通常在程序空间上执行某种形式的搜索，以生成与各种类型一致的程序约束(例如输入输出示例，演示，自然语言，部分程序和断言)。程序综合是编程理论中最核心的问题之一~\cite{pnueli1989synthesis}。早期的想法是通过组合子问题生成带有证明的、可解释的实现。一个分支是使用定理证明器首先证明用户提供的规约，再使用这个证明提取相应的程序逻辑。而另一个较为流行的方法是从一个高层规约开始，不断的进行转换，直到实现目标程序。近期的程序综合方法中，用户提供规约的同时，还可以提供目标程序的语法框架。这样使得基于语法结构进行的综合过程更加高效，得到的程序的可解释性更高。
|
||||
|
||||
\subsection{程序的精化}
|
||||
程序精化\index{程序精化}是将抽象（高级）形式规范可验证地转换为具体（低级）可执行程序的过程，是通过逐步细化分阶段完成。精化（Refinement）是一种数学表示法和若干规则的集合，它对Dijkstra的卫式命令语言进行扩充，通过结合规约语句、精化规则和语言本身，从程序规约推导出命令式程序。程序精化(程序规约转换成可执行代码)可分为数据精化和算法精化两种，形式化将程序逐步转换为更加便于实现的形式：数据精化把抽象的数据结构转换为可以高效实现的形式；算法精化将程序逐步转换为更加便于实现的代码形式。
|
||||
程序精化\index{程序精化}是将抽象（高级）形式规范可验证地转换为具体（低级）可执行程序的过程，是通过逐步细化分阶段完成。精化（Refinement）是一种数学表示法和若干规则的集合，它对Dijkstra的卫式命令语言进行扩充，通过结合规约语句、精化规则和语言本身，从程序规约推导出命令式程序。程序精化(程序规约转换成可执行代码)可分为数据精化和算法精化两种，将程序逐步转换为更加便于实现的形式：数据精化把抽象的数据结构转换为可以高效实现的形式；算法精化将程序逐步转换为更加便于实现的代码形式。
|
||||
|
||||
\section{本章小结}
|
||||
开发软件，离不开程序设计语言。
|
||||
开发软件，离不开程序设计语言。随着计算机硬件技术的发展，软件的多样化、需求的复杂化推动了程序设计语言与程序理论的演化与发展。
|
||||
在计算机发展的不同阶段，为了应对一些典型应用，各种不同的程序设计语言应运而生。
|
||||
第一，现阶段，多范型、函数式程序设计语言逐渐成为主流，如Java、C++及新出现的程序设计语言；第二，虽然如JavaScript、Python等语言强调动态类型安全（编译器能够对查询执行语法正确性检查），新出现的语言重新强调静态类型安全（不使用编译器不能保证安全的语言功能）；第三，新出现的语言语法更加简洁，并更加重视语言的可扩充性；同时，轻量级并发程序设计变得越来越普及。同时，为了适应软件的新形态，程序理论也取得了长足的进步。首先，随着新领域的涌现，出现了新的计算模型与语义，例如，描述量子程序设计的理论模型；其次，程序规约的形式随着需求的发展日益复杂；再次，待验证程序的类型表现出多元化特征，从简单的串行程序到并发、分布式；最后，可验证程序规模日益增加，从简单的驱动程序，到编译器，甚至是操作系统层次。
|
||||
正是由于在程序设计语言和相关理论领域的先驱工作，目前已经有23位研究人员获得了图灵奖。
|
||||
第一，同时支持面向对象编程和函数式编程的多范式程序设计语言逐渐成为主流；
|
||||
不仅经典面向对象语言JAVA和C++中加入了函数式编程风格的支持，新流行的语言如Swift、Kotlin也均支持多范式编程。第二，虽然JavaScript、Python 等动态类型的脚本语言大行其道，深受欢迎，新出现的语言
|
||||
（如Swift，Typescript等）重新强调静态类型安全，无需执行程序就能通过类型检查来发现程序中的类型错误，体现了开发者对程序安全和开发大型软件项目的能力的重视。第三，现代语言更加强调语法简洁，同时强调语言的可扩充性，重视领域专用语言、特别是内嵌式领域专用语言的开发（eDSL）。
|
||||
|
||||
同时，为了适应软件的新形态，程序理论也取得了长足的进步。首先，随着新领域的涌现，出现了新的计算模型与语义，例如，描述量子程序设计的理论模型；其次，程序规约的形式随着需求的发展日益复杂；再次，待验证程序的类型表现出多元化特征，从简单的串行程序到并发、分布式；最后，可验证程序规模日益增加，从简单的驱动程序，到编译器，甚至是操作系统层次。
|
||||
正是由于在程序设计语言和相关理论领域的先驱工作，目前已经有23位著名学者获得了图灵奖。
|
||||
|
||||
%\section{参考文献}
|
||||
%
|
||||
|
|
|
|||
|
|
@ -1,18 +1,18 @@
|
|||
% !TEX root = main.tex
|
||||
|
||||
任何一个学科的发展都需要基础理论作为支撑。涵盖计算理论与程序理论的软件理论是软件学科的基础。重要的理论结果和方法也有助于实际软件开发。信息技术的快速发展推动了整个社会的信息化程度不断提高。软件作为重要的基础设施之一，需要不断提高其品质。著名软件工程师Laurence Peter Deutsch \cite{Deutsch99}给学生的建议包括：“Good software requires the ability to think formally (mathematically),…Make sure you have some exposure to assertions, proofs, and analysis of algorithms, …”，也就是说，高质量的软件需要进行一定的形式化（数学）分析，确保算法的正确性。
|
||||
任何一个学科的发展都需要基础理论作为支撑。涵盖计算理论与程序理论的软件理论是软件学科的基础。重要的理论结果和方法也有助于实际软件开发。信息技术的快速发展推动了整个社会的信息化程度不断提高。软件作为重要的基础设施之一，需要不断提高其品质。著名软件工程师Laurence Peter Deutsch \cite{Deutsch99}给学生的建议包括：“Good software requires the ability to think formally (mathematically),…Make sure you have some exposure to assertions, proofs, and analysis of algorithms, …”，也就是说，高质量的软件需要进行一定的形式化（数学）分析，以确保算法的效率和正确性。
|
||||
|
||||
|
||||
在满足实际需求的过程中，理论本身不断完善。随着软件应用需求和场景的持续发展和丰富、软件运行环境和硬件平台的不断变革、以及软件基础性地位的日益提升，软件理论有着更为广阔的应用前景和发展机遇，但同时也面临巨大的挑战。最近十余年，物联网\index{物联网}、大数据、人工智能等信息领域技术浪潮不断兴起，对计算和程序理论提出了一系列新的需求和挑战。
|
||||
在满足实际需求的过程中，理论本身不断完善。随着软件应用需求和场景的持续发展和丰富、软件运行环境和硬件平台的不断变革以及软件基础性地位的日益提升，软件理论有着更为广阔的应用前景和发展机遇，但同时也面临巨大的挑战。最近十余年，物联网\index{物联网}、大数据、人工智能等信息领域技术浪潮不断兴起，对计算和程序理论提出了一系列新的需求和挑战。
|
||||
|
||||
|
||||
首先，新型的软件应用需求和场景为软件理论带来挑战。大数据应用需要新型算法和复杂性理论\index{复杂性理论}支持海量数据的高效处理；云计算的发展需要新型的分布式计算理论\index{计算理论}以及新型的编程模型；人工智能的发展使得具有不确定性的知识表示和推理成为一种常规的思维方式，从而为算法和复杂性理论、编程模型、以及软件的可靠性分析\index{软件可靠性}等带来众多问题；信息物理融合系统（CPS）\index{信息物理融合系统}和物联网应用则使得既有离散事件又有连续状态变化的混成系统系统\index{混成系统系统}的建模、分析和验证成为难以回避的挑战。
|
||||
首先，新型的软件应用需求和场景为软件理论带来挑战。大数据应用需要新型算法和复杂性理论\index{复杂性理论}支持海量数据的高效处理\cite{chen2014data}；云端计算的发展需要新型的分布式计算理论\index{计算理论}以及新型的编程模型；人工智能的发展使得具有不确定性的知识表示和推理成为一种常规的思维方式，从而给算法和复杂性理论、编程模型以及软件的可靠性分析\index{软件可靠性}等带来众多问题\cite{arpteg2018software}；信息物理融合系统（CPS）\index{信息物理融合系统}和物联网应用则使得既有离散事件又有连续状态变化的混成系统\index{混成系统系统}的建模、分析和验证成为难以回避的挑战\cite{lunze2009handbook}。
|
||||
|
||||
|
||||
其次，软件运行环境和硬件平台的变革为软件理论带来机遇和挑战。一方面，处理器能力和网络带宽的大幅提升，使得以往受限于计算或通信能力的技术变得更具有实用性，包括特定的编程模型以及程序的自动化分析和验证技术，从而为软件理论的发展带来新的驱动力。另一方面，运行环境和硬件平台的变革也带来巨大挑战：人、机、物的融合使得软件运行在具有高度动态化和不确定性的环境中，为软件的规约、建模、分析和验证带来困难；多核处理器的普及促进了并发程序的使用，但对于高效并发算法的验证缺少理论和工具支持；其他挑战还包括搭载异构芯片的处理器、云平台上数据一致性的形式化规约和验证等。
|
||||
其次，软件运行环境和硬件平台的变革为软件理论带来挑战。一方面，处理器能力和网络带宽的大幅提升，使得以往受限于计算或通信能力的技术变得更具有实用性，包括：特定的编程模型以及程序的自动化分析和验证技术，从而为软件理论的发展带来新的驱动力。另一方面，硬件平台和运行环境的变革也带来巨大挑战，为软件的规约、建模、分析和验证带来困难，包括：多核处理器的普及促进了并发程序的使用，但对于高效并发算法的验证缺少理论和工具支持\cite{herlihy2011art}；其他还包括：搭载异构芯片的处理器、云平台上数据一致性的形式化规约和验证等。
|
||||
|
||||
|
||||
其三，软件基础性地位的提升为软件理论带来挑战。软件作为基础设施，日益深入到我们生产生活的方方面面，相应地，对软件可靠性的要求也变得越来越强。人们开始期望那些在以往仅仅针对特定算法和协议的验证技术能够应用于代码级的完整系统验证上，特别是底层系统软件的验证，如操作系统内核、编译器\index{编译器}、密码算法和协议实现等。信息物理融合系统\index{信息物理融合系统}以及基于学习的人工智能技术在自动驾驶等安全攸关系统中的应用使得混成系统和概率系统的形式验证需求越发迫切。同时，软件复杂度的提高，对于可信软件的自动化开发和验证技术也提出了更高的要求。
|
||||
其三，软件基础性地位的提升为软件理论带来挑战。软件作为基础设施，日益深入到我们生产生活的方方面面，相应地，对软件可靠性的要求也变得越来越强。人们开始期望那些在以往仅仅针对特定算法和协议的验证技术能够应用于代码级的完整的全栈系统验证上，特别是底层系统软件的验证，如操作系统内核、编译器\index{编译器}、密码算法和协议实现等\cite{sewell2013translation}。基于学习的人工智能技术在自动驾驶等安全攸关系统中的应用使得混成系统和概率系统的形式验证需求越发迫切\cite{koopman2017autonomous}。同时，软件复杂度的提高，对于可信软件的自动化开发和验证技术也提出了更高的要求。
|
||||
|
||||
|
||||
本章将针对软件理论的核心内容，包括算法及复杂性理论、程序正确性理论等，逐一探讨其面临的挑战，以及将来需要开展的研究。
|
||||
|
|
@ -25,66 +25,66 @@
|
|||
\subsection{面向数据科学的算法与计算复杂性理论}\label{sec:st-complexity}
|
||||
构建高效的软件系统，需要发展算法设计与分析技术；确保算法的性能、理解计算的本质与界限，需要发展相应的计算复杂性理论。算法与计算复杂性理论，就是在这一背景与宗旨下发展形成的，是软件科学乃至计算机科学的根基。随着现代计算机科学进入大数据时代，建立在多项式时间图灵机和最坏情况复杂度分析基础上的传统算法与计算复杂性理论，在计算模型、问题模型和解决标准上，都面临新的挑战。
|
||||
|
||||
在计算模型方面，面向大规模的实时动态输入数据，多项式时间图灵机这一传统计算模型已难以用来刻画高效计算。面向大数据的计算，往往需考虑并行、分布式、低通信、在线计算、动态输入、局部计算等多种计算模型上的约束。因此需面向这些约束，建立新的计算模型。并在新模型上系统地发展相应的算法设计与分析的新范式，以及包含复杂性下界与分类在内的新的计算复杂性理论。
|
||||
在计算模型方面，面向大规模的实时动态输入数据，多项式时间图灵机这一传统计算模型已难以用来刻画高效计算。面向大数据的计算，往往需考虑并行、分布式、低通信、在线计算、动态输入、局部计算等多种计算模型上的约束。因此需面向这些约束，建立新的计算模型，并在新模型上系统地发展相应的算法设计与分析的新范式，以及包含复杂性下界与分类在内的新的计算复杂性理论。
|
||||
|
||||
在问题模型方面，随着数据科学的发展，计算的重心逐步由判定、求解、组合优化等关注单个解的传统计算问题转移到推断、学习、统计、采样、度量等关注整个解空间宏观特性的以数据科学为导向的新型计算问题。为这些非传统计算问题提供高效算法，需要发展新的算法设计与分析技术；理解其计算复杂性的变化规律，需要发展“计算相变”等计算复杂性理论。
|
||||
|
||||
在解决标准方面，面向大数据的计算很多情况下是针对特定分布的真实数据，且往往可以容忍各种形式的近似，因此基于最坏情况复杂度分析的传统已不再适用，需发展数据依赖的算法设计和参数复杂性等非最坏情况复杂性分析，并允许随机与近似计算。另一方面，大数据计算对计算的开销的限制却更加苛刻，因此需发展亚线性时间开销算法、以及精细计算复杂性理论。同时，现实大数据的计算场景还需顾及到隐私、公平、容错等额外的约束，对何为一个计算问题的“解决”有更加丰富的要求。这都需要发展相应的算法设计与分析技术以及计算复杂性理论。
|
||||
在实际的软件系统中，上述挑战往往并非单独出现，而是以多种组合形式出现的。因此，不同于算法与计算复杂性理论中很多情况下“一题一议”的特点，需要更加注重发展通用算法技术，研究基本算法原语及其复杂性。发展适应大数据时代的更加“鲁棒”的算法与计算复杂性理论。
|
||||
在解决标准方面，面向大数据的计算很多情况下是针对特定分布的真实数据，且往往可以容忍各种形式的近似，因此基于最坏情况复杂度分析的传统已不再适用，需发展数据依赖的算法设计和参数复杂性等非最坏情况复杂性分析，并允许随机与近似计算。另一方面，大数据计算对计算的开销的限制却更加苛刻，因此需发展亚线性时间开销算法以及精细计算复杂性理论。同时，现实大数据的计算场景还需顾及到隐私、公平、容错等额外的约束，对何为一个计算问题的“解决”有更加丰富的要求。这都需要发展相应的算法设计与分析技术以及计算复杂性理论。
|
||||
在实际的软件系统中，上述挑战往往并非单独出现，而是以多种组合形式出现的。因此，不同于经典算法与计算复杂性理论中很多情况下“一题一议”的特点，需要更加注重发展通用算法技术，研究基本算法原语及其复杂性，发展适应大数据时代的更加“鲁棒”的算法与计算复杂性理论。
|
||||
|
||||
|
||||
\subsection{复杂系统的可靠性保证}\label{sec:st-reliability}
|
||||
近年来，计算机越来越深入到人们生活中的方方面面，对软件系统可靠性的要求越来越高。另一方面，随着处理器计算能力的增强和形式验证理论与技术的发展，软件验证的能力也在提高。因此，用形式化验证技术来确保复杂系统的可靠性成为一种可行的方案，得到了越来越多的关注和研究，近年来也出现了一些有代表性的优秀成果。
|
||||
近年来，计算机越来越深入到人们生活中的方方面面，对软件系统可靠性的要求越来越高。另一方面，随着处理器计算能力的增强和形式验证理论与技术的发展，软件验证的能力也在提高。因此，用形式化验证技术来确保复杂系统的可靠性得到了越来越多的关注和研究，近年来也出现了一些有代表性的优秀成果。
|
||||
|
||||
|
||||
然而，在软件日益得到广泛应用的同时，其复杂度也在不断增加。软件系统的复杂性主要体现在单点技术特性复杂、系统结构复杂、系统规模庞大等方面。复杂软件系统的验证技术也随之面临重要挑战。在形式化方法中，系统的可靠性或其他安全攸关性质可以通过规约描述，而系统是否满足规约的分析过程依赖于系统的形式化建模、分析和验证。
|
||||
然而，在软件日益得到广泛应用的同时，其复杂度也在不断增加。软件系统的复杂性主要体现在单点技术特性复杂、系统结构复杂、系统规模庞大等方面。复杂软件系统的验证技术也随之面临重要挑战。在形式化方法中，系统的可靠性或其他安全攸关性质可以通过规约描述，而系统是否满足规约的确认过程依赖于系统的形式建模、分析和验证。
|
||||
|
||||
|
||||
复杂系统的可靠性挑战主要体现在以下几个方面：
|
||||
复杂软件系统的可靠性挑战主要体现在以下几个方面：
|
||||
|
||||
|
||||
首先，如何准确表示复杂系统的规约。系统的规约一般通过逻辑公式、集合论等来描述对系统安全性、可靠性、正确性等各方面的需求。系统规约要解决的主要问题是，将各种非形式化表述中使用的关键概念和性质，采用简洁直观又容易被用来推理验证的数学和逻辑语言进行描述。
|
||||
|
||||
|
||||
随着系统复杂性的增加和系统应用场景的多样化，使得需要描述的性质变得更加复杂。例如，信息物理融合系统除了关心功能正确性，还关心非功能相关的性质，包括实时、空间位置等时空特性；机器学习算法和系统的正确性和安全性的研究目前仍处于起步阶段，即便非形式的定义和刻画这些性质仍然是开放性问题，其中一些已经被大家所接受的重要性质，如鲁棒性（Robustness），其性质刻画与经典的程序功能正确性刻画显著不同。在并发系统中，除了线性一致性（Linearizability）这种经典的对并发对象的功能正确性的刻画以外，人们还提出了各种新型的量化松弛算法，它们部分放松了线性一致性的要求，但仍然能够提供一定的正确性保证。这些放松后的保证该如何进行形式化的刻画，是目前面临的关键挑战。与之类似，为了解决云计算中分布式多拷贝数据的一致性问题，并在一致性、可用性、以及系统性能方面取得平衡，人们提出了各种不同强度的数据一致性，包括最终一致性、因果一致性、顺序一致性以及各种变体，还包括多种数据一致性相结合的算法和系统，这些不同的一致性的形式化规约是当前研究的热点问题。在信息安全领域，很多安全特性不是描述程序一次运行的性质，而是要刻画程序多次运行之间的关系，如信息流安全中经典的非干扰性（Non-interference），这一类性质往往被称为“超安全性质”（Hyper-properties），其规约也和经典的功能正确性有所不同。
|
||||
随着系统复杂性的增加和系统应用场景的多样化，使得需要描述的性质变得更加复杂。例如，信息物理融合系统除了关心功能正确性，还关心非功能相关的性质，包括实时、空间位置等时空特性；机器学习算法和系统的正确性和安全性的研究目前仍处于起步阶段，即便非形式的定义和刻画这些性质仍然是开放性问题，其中一些已经被大家所接受的重要性质，如鲁棒性（Robustness），其性质刻画与经典的程序功能正确性刻画显著不同。在并发系统中，除了线性一致性（Linearizability）这种经典的对并发对象的功能正确性的刻画以外，人们还提出了各种新型的量化松弛算法，它们部分放松了线性一致性的要求，但仍然能够提供一定的正确性保证。这些放松后的保证该如何进行形式化的刻画，是目前面临的关键挑战。与之类似，为了解决云计算中分布式多拷贝数据的一致性问题，并在一致性、可用性以及系统性能方面取得平衡，人们提出了各种不同强度的数据一致性，包括最终一致性、因果一致性、顺序一致性以及各种变体，还包括多种数据一致性相结合的算法和系统。这些不同的一致性的形式规约是当前研究的热点问题。在信息安全领域，很多安全特性不是描述程序一次运行的性质，而是要刻画程序多次运行之间的关系，如信息流安全中经典的非干扰性（Non-interference），这一类性质往往被称为“超安全性质”（Hyper-properties），其规约也和经典的功能正确性有所不同。
|
||||
|
||||
|
||||
其次，如何形式化表示复杂软件系统。安全攸关领域的很多系统往往可看成是信息物理融合系统在复杂环境中的运行，不仅兼有离散事件与连续的状态变化，同时计算与控制过程共存。由于系统的非确定性，或克服复杂性而进行的简化，很多都具有概率与随机行为。例如，由于风对飞行器运动的影响，网络控制的系统中消息的丢失及其他随机事件。因此，对随机混成系统的建模、分析与验证是非常困难的。为了实现随机混成系统的分析，可以通过添加概率或随机性对混成自动机进行扩展。然后对随机混成系统的验证转化成通过概率模型检验或统计模型检验进行可达性分析。但是，现有的基于随机混成系统的可达性分析\index{可达性分析}方法仍存在很多不足。
|
||||
其次，如何形式化表示复杂软件系统。安全攸关领域的很多系统往往可看成是信息物理融合系统在复杂环境中的运行，不仅兼有离散事件与连续的状态变化，同时计算与控制过程共存。由于系统的非确定性，或克服复杂性而进行的简化，很多都具有概率与随机行为。例如，风对飞行器运动的影响，网络控制的系统中消息的丢失及其他随机事件。因此，对随机混成系统的建模、分析与验证是必要的，然而却是非常困难的。现有的基于随机混成系统的可达性分析\index{可达性分析}方法仍存在很多不足。
|
||||
|
||||
|
||||
第三，如何保证具有复杂数据结构、算法或协议的系统的可靠性。现有软件系统中含有非常复杂的数据结构、算法和协议等，现有的验证理论难以完全支持。例如，操作系统内核中，为了提高系统效率，往往会使用非常复杂的指针数据结构，其复杂度远远超出双向链表、红黑树等教科书上的经典数据结构。操作系统内核和文件系统中，还会使用很多巧妙的无锁并发算法，其验证一直是形式化验证中的难点。加密算法和协议的验证则需要概率相关的特定验证理论。云计算平台中普遍使用地理上分布的多拷贝数据，其数据一致性算法的验证目前也缺少成熟理论的支持。
|
||||
第三，如何保证具有复杂数据结构、算法或协议的系统的可靠性。对于含有非常复杂的数据结构、算法和协议等软件系统，现有的验证理论难以完全支持。例如，操作系统内核中，为了提高系统效率，往往会使用非常复杂的指针数据结构，其复杂度远远超出双向链表、红黑树等教科书上的经典数据结构。操作系统内核和文件系统中，还会使用很多巧妙的无锁并发算法，其验证一直是形式化验证中的难点。加密算法和协议的验证则需要概率相关的特定验证理论。云计算平台中普遍使用地理上分布的多拷贝数据，其数据一致性算法的验证目前也缺少成熟理论的支持。
|
||||
|
||||
|
||||
第四，如何保证具有复杂体系结构的系统的可靠性。复杂系统往往由大量模块构成，模块之间的组合方式复杂，总体体现为两点：（a）从纵向看，模块之间相互调用，抽象层次不同。一方面，不同抽象层次的代码特性不同，所需要的验证理论和技术也会不尽相同；另一方面，为了实现完整系统的验证，需要将这些不同抽象层次的模块验证后，得出完整系统的可靠性结论。这需要验证技术能够有效集成不同的验证方法、理论和工具，并具有很好的纵向可组合性。（b）从横向看，模块之间有多重组合方式，例如多线程并发、事件驱动等。不同的组合方式导致模块执行的控制流的多样性，这也对系统的模块化验证以及水平方向的可组合性带来挑战。
|
||||
|
||||
|
||||
第五，如何提高软件开发的自动化程度，实现构建即正确的系统。综合(Synthesis)技术可以提高软件的自动化程度。基于演绎的方法可以从高层规范的实现中派生出低层实现；基于归纳的方法可以根据实例的行为，生成满足实例的程序。但状态空间爆炸问题制约了可综合的系统规模。符号化方法、组合式方法可以提高可综合系统的规模，却难以真正投入使用。虽然推理、求解技术的发展与硬件计算能力的提高能一定程度上推动了综合技术的应用，然而，由于可合成系统规模有限，软件的自动化仍缺乏实际应用。
|
||||
第五，如何提高软件开发的自动化程度，实现构建即正确的系统。综合(Synthesis)技术可以提高软件的自动化程度。基于演绎的方法可以从高层规范的实现中派生出低层实现；基于归纳的方法可以根据实例的行为，生成满足实例的程序。但状态空间爆炸问题制约了可综合的系统规模。符号化方法、组合式方法可以提高可综合系统的规模，却难以真正投入使用。虽然推理、求解技术的发展与硬件计算能力的提高能一定程度上推动综合技术的应用，然而，由于可合成系统规模有限，软件的自动化仍缺乏实际应用。
|
||||
|
||||
|
||||
最后，如何验证基于学习技术的复杂系统。机器学习的准确率难以达到百分之百。有必要对使用机器学习的系统鲁棒性进行分析。这种鲁棒性分析首先根据系统使用的神经网络结构构建相应的抽象关系，再基于抽象关系分析输入在一定的扰动下，输出是否会出现分类错误。由于复杂神经网络的神经元个数是百万级别的，而且使用了大量的非线性函数，传统的方法如基于线性规划\index{线性规划}或约束求解\index{约束求解}的方法很难实现对实际系统的分析。基于神经网络中使用的非线性函数的利普希茨(Lipschitz)连续特点对非线性函数进行抽象，或使用多面体(Zonotope)抽象表示神经网络每层的值域可以提高可分析系统的规模，但仍缺乏对实际基于学习系统的验证~\cite{Huang2018}。
|
||||
最后，如何验证基于学习技术的复杂系统。机器学习的准确率难以达到百分之百。有必要对使用机器学习的系统鲁棒性进行分析。这种鲁棒性分析首先根据系统使用的神经网络结构构建相应的抽象关系，再基于抽象关系分析输入在一定的扰动下，输出是否会出现分类错误。由于复杂神经网络的神经元个数是百万级别的，而且使用了大量的非线性函数，传统的方法如基于线性规划\index{线性规划}或约束求解\index{约束求解}的方法很难实现对实际系统的分析。基于神经网络中使用的非线性函数的利普希茨(Lipschitz)连续特点对非线性函数进行抽象，或使用多面体(Zonotope)抽象表示神经网络每层的值域可以提高可分析系统的规模，但仍缺乏对实际基于学习系统的验证~\cite{huang2017}。
|
||||
|
||||
\subsection{新型体系结构和计算平台下的程序语义刻画和正确性保证}\label{sec:st-architecture}
|
||||
近年来，新的体系结构和计算平台大量涌现，包括多核处理器、GPU和异构芯片、分布式云计算平台\index{分布式云计算平台}等。它们对程序设计有各自特定的要求，也对相应的程序验证带来了重要的机遇和挑战。
|
||||
|
||||
|
||||
首先，多处理器架构\index{多处理器架构}对程序本身的内存模型分析与设计带来新的挑战。多核处理器的流行让并发编程由一种高级编程技巧变为一种基本的编程技能~\cite{Herlihy2008}。然而，并发编程自身的困难并未随之消失，特别是经典的共享内存的多任务并发模型及其基于锁的同步机制，为并发程序设计带来了数据竞争\index{数据竞争}、原子性违背\index{原子性违背}、死锁\index{死锁}、活锁\index{活锁}等各种问题。针对这些问题，新的易用、可靠的并发编程模型一度成为研究的热点，提出的新型编程模型包括软件事务型内存（Software Transactional Memory，简称STM）、事件驱动的并发模型、基于消息传递的并发模型等。然而，从易用程度和程序效率的需求看，现有编程模型仍然无法替代经典的共享内存并发模型。并发编程的另一大挑战是内存模型问题。编译器和处理器的优化导致每个并发任务的执行并不是严格按照代码顺序逐条指令运行。虽然这些指令执行顺序的改变不会影响单个任务的串行行为，但会对多任务的程序行为产生影响。相应的，并发程序行为呈现出所谓的弱内存模型。任何一个并发编程语言需要都需要描述其内存模型，然而由于编译器优化的复杂性，为高级语言定义内存模型的工作仍然是一个开放性问题。例如Java和C++现有的内存模型仍然存在各种问题。因此，对这些模型的形式化定义和改善成为当前研究的一大热点。
|
||||
首先，多处理器架构\index{多处理器架构}对程序本身的内存模型分析与设计带来新的挑战。多核处理器的流行让并发编程由一种高级编程技巧变为一种基本的编程技能~\cite{Herlihy2008}。然而，并发编程自身的困难并未随之消失，特别是经典的共享内存的多任务并发模型及其基于锁的同步机制，为并发程序设计带来了数据竞争\index{数据竞争}、原子性违背\index{原子性违背}、死锁\index{死锁}、活锁\index{活锁}等各种问题。针对这些问题，新的易用、可靠的并发编程模型一度成为研究的热点，提出的新型编程模型包括软件事务型内存（Software Transactional Memory，简称STM）、事件驱动的并发模型、基于消息传递的并发模型等。然而，从易用程度和程序效率的需求看，现有编程模型仍然无法替代经典的共享内存并发模型。并发编程的另一大挑战是内存模型问题。编译器和处理器的优化导致每个并发任务的执行并不是严格按照代码顺序逐条指令运行。虽然这些指令执行顺序的改变不会影响单个任务的串行行为，但会对多任务的程序行为产生影响。相应的，并发程序行为呈现出所谓的弱内存模型。任何一个并发编程语言都需要描述其内存模型，然而由于编译器优化的复杂性，为高级语言定义内存模型的工作仍然是一个开放性问题。例如Java和C++现有的内存模型仍然存在各种问题。因此，对这些模型的形式化定义和改善成为当前研究的一大热点。
|
||||
|
||||
|
||||
其次，多处理架构引发了并发程序数据一致性分析的挑战。多核平台中存在多线程并发程序对共享资源的访问冲突。多线程并发程序已经成为现代程序设计的趋势。并发软件应用中的并发数据结构提供支持多线程并发访问。但并发线程的执行存在不确定性,传统的测试方法很难发现这类错误。多核平台下的弱内存模型则使得多线程间数据访问的一致性难以保证。并发数据结构实现的可线性化（或其量化松弛）验证问题已经取得了一定进展，可线性化条件对有界多并发线程是可判定的，但对无界多并发线程是不可判定的。
|
||||
其次，多处理架构引发了并发程序数据一致性分析的挑战。多核平台中存在多线程并发程序对共享资源的访问冲突。多线程并发程序已经成为现代程序设计的常态。并发软件应用中的并发数据结构提供支持多线程并发访问。但并发线程的执行存在不确定性,传统的测试方法很难发现这类错误。多核平台下的弱内存模型则使得多线程间数据访问的一致性难以保证。并发数据结构实现的可线性化（或其量化松弛）验证问题已经取得了一定进展，可线性化条件对有界多并发线程是可判定的，但对无界多并发线程是不可判定的。
|
||||
|
||||
|
||||
最后，新型计算平台引发了分布式系统数据一致性分析的挑战。云计算平台中，为了提高系统的可用性，往往采用地理上分布的多拷贝数据，这也使得系统开发需要面对数据一致性、可用性和对网络分割的容忍性这三者不可兼得的经典问题（即所谓的CAP定理），需要在三者中做出取舍，取得合理折中。考虑到强数据一致性（串行一致性）的实现对效率影响较大，实际系统中往往根据业务特点来适当放松对一致性的保证，这样带来的结果是：一方面系统中可能多种一致性并存，另一方面应用级程序员在使用弱一致性数据的时候，难以保证程序业务的正确性。如何在编程语言和模型中既支持多种一致性，又能简化编程负担，并且对程序的可靠性和正确性给出指导原则和分析验证技术，是当前研究的热点。
|
||||
|
||||
\subsection{新型计算模型下的计算复杂性理论与程序正确性保证}\label{sec:st-quantum}
|
||||
量子硬件设计与制造技术的飞速发展，人们乐观的预测多于一百个量子比特的特定用途的量子计算机有望在5-10 年内实现。量子计算拟充分利用量子力学的两大特性——量子叠加与量子纠缠——来获得潜在的比传统计算性能上的大幅度提升，从而有可能使用量子计算模型来解决经典计算模型中无法高效计算的问题，特别是一些经典困难问题，例如Shor提出的量子整数分解算法可以高效地求解大整数的质因数分解问题，Grover提出的量子搜索算法可以开平方根量级的加速无序数组的查找问题。
|
||||
随着量子硬件设计与制造技术的飞速发展，人们乐观地预测多于一百个量子比特的特定用途的量子计算机有望在5-10 年内实现。量子计算拟充分利用量子力学的两大特性——量子叠加与量子纠缠——来获得潜在的比传统计算性能上的大幅度提升，从而有可能使用量子计算模型来解决经典计算模型中无法高效计算的问题\cite{montanaro2016quantum}，特别是一些经典困难问题，例如Shor提出的量子整数分解算法可以高效地求解大整数的质因数分解问题，Grover提出的量子搜索算法可以开平方根量级的加速无序数组的查找问题。
|
||||
|
||||
量子软件与算法领域最核心的挑战问题仍然是：量子软件与算法能否比经典软件算法在效率上有本质的提升？如果可以提升，那在哪些问题上可以有提升？最多可以提升多大量级？即能否从数学上完全刻画出量子计算能够有效加速的范围及其加速的极限。这对于我们更加深刻的理解计算的本质，特别是计算困难性的起源有着重要的科学意义。同时它还有助于加深我们对于量子力学本质的认识，以及在宏观尺度下量子效应的展示。
|
||||
|
||||
另一个重要的挑战是量子软件和程序该如何进行验证。虽然量子程序的分析与形式化验证领域已经取得了一些可喜的进展，但目前的研究还非常零散，很多问题甚至还不清楚如何准确定义。对于整数分解问题，因其属于NP复杂性类，其结果可以有效地经典验证，但是对一个超出经典计算能力的量子程序，如何才能验证其正确性？例如最近谷歌宣称的“量子优越性”实验。量子密码协议，特别是量子密钥分发协议从理论上具有比经典协议更好的安全性保障，但如何才能够使用经典的方式来验证所设计的量子密码协议的正确性？
|
||||
另一个重要的挑战是量子软件和程序该如何进行验证~\cite{ying2016foundations}。虽然量子程序的分析与形式验证领域已经取得了一些可喜的进展，但目前的研究还非常零散，很多问题甚至还不清楚如何准确定义。对于整数分解问题，因其属于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-quantum})；最后，为了提高新型软件的可靠性，需要研究新型软件的特点，从而给出相应的分析方法(§\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}
|
||||
|
|
@ -98,7 +98,7 @@
|
|||
主要研究内容包括：并行、分布式、低通信、在线、动态输入、局部计算等约束下的算法设计与分析范式；反映出这些约束的大数据计算模型中的计算复杂性下界与分类；推断、学习、统计、采样、度量等数据科学的计算原语，在大数据环境下有理论保证的高效算法与计算复杂性分析；数据依赖的算法设计和参数复杂性等非最坏情况复杂度分析理论；随机化、近似、亚线性计算及其复杂性下界；满足隐私性、公平性、容错性等理论保障的高效算法设计与分析。
|
||||
|
||||
\subsection{形式化方法的理论研究}\label{sec:stc-reliability}
|
||||
一般来说，形式化方法的理论研究内容主要涉及规约、建模、分析与验证方法。其中，规约与建模是系统正确性、可靠性分析的基础，而分析与验证方法是保证系统正确性、可靠性的手段。
|
||||
形式化方法的理论研究内容主要涉及规约、建模、分析与验证方法。其中，规约与建模是系统正确性、可靠性分析的基础，而分析与验证方法是保证系统正确性、可靠性的手段。
|
||||
|
||||
%\begin{itemize}
|
||||
% \item 形式规约
|
||||
|
|
@ -121,7 +121,7 @@
|
|||
% \item 形式建模方法
|
||||
%\end{itemize}
|
||||
|
||||
形式建模的研究包括动态行为建模方法的研究，如支持离散指令与环境连续变化的描述；如何描述静态的系统架构；如何构造结构化的建模方法；如何刻画无穷状态系统的随机、参数化等特征；如何对新型的软件系统进行抽象建模。
|
||||
形式建模的研究包括动态行为建模方法的研究，如支持离散指令与环境连续变化的描述、静态系统架构的描述、结构化的建模方法、无穷状态系统的随机和参数化等特征的刻画、新型软件系统的抽象建模等。
|
||||
|
||||
%形式建模方法用于精确地刻画计算机软硬件系统的行为。如何以数学的形式描述日益复杂的系统结构与行为，用于系统正确性分析，是形式建模研究的核心问题之一。在一些安全关键领域，为了描述和验证系统的安全性，既需要描述离散的机器指令，又需要描述系统所处环境的连续特性。通常，使用混成自动机刻画这类系统。然而，与状态机类似，混成自动机缺乏对结构的描述。因此，出现了很多辅助复杂系统模块化表示的方法。例如，支持混成行为的层次化规范的环境SHIFT、PTOLEMY，描述并发混成行为的I/O自动机、CHARON，描述混成行为的规范HCSP(Hybrid CSP)、描述基于逻辑与组合分析的混成Hoare逻辑HHL(Hybrid Hoare logic)等。工业界常使用Simulink/Stateflow环境实现复杂系统的建模，但它缺乏统一的形式语义。为了对复杂系统的建模，人们还提出了组合建模方法，如HMODEST，随机混成程序。
|
||||
|
||||
|
|
@ -137,27 +137,28 @@
|
|||
%
|
||||
%软件系统的分析与验证的核心问题与挑战是如何缓解大规模复杂系统验证过程中的状态空间爆炸问题，并提高分析的精度与效率。
|
||||
|
||||
形式分析与验证方法主要包括符号执行、抽象解释、定理证明、模型检验等，从不同方法与角度提高分析验证系统的精度与规模。
|
||||
\begin{itemize}
|
||||
\item 基于符号执行的程序分析方法研究集中在增加可分析问题类型、提高可行性、可分析程序规模与算法效率这些方面。在可行性方面的研究基本都是在分析的精确性、可靠性、建模工作量以及可扩展性之间进行权衡和折中。提高可分析程序规模方面的研究包括设立特定的搜索策略、约束输入范围减少程序的路径空间、优化路径条件、或面向特征的高效编码等。面向新的分析需求，也有一些新的符号执行技术出现，其中比较有代表性的是概率符号执行技术。符号执行技术与其他技术之间的紧密融合，以提高分析的效果，也是目前新的发展趋势，包括与模型检验、抽象解释\index{抽象解释}、模糊测试\index{模糊测试}、随机测试\index{随机测试}等的一些技术结合，以提高程序的覆盖率或缺陷发现效率。
|
||||
形式分析与验证方法主要包括符号执行、抽象解释、定理证明、模型检验等，从不同方法与角度提高分析验证系统的精度与规模。基于符号执行的程序分析方法研究集中在增加可分析问题类型、提高可分析程序规模与算法效率这些方面。基于抽象解释的形式验证主要包括提高抽象精度与可行性方面的研究。基于演绎推理的定理证明研究包括如何采用多种策略加速求解过程，如何支撑构造即正确的系统软件开发。基于模型检验的形式验证研究包括使用抽象或符号化等方法减少验证过程中遍历的状态空间规模、计算混成系统的可达集等。此外，还需研究约束求解及解计数技术，特别是可满足性判定（SAT/SMT）方法。
|
||||
|
||||
\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}
|
||||
%\begin{itemize}
|
||||
%\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}
|
||||
|
||||
|
||||
\subsection{新型体系结构和计算平台下的程序理论}\label{sec:stc-architecture}
|
||||
为了应对新涌现的体系结构与计算平台，软件与程序理论主要研究运行于新体系架构程序的语义、可靠性保证等问题。
|
||||
研究内容包括：新型体系结构下支持编译优化、多线程程序设计、与虚拟机性能提升的内存模型的形式化定义；多处理器架构的并发程序可线性化问题、可线性化在有界与无界并发线程操作中的可判定性问题、大规模并行程序的验证等。
|
||||
为了应对新涌现的体系结构与计算平台，应研究运行于新体系架构程序的语义、可靠性保证等问题。
|
||||
研究内容包括：新型体系结构下支持编译优化、多线程程序设计、使虚拟机性能提升的内存模型的形式化定义；多处理器架构的并发程序可线性化问题、可线性化在有界与无界并发线程操作中的可判定性问题、大规模并行程序的验证等。
|
||||
%新型体系结构下内存模型的形式化定义是软件理论研究的领域之一。片上多核／众核处理器已成为计算机体系结构发展的主流。传统的顺序一致性（Sequential Consistency）模型虽然符合程序设计的直觉，但已不能满足编译优化、处理器性能提升等多方面的需要。目前主流的多核处理器如x86、ARM和Power等所实现的内存模型都放松了对一致性的要求，允许同一线程对不同地址的读写访问可以乱序执行。在程序设计语言层面，如C11/C++11、Java等，也直接定义了内存模型，支持基于共享内存的多线程程序设计，为编译优化、虚拟机性能提升等提供必要基础。但目前，处理器及程序设计语言层面的内存模型仍缺乏严格的形式化定义，使并发程序设计及验证变得更加困难。已有的语义有x86-TSO内存模型的操作语义、Power内存模型的公理语义。但如何严格刻画不同处理器、程序设计语言的内存模型，仍有待进一步研究。
|
||||
%
|
||||
%
|
||||
|
|
@ -169,8 +170,11 @@
|
|||
针对量子计算模型下的挑战性问题，具体研究内容如下：量子程序设计与验证、量子密码协议设计与验证、量子复杂性下界问题等。量子程序设计与验证的研究包括量子程序设计模型和基本指令集；适用于量子计算的程序逻辑；量子程序不变式生成问题；量子程序的模型检验问题；并行与分布式量子程序设计技术等。量子密码协议设计与验证的研究包括抗量子攻击的经典密码协议，量子随机数生成，量子密码协议验证，量子纠错与编码等。量子复杂性下界研究包括图灵机模型下量子与经典复杂性类的（神谕）区分；量子通信协议复杂性下界；量子判定树模型复杂性下界；量子计算的交互式验证等。
|
||||
|
||||
\subsection{新型软件及应用的处理与分析方法}\label{sec:stc-newsoftware}
|
||||
对于近年来新出现的各种软件及应用，核心问题是在提高系统效率的同时，如何保证系统的可靠性。基于学习的系统是近期出现的主流新型软件之一。根据不同的系统需求，有不同的研究方法。
|
||||
主要研究内容包括如何使用梯度下降优化、模型与噪音的优化等方法快速攻击系统并产生对抗样本；如何使用对抗训练、防御蒸馏等方法有效防御对基于学习系统的攻击；如何以形式化分析为基础提供该类系统的可靠性、鲁棒性等保证，如对部分系统进行验证、将语义作为训练内容增加系统可解释性、根据网络结构特点构建输出的监测器。
|
||||
|
||||
对于近年来新出现的各种软件及应用，核心问题是在提高系统效率的同时，如何保证系统的可靠性。基于机器学习的系统是近期出现的主流新型软件之一。
|
||||
%根据不同的系统需求，有不同的研究方法。
|
||||
主要研究内容包括如何快速攻击系统并产生对抗样本；如何有效防御对基于学习系统的攻击；如何以形式化分析为基础提供该类系统的可靠性、鲁棒性等保证。
|
||||
%如对部分系统进行验证、将语义作为训练内容增加系统可解释性、根据网络结构特点构建输出的监测器。
|
||||
|
||||
%一类研究围绕着如何攻击与防御人工智能系统。基于学习的模型极易受到噪音的影响，输入中的一点噪音就会改变输出结果。因此对抗样本是不可避免的。在实际系统中，对抗样本攻击的成功率非常高。如何快速地寻找对抗样本，进行攻击，是个重要的研究问题。它本质是一个优化问题，通常可以利用梯度下降优化的方法得到较好的解。目前较新的方法将模型与噪声都转变成优化目标项，而输出限制条件转换成损失函数，值域限制被转换成了平滑截断函数的变量，这样优化器可以通过直接优化目标函数，得到对抗样本。除了对抗样本的寻找，另一个方向是如何进行防御，如对抗训练、防御蒸馏等。有研究表明，即使在有防御蒸馏保护的前提下，仍可以通过转移学习生成有效的对抗样本。
|
||||
%
|
||||
|
|
@ -178,7 +182,7 @@
|
|||
%另一类研究以形式化分析为基础，提供该类系统的可靠性、鲁棒性等保证。基于神经网络的智能系统结构\index{智能系统结构}复杂，神经元结点数众多。如何验证这类系统的正确性、分析其可靠性，是一个挑战性的问题。基于抽象的方法大大提高了可处理的神经元个数。由于实际系统的输入具有不确定性，针对确定的神经网络结构判断系统对每个输入的鲁棒性难以推广，目前缺乏对实际系统可用的验证方法。一种可行的方法是对接近输出的中间层进行验证。或者，针对神经网络的可解释性问题，把语义作为训练内容，与现有的系统结合，增加网络的可解释性。另一种可行的方法是根据系统训练过程中网络结构特点，构建输出的监测器。在使用中若某个输入导致了异常的网络内部结构，则该输入可能未在训练集范围内，输出结果不一定可靠。
|
||||
|
||||
\section{本章小结}
|
||||
计算机软硬件的飞速发展以及不同领域需求的日益复杂，催生出各种实际问题，为软件的设计与开发带来巨大的机遇与挑战。作为软件学科基础的理论与方法也需要与时俱进；我们需要不断探索解决这些挑战性问题的新途径。软件理论依赖于各种数学手段；反过来，软件及理论的发展也可能给数学研究带来新的问题。
|
||||
计算机软硬件的飞速发展以及不同领域需求的日益复杂，催生出各种实际问题，为软件的设计与开发带来巨大的机遇与挑战。我们需要不断探索解决这些挑战性问题的新途径。软件理论依赖于各种数学手段；反过来，软件及理论的发展也可能给数学研究带来新的问题。作为软件学科基础的理论与方法需要与时俱进。
|
||||
|
||||
%\section{参考文献}
|
||||
%[1]. L. Peter Deutsch, Ronald B. Finkbine. ACM Fellow profile. ACM SIGSOFT Software Engineering Notes 24(1): 21 (1999).
|
||||
|
|
|
|||
|
|
@ -1,8 +1,8 @@
|
|||
|
||||
世界离不开计算，描述计算离不开程序设计语言\index{程序设计语言}。不同的程序设计语言描述不同的计算模式\index{计算模式}
|
||||
，比如，命令式语言描述以状态变迁作为计算的模式，函数式语言描述以函数作为计算的模式，逻辑语言描述以证明作为计算的模式，而量子语言则描述遵循量子力学规律调控量子信息单元进行计算的模式。在第\ref{book1-PL}章，我们对众多的程序设计语言进行了比较并回顾了程序设计语言的发展历史，从中可以看到，新的程序设计语言的出现通常是为了应对新的计算模式、新兴应用、或者新兴硬件和计算平台的需要。
|
||||
，例如，命令式语言描述以状态变迁作为计算的模式，函数式语言描述以函数作为计算的模式，逻辑语言描述以证明作为计算的模式，而量子语言则描述遵循量子力学规律调控量子信息单元进行计算的模式。在第\ref{book1-PL}章，我们对众多的程序设计语言进行了比较并回顾了程序设计语言的发展历史，从中可以看到，新的程序设计语言的出现通常是为了应对新的计算模式、新兴应用、或者新兴硬件和计算平台的需要
|
||||
|
||||
“软件定义一切”本质上是可编程思想扩张到整个社会和物理世界，是一种以软件实现分层抽象的方式来驾驭复杂性的方法论。随着人机物融合的发展，计算的泛在化成为必然，程序设计语言向下需要对物理世界进行抽象并提供处理物理世界的接口，向上需要能够处理不同场景的应用编程。{泛在计算}\index{泛在计算}中不断涌现出的新的计算模式、新的计算平台和新的应用问题给程序设计语言的定义和实现带来了新的机遇和挑战。
|
||||
“软件定义一切”本质上是可编程思想扩张到整个社会和物理世界，是一种以软件实现分层抽象的方式来驾驭复杂性的方法论。随着人机物融合的发展，计算的泛在化成为必然，程序设计语言向下需要对物理世界进行抽象并提供处理物理世界的接口，向上需要能够支撑不同场景的应用编程。{泛在计算}\index{泛在计算}中不断涌现出的新的计算模式、新的计算平台和新的应用问题给程序设计语言的定义和实现带来了新的机遇和挑战。
|
||||
|
||||
|
||||
首先，新的计算模式需要新的程序设计语言。随着不断涌现的新的计算模式，如适合于抽象描述机器学习的概率计算、神经网络计算、大数据计算、保护隐私的计算\cite{DBLP:conf/sp/RastogiHH14}等，我们需要新的语言定义和实现技术，快速开发各种各样新的程序设计语言，支持各类新型计算模式。
|
||||
|
|
@ -20,32 +20,33 @@
|
|||
在这一章里，我们将从计算的泛在和多样性，计算平台，软件的复杂性和安全性，以及软件生产率等几个方面来讨论新时代软件设计语言与支撑环境方面的挑战，列出重要的研究内容，并阐述展示程序设计语言及支撑环境方面的研究趋势。
|
||||
|
||||
\section{重大挑战问题}
|
||||
程序设计语言的挑战问题集中于如何建立、描述和实现抽象。具体来说，其挑战表现在两个方面。首先，在抽象建立和描述方面，主要表现在如何通过对领域和应用问题的抽象，开发有效的领域特定语言\index{领域特定语言}(§\ref{2_3_1_1})、支持多范式程序设计\index{多范式程序设计}(§\ref{2_3_1_2})，特别是加强大数据时代语言对数据处理的支持(§\ref{2_3_1_3})。其次，在抽象的实现方面，主要表现在如何开发人机物融合的泛在范型的编译技术(§\ref{2_3_1_4})和构建程序语言的安全性保障机制(§\ref{2_3_1_5})。
|
||||
程序设计语言的挑战问题集中于如何建立、描述和实现抽象。具体来说，其挑战表现在两个方面。首先，在抽象建立和描述方面，主要表现在如何通过对领域和应用问题的抽象，开发有效的领域特定语言\index{领域特定语言}(§\ref{2_3_1_1})、支持多范式程序设计\index{多范式程序设计}(§\ref{2_3_1_2})，特别是加强大数据时代语言对数据处理的支持(§\ref{2_3_1_3})。其次，在抽象的实现方面，主要表现在如何开发人机物融合的泛在范式的编译技术(§\ref{2_3_1_4})和构建程序语言的安全性保障机制(§\ref{2_3_1_5})。
|
||||
\note{人机物同融合的泛在范式的编译技术 请考虑一下}
|
||||
|
||||
\subsection{面向泛在计算的语言的定制}\label{2_3_1_1}
|
||||
随着泛在计算的普及，一方面，专用化的计算设备和运行平台需要软件具备面向不同专用硬件和平台的高效定制能力；另一方面，泛在服务软件需要提供各种特定的编程抽象，支持面向人机物融合的最终用户编程。在泛在计算的环境下，程序员的概念也不断泛化——未来越来越多的人，甚至那些缺乏足够计算机专业知识的领域专家，需要对专用化的设备或特定领域的问题进行程序设计。这就需要我们开发各式各样的领域特定语言。泛在计算对领域特定语言的定义和实现带来了新的挑战。
|
||||
|
||||
\begin{itemize}
|
||||
\item 特定领域语言一般是轻量的，是通用语言的特例。在通用语言的实现已经存在的前提下，我们可以用通用语言的方式来定义和实现领域特定语言。然而，这种方式不仅增加了开发的难度，而且也不经济。我们需要一种高效的特定语言的定义和实现方法。一种思路是设计并实现一种通用语言作为特定语言定义和实现的基础，但是什么样的通用语言适合于定义和实现各类特定领域语言是一个必须解决的问题。
|
||||
\item 对于通用语言，我们已经开发了不少很有用的程序分析、优化、调试、测试方法。对于特定领域语言，我们需要利用这些方法。尽管我们可以用通用语言来实现某种特定领域语言，但是如何能够将这些一般性的方法系统化地映射到特定语言的实现上是一个挑战。比如，假设我们在通用语言上实现了一个测试方法，但是通用语言上的测试结果对于特定领域语言的用户而言是不能理解的。我们需要将通用语言上的测试例子和结果映射到特定语言程序上，特定领域语言的用户才能理解。
|
||||
\item 在设计特定领域语言时存在的一个选择是应该设计一个小而精的语言，还是设计一个大而全面的语言？Schema语言的设计者之一的Guy Steele认为，既不应该建立一种小语言，也不应该建立一种大语言，而需要设计一种可以成长的语言。语言设计应该是增长式的——语言必须从小开始，能够随着用户集的增长而增长。例如，我们可以比较APL语言和Lisp语言：APL不允许用户以“流畅”的方式向该语言添加新的原语（Premitive)，这使得用户难以扩展该语言；在Lisp中，用户可以定义与语言基元保持一致的单词，它使语言用户可以轻松扩展语言并共享代码。为此，在设计语言时，我们面临的挑战是，如何保证其具有一定的韧性，支持新的语言构造和特性可以被无缝接入其中，同时，在语言演化过程中，也能保证遗留系统被无障碍地执行。
|
||||
\item 特定领域语言一般是轻量的，是通用语言的特例。在通用语言的实现已经存在的前提下，我们可以用通用语言的方式来定义和实现领域特定语言。然而，这种方式不仅增加了开发的难度，而且也不经济。我们需要一种高效的特定语言的定义和实现方法。一种思路是设计并实现一种通用元级语言作为特定语言定义和实现的基础，但是什么样的通用语言适合于定义和实现各类特定领域语言是一个必须解决的问题。
|
||||
\item 对于通用语言，我们已经开发了不少很有用的程序分析、优化、调试、测试方法。对于特定领域语言，我们需要利用这些方法。尽管我们可以用通用语言来实现某种特定领域语言，但是如何能够将这些一般性的方法系统化地映射到特定语言的实现上是一个挑战。例如，假设我们在通用语言上实现了一个测试方法，但是通用语言上的测试结果对于特定领域语言的用户而言是不能理解的。我们需要将通用语言上的测试例子和结果映射到特定语言程序上，特定领域语言的用户才能理解。
|
||||
\item 在设计特定领域语言时存在的一个选择是应该设计一个小而精的语言，还是设计一个大而全面的语言？Schema语言的设计者之一的Guy Steele认为，既不应该建立一种小语言，也不应该建立一种大语言，而需要设计一种可以成长的语言。语言设计应该是增长式的——语言必须从小开始，能够随着用户集的增长而增长。例如，我们可以比较APL语言和Lisp语言：APL不允许用户以“流畅”的方式向该语言添加新的原语（Premitive)，这使得用户难以扩展该语言；在Lisp中，用户可以定义与语言基元保持一致的单词，它使语言用户可以轻松扩展语言并共享代码。为此，在设计语言时，我们面临的挑战是，如何保证其具有一定的柔性，支持新的语言构造和特性可以被无缝接入其中，同时，在语言演化过程中，也能保证遗留系统被无障碍地执行。
|
||||
\end{itemize}
|
||||
|
||||
\subsection{多范式程序设计的语言支持}\label{2_3_1_2}
|
||||
主流程序设计语言支持不同的程序设计范式\cite{ DBLP:journals/software/WamplerC10}。从程序设计语言的角度出发，一方面，需要设计与程序设计语言相适应的程序设
|
||||
计范型或者程序设计模型，以获取程序可读性、模块性、抽象性和性能上的平衡。另一方面，需要提供技术手段，根据程序员能力或者开发任务自动选择或者推荐程序设计范型，
|
||||
提升程序员程序设计效率。然而随着解决的问题越来越复杂，我们需要研究支持多范型的程序设计语言，以及对多范型语言的高效实现机制。特别是，我们面对下面一些挑战。
|
||||
计范式或者程序设计模型，以获取程序可读性、模块性、抽象性和性能上的平衡。另一方面，需要提供技术手段，根据程序员能力或者开发任务自动选择或者推荐程序设计范式，
|
||||
提升程序员程序设计效率。然而随着解决的问题越来越复杂，我们需要研究支持多范式的程序设计语言，以及对多范式语言的高效实现机制。特别是，我们面对下面一些挑战。
|
||||
|
||||
|
||||
首先，如何将描述函数计算最直接的函数式程序设计\index{函数式程序设计}融合到其它语言中是多范型语言设计的一个挑战。函数式程序设计\cite{kar50323}用函数来抽象
|
||||
计算，它的高阶函数和计算的透明性的两个重要特征，一方面使函数式语言适用于大数据处理、人工智能等领域，但是另一方面也使它不容易与其它语言共用。尽管已有不少关于研究和系统讨论如何融合逻辑语言与函数式语言\cite{DBLP:series/lncs/Torra16}，融合面向目标式语言和函数式语言，不少通用程序设计语言（C++和Java、Kotlin等）也
|
||||
开始支持函数式程序设计，但是，现在还没有一个公认的计算模型来系统地支持这种融合的设计和实现。如何将函数式语言的高阶函数和计算透明性有效而便捷地扩展至通用程序设计语言及支撑环境，以支持函数式程序设计或混成程序设计，成为一个值得关注的挑战问题。
|
||||
首先，如何将描述函数计算最直接的函数式程序设计\index{函数式程序设计}融合到其它语言中是多范式语言设计的一个挑战。函数式程序设计\cite{kar50323}用函数来抽象
|
||||
计算，它的高阶函数和计算的透明性的两个重要特征，一方面使函数式语言适用于大数据处理、人工智能等领域，但是另一方面也使它不容易与其它语言共用。尽管已有不少关于研究和系统讨论如何融合逻辑语言与函数式语言\cite{DBLP:series/lncs/Torra16}，融合面向对象语言和函数式语言，不少通用程序设计语言（C++和Java、Kotlin等）也
|
||||
开始支持函数式程序设计，但是，现在还没有一个公认的计算模型来系统地支持这种融合的设计和实现。如何将函数式语言的高阶函数和计算透明性有效而便捷地扩展至函数式语言以外的其他通用程序设计语言，以支持函数式程序设计或混成程序设计，成为一个值得关注的挑战问题。
|
||||
|
||||
|
||||
其次，无缝融合并发程序设计是多范型语言设计和实现的另一个挑战。目前已经存在很多并发程序设计模型，它们指定了系统中的线程/
|
||||
其次，无缝融合并发程序设计是多范式语言设计和实现的另一个挑战。目前已经存在很多并发程序设计模型，它们指定了系统中的线程/
|
||||
进程如何通过协作来完成分配给它们的作业——不同的并发模型采用不同的方式拆分任务，线程/进程间的协作和交互方式也不相同。为此，需要建立与特定程序设计语言相适应的
|
||||
一组并发模型，更好支持程序员设计与实现并发任务。此外，传统的并发思维，是在单个处理器上，使用分时方式或是时间片模型来执行多个任务。如今的并发场景则正好相反，
|
||||
是将一个逻辑上的任务放在多个处理器或者多核上执行。因此，程序设计语言需要提供足够的机制来分解任务。然而，基于目前并发API，比如线程、线程池、监视等，编写并发程
|
||||
是将一个逻辑上的任务放在多个处理器或者多核上执行。因此，程序设计语言需要提供足够的机制来分解任务。然而，基于目前并发API，例如，线程、线程池、监视等，编写并发程
|
||||
序依然很困难，还需要更多关于程序设计语言及实现方面的努力。例如，可以由编译器甚至执行引擎识别出程序中可并发的任务，以便多核计算机可以将其安全地并发执行。
|
||||
|
||||
\subsection{大数据处理的程序语言支持}\label{2_3_1_3}
|
||||
|
|
@ -58,12 +59,12 @@
|
|||
其次，大数据具有体量巨大、数据增长快的特点。这就意味着，要对海量的大数据进行分析，不但人工无法完成，小型计算机系统通常也无法完成。要完成海量的数据分析，往往需要包含多个CPU的大型机系统，或者由多个中小型计算机联网形成的集群系统。但是，用普通程序设计语言编写这类集群系统上的大数据处理程序非常复杂，因为程序员必须处理并行任务分解、多CPU/计算机调度、进程/线程同步等一系列问题。需要新的程序设计语言来降低大数据处理程序的编写难度。尽管MapReduce, Pregel等面向大数据处理的并行计算模型已经提出，但是基于这些模型的程序语言要么接近于模型、用户难以使用，要么用户容易写，但是缺少优化方法、运行效率低。需要新的程序设计语言来解决此类数据计算需求。
|
||||
|
||||
|
||||
最后，大数据具有价值密度低的特点，这就意味着如果要发挥大数据的作用，需要采用合适的方式对数据进行统计。有效的统计方法往往需要我们针对数据的特点构建统计模型，然后根据统计模型对数据进行统计。比如，现在流行的神经网络需要用户首先给出网络结构，然后根据数据确定网络中参数数值。而基于统计学的概率图方法需要先确定随机变量的分布和随机变量之间的依赖关系，然后基于数据确定随机变量的后验分布。这些统计模型的编写较为复杂，同时给定模型之后的统计算法也比较复杂，因此，需要有新的程序设计语言来支持这类模型的描述（如概率编程等）、验证和测试。
|
||||
最后，大数据具有价值密度低的特点，这就意味着如果要发挥大数据的作用，需要采用合适的方式对数据进行统计。有效的统计方法往往需要我们针对数据的特点构建统计模型，然后根据统计模型对数据进行统计。例如，现在流行的神经网络需要用户首先给出网络结构，然后根据数据确定网络中参数数值。而基于统计学的概率图方法需要先确定随机变量的分布和随机变量之间的依赖关系，然后基于数据确定随机变量的后验分布。这些统计模型的编写较为复杂，同时给定模型之后的统计算法也比较复杂，因此，需要有新的程序设计语言来支持这类模型的描述（如概率编程等）、验证和测试。
|
||||
|
||||
\subsection{面向人机物融合的编译}\label{2_3_1_4}
|
||||
\subsection{面向人机物融合的泛在范式的编译技术}\label{2_3_1_4}
|
||||
编译器\index{编译器}是程序设计语言的重要支撑环境，其负责将一种语言（通常为高级语言）所书写的程序变换成另一种语言（通常为低级语言）程序。编译器的另一个主要功能是对程序进行优化，提升软件的性能。现代软件系统呈现人机物融合的泛在混成特性，对编译技术也带来新的挑战。
|
||||
|
||||
首先，编译器需要能够快速应对不断出现的专用处理器。摩尔定律的逐渐失效以及大数据处理深度学习等新应用需求的出现，正助推计算机行业从通用计算机系统，转向一个青睐专用微处理器和专用存储系统等专用硬件的时代。这种转变需要我们研究新的更有效的编译技术。当一个新的硬件出现之后，首先，应该对专用硬件进行抽象，定义一个底层使用该硬件的领域特定语言（DSL）\cite{ DBLP:books/daglib/0030751}\cite{Thereska:2013:ISS:2517349.2522723}；然后，扩充现有的语言，为之提供一个高层次的界面，以便用户描述专用硬件上的计算；最后，定义如何将高层次的程序翻译到底层的DSL。为了支持这个过程，我们需要研究自动编译技术——我们预测未来的编译器能够在SMT等求解器的帮助下自动生成能在专用处理器上运行的的目标程序，通过重写策略对目标程序自动优化，且保证编译过程的正确性和代码质量\cite{Rompf:2012:LMS:2184319.2184345}\cite{ Chen:2018:TAE:3291168.3291211}\cite{Monsanto:2012:CRS:2103656.2103685}。
|
||||
首先，编译器需要能够快速应对不断出现的专用处理器。摩尔定律的逐渐失效以及大数据处理深度学习等新应用需求的出现，正助推计算机行业从通用计算机系统，转向一个青睐专用微处理器和专用存储系统等专用硬件的时代。这种转变需要我们研究新的更有效的编译技术。当一个新的硬件出现之后，首先，应该对专用硬件进行抽象，定义一个底层使用该硬件的领域特定语言（DSL）\cite{ DBLP:books/daglib/0030751}\cite{Thereska:2013:ISS:2517349.2522723}；然后，扩充现有的语言，为之提供一个高层次的界面，以便用户描述专用硬件上的计算；最后，定义如何将高层次的程序翻译到底层的DSL。为了支持这个过程，我们需要研究自动编译技术——我们预测未来的编译器能够在SMT等求解器的帮助下自动生成能在专用处理器上运行的目标程序，通过重写策略对目标程序自动优化，且保证编译过程的正确性和代码质量\cite{Rompf:2012:LMS:2184319.2184345}\cite{ Chen:2018:TAE:3291168.3291211}\cite{Monsanto:2012:CRS:2103656.2103685}。
|
||||
|
||||
|
||||
其次，编译器需要能够高效地处理混成系统\index{混成系统}。现在的软件系统越来越复杂，形成了一个混成的系统，需要既能处理离散的又能处理连续的计算，既能处理确定性（逻辑式）的又能处理概率性的计算，既针对命令式的又针对函数式的程序设计语言，既可静态类型检查又可以动态确认程序满足的性质。为了开发这样的复杂的软件系统，混成语言以及相应编译技术变得非常重要。此外，复杂软件系统可能由不同程序设计语言书写的程序组成。对不同程序设计语言所书写的程序进行高效混成编译，也是一个值得关注的研究问题。
|
||||
|
|
@ -74,7 +75,7 @@
|
|||
首先，需要建立语言安全性和灵活性、复杂性之间的平衡。程序设计语言的安全性主要体现为程序设计模型中一组机制，保障程序员写出安全的程序。例如，C++支持的RAII（资源获取即初始化）通过栈语义保证对象析构函数的自动调用，解决了内存泄漏问题；类型系统使代码仅能访问被授权可以访问的内存位置；脸书公司推出的智能合约语言Move语言不支持动态分配和循环递归依赖等\cite{ 2019Move}等。然而，语言安全性的提升意味着程序设计灵活性的下降、支撑环境复杂性的提升。为此，在设计一门程序设计语言的同时，需要定义一组通用的或领域/环境相关的安全机制，包括是否支持指针、自动垃圾回收、异常处理，是否支持强类型检查和中间码验证等，一方面允许程序设计人员编写出既功能强大又足够安全的程序，另一方面在静态编译或者动态执行时实现程序的安全性检查。
|
||||
|
||||
|
||||
其次，需要提供充分保障支撑环境可靠性、安全性的分析、测试和验证等技术手段。编译器、虚拟机和执行引擎的代码复杂，其中潜伏着包含缺陷或者安全漏洞。如何提升编译器、虚拟机和执行引擎的安全性是一个重要的问题。当前已经出现了经过验证的编译器，例如CompCert\cite{Leroy:2009:FVR:1538788.1538814}\cite{Wang:2019:ASB:3302515.3290375}。此外，已经出现了一批针对编译器和虚拟机的测试和安全分析工作，例如CSmith\cite{Yang:2011:FUB:1993498.1993532}、EMI等。尽管如此，对编译器（包括优化算法）及虚拟机等安全性分析、测试、验证工作还面临很多问题，我们仍需要能够充分保障编译器、虚拟机和执行引擎的安全性的分析、测试和验证技术手段。例如，不可能枚举出一个语言的所有程序实例以对支撑环境进行穷尽测试，相反，需要提供一套策略，协助选择或者自动生成具有代表性的程序实例以高效测试支撑环境的健壮性。特别是，针对支撑环境进行广泛测试，针对各类编译技术和算法（如优化算法和垃圾回收算法）进行正确性验证，及验证应用程序接口的正确性，仍然是这个方向上的难点问题。此外，在程序设计语言动态演化过程中，需要提供足够的技术手段，保障语言新特性和支撑环境新功能可以被可靠地、安全地加入至既有语言和支撑环境中。
|
||||
其次，需要提供充分保障支撑环境可靠性、安全性的分析、测试和验证等技术手段。编译器、虚拟机和执行引擎的代码复杂，其中潜伏着包含缺陷或者安全漏洞。如何提升编译器、虚拟机和执行引擎的安全性是一个重要的问题。当前已经出现了经过验证的编译器，例如，CompCert\cite{Leroy:2009:FVR:1538788.1538814}\cite{Wang:2019:ASB:3302515.3290375}。此外，已经出现了一批针对编译器和虚拟机的测试和安全分析工作，例如，CSmith\cite{Yang:2011:FUB:1993498.1993532}、EMI等。尽管如此，对编译器（包括优化算法）及虚拟机等安全性分析、测试、验证工作还面临很多问题，我们仍需要能够充分保障编译器、虚拟机和执行引擎的安全性的分析、测试和验证技术手段。例如，不可能枚举出一个语言的所有程序实例以对支撑环境进行穷尽测试，相反，需要提供一套策略，协助选择或者自动生成具有代表性的程序实例以高效测试支撑环境的健壮性。特别是，针对支撑环境进行广泛测试，针对各类编译技术和算法（如优化算法和垃圾回收算法）进行正确性验证，及验证应用程序接口的正确性，仍然是这个方向上的难点问题。此外，在程序设计语言动态演化过程中，需要提供足够的技术手段，保障语言新特性和支撑环境新功能可以被可靠地、安全地加入至既有语言和支撑环境中。
|
||||
|
||||
\tikzstyle{every node}=[draw=black,thick,anchor=west]
|
||||
\tikzstyle{selected}=[draw=red,fill=red!30]
|
||||
|
|
@ -114,8 +115,9 @@
|
|||
child {node {\bf 支持最终用户编程的程序设计语言}}
|
||||
}
|
||||
child [missing] {}
|
||||
child {node {多范型程序设计}
|
||||
child {node {\bf 多范型和领域特定的程序设计语言}}
|
||||
child {node {多范式/新范式程序设计}
|
||||
child {node {\bf 多范式和领域特定的程序设计语言}}
|
||||
child {node {\bf 智能合约的设计语言}}
|
||||
}
|
||||
child [missing] {}
|
||||
}
|
||||
|
|
@ -163,10 +165,10 @@
|
|||
|
||||
|
||||
\section{主要研究内容}
|
||||
程序设计语言的主要研究内容请参见图\ref{fig:ProgrammingLanguages}。为了应对上述重大挑战，需要在多方面开展研究。首先，为了支持泛在计算(§\ref{2_3_2_1})、大数据处理(§\ref{2_3_2_3})、和人机物融合(§\ref{2_3_2_4})等多种新型应用场景，需要研究面向不同领域的编程语言，包括面向数据管理统计的程序设计语言(§\ref{2_3_2_2})、面向软件定义网络的程序设计语言(§\ref{2_3_2_3})、支持最终用户编程的程序设计语言(§\ref{2_3_2_6})。其次，为了设计面向泛在计算的语言(§\ref{2_3_2_1})和实现多范型程序设计支持(§\ref{2_3_2_2})，需要研究多范型和领域特定的程序设计语言(§\ref{2_3_2_1})、离散和连续混成系统的语言和工具(§\ref{2_3_2_4})以及支持共享内存模型的并发程序设计(§\ref{2_3_2_5})。最后，为了支持新语言所带来的开发环境和生态的变化，我们需要研究程序设计框架和程序设计开发环境(§\ref{2_3_2_7})、特定领域语言的元编程和开发环境(§\ref{2_3_2_8})、程序设计语言的生态及其演化规律(§\ref{2_3_2_9})。在图中，我们用粗体表示本章讨论的研究内容。
|
||||
程序设计语言的主要研究内容请参见图\ref{fig:ProgrammingLanguages}。为了应对上述重大挑战，需要在多方面开展研究。首先，为了支持泛在计算、大数据处理、和人机物融合等多种新型应用场景，需要研究面向不同领域的编程语言，包括面向数据管理统计的程序设计语言(§\ref{2_3_2_2})、面向软件定义网络的程序设计语言(§\ref{2_3_2_3})、描述智能合约的设计语言(§\ref{2_3_2_10})、支持最终用户编程的程序设计语言(§\ref{2_3_2_6})。其次，为了设计面向泛在计算的语言和实现多范式程序设计支持，需要研究多范式和领域特定的程序设计语言(§\ref{2_3_2_1})、离散和连续混成系统的语言和工具(§\ref{2_3_2_4})以及支持共享内存模型的并发程序设计(§\ref{2_3_2_5})。最后，为了支持新语言所带来的开发环境和生态的变化，我们需要研究程序设计框架和程序设计开发环境(§\ref{2_3_2_7})、特定领域语言的元编程和开发环境(§\ref{2_3_2_8})、程序设计语言的生态及其演化规律(§\ref{2_3_2_9})。在图中，我们用粗体表示本章讨论的研究内容。
|
||||
|
||||
\subsection{多范型和领域特定的程序设计语言}\label{2_3_2_1}
|
||||
主流程序设计语言都支持多种程序设计范型。一方面需要研究如何设计程序设计语言所支持的范型乃至于库、编程框架等，以助于程序员更便捷地编写大型应用。另一方面，需要研究如何根据程序员能力或者开发任务自动选择或者推荐程序设计范型，以提升程序员程序设计效率。此外，也需要对多范型程序设计语言的支撑环境（含编译、编译时和运行时优化、内存管理、多线程处理、垃圾回收等）及其程序分析、验证技术进行研究——在一门程序设计语言中引入新的程序设计范型，往往需要很多工业界和学术界的努力，避免支撑环境的复杂性、分析及验证技术难度的急剧上升。
|
||||
\subsection{多范式和领域特定的程序设计语言}\label{2_3_2_1}
|
||||
主流程序设计语言都支持多种程序设计范式。一方面需要研究如何设计程序设计语言所支持的范式乃至于库、编程框架等，以助于程序员更便捷地编写大型应用。另一方面，需要研究如何根据程序员能力或者开发任务自动选择或者推荐程序设计范式，以提升程序员程序设计效率。此外，也需要对多范式程序设计语言的支撑环境（含编译、编译时和运行时优化、内存管理、多线程处理、垃圾回收等）及其程序分析、验证技术进行研究——在一门程序设计语言中引入新的程序设计范式，往往需要很多工业界和学术界的努力，避免支撑环境的复杂性、分析及验证技术难度的急剧上升。
|
||||
|
||||
|
||||
随着专用处理器（如GPU、TPU）等硬件的不断出现以及各种特定应用领域软件开发的需求，领域特定语言的开发变得非常重要。领域特定语言既向下提供特定平台的编程模型，也向上提供具体应用场景的需求描述方法。尽管我们可以使用一般的程序语言的设计方法和编译技术，但是这样开发效率低。我们应该开发在通用语言的基础上实现领域特定语言的技术。主要研究内容包括：（1）运行时和编译时的错误的直观表示；（2）DSL程序测试用例的自动生成；和（3）深度嵌入和浅度嵌入的领域特定语言的定义方法的有机结合。
|
||||
|
|
@ -188,22 +190,22 @@
|
|||
由于处理器和编译器对程序的优化，大多数处理器和程序设计语言（如C++或Java）无法提供理想化的顺序一致性（Sequential Consistency）内存模型\index{内存模型}。近年，来对内存一致性模型的形式化定义成为研究的热点，包括对处理器（如x86、Arm、Power等）和并发程序设计语言（如C++和Java等）的内存模型的设计与实现等。然而，现有程序设计语言的内存模型仍然存在较多问题。Java和C++的内存模型仍然过于复杂，且允许程序产生违背直观的行为，特别是跟程序逻辑完全无关的行为（即所谓的out-of-thin-air行为，简写为OOTA）。因此这些内存模型还有待改进。另一方面，经典的并发验证逻辑和既有分析、测试、验证工具无法直接应用于弱内存模型程序，我们需要新的理论和工具支持。针对以上不足，我们需要解决以下问题：（1）改良现有的程序设计语言中的内存模型，避免内存模型中的OOTA行为；（2）基于改良后的内存模型，给出新型的并发程序验证、分析、测试的技术，保证弱内存模型下的并发程序编译及执行的正确性。
|
||||
|
||||
|
||||
\subsection{智能合约的设计语言和开发环境}
|
||||
\subsection{智能合约的设计语言和开发环境}\label{2_3_2_10}
|
||||
|
||||
智能合约是一种以信息化方式传播、验证或执行合同的计算机协议，允许在没有第三方的情况下进行可信合约的签订。智能合约实质上是一种代码合约和算法合同，将成为未来数字社会的基础技术。它的主要研究内容包括：(1) 设计易于开发智能合约的设计语言；（2）研究规模化智能合约的自动生成技术；（3）研究适合于智能合约生命周期的形式化验证框架和验证方法；（4）实现智能合约的开发环境。
|
||||
|
||||
|
||||
\subsection{支持最终用户编程的程序设计语言}\label{2_3_2_6}
|
||||
最终用户程序设计主要涉及两条研究路线。一条路线是从教育的角度出发，把现有程序设计语言中的概念用更简单直观的图形化方式表达出来，使得没有学过程序设计的人也能很快熟悉和掌握。研究内容包括：(1)设计一组被最终用户所能接受和使用的语言构造，并通过相关支撑环境实现将用户设计的程序“编译”为可以被具体执行的程序; (2)研究提升此类程序设计语言的表达及容错能力的方法。\index{最终用户程序设计}的另一条路线是针对特定领域让用户用最自然的方式表达需求，同时用程序综合的方式来完成程序的构造\cite{ DBLP:journals/ftpl/GulwaniPS17}。主要研究内容包括：（1）研究适用于不同应用场景和不同用户级别的需求表达方式；（2）研究将这些需求自动转换成程序的方法。
|
||||
最终用户程序设计主要涉及两条研究路线。一条路线是从教育的角度出发，把现有程序设计语言中的概念用更简单直观的图形化方式表达出来，使得没有学过程序设计的人也能很快熟悉和掌握。研究内容包括：(1)设计一组被最终用户所能接受和使用的语言构造，并通过相关支撑环境实现将用户设计的程序“编译”为可以被具体执行的程序; (2)研究提升此类程序设计语言的表达及容错能力的方法。最终用户程序设计\index{最终用户程序设计}的另一条路线是针对特定领域让用户用最自然的方式表达需求，同时用程序综合的方式来完成程序的构造\cite{ DBLP:journals/ftpl/GulwaniPS17}。主要研究内容包括：（1）研究适用于不同应用场景和不同用户级别的需求表达方式；（2）研究将这些需求自动转换成程序的方法。
|
||||
|
||||
最终用户程序设计的一个重要应用领域是应对面向人机物融合的大趋势，为最终用户提供控制网络上设备的编程方式。目前，在这个方向上已经有一些典型的应用，包括为智能家居的物联网设备编程。比如，物联网编程语言IFTTT采用了IF语句作为基础编程单元，主要表达不同条件满足的时候设备应该采用的动作。很多主流的智能家居企业比如小米、华为都采用了这种编程模型。但目前编程模型的能力还有较大局限性，一些需求无法完全表达；同时在程序变得比较复杂的时候，基于IFTTT的编程方式也容易带来预期之外的交互，引起较难调试的问题。
|
||||
最终用户程序设计的一个重要应用领域是应对面向人机物融合的大趋势，为最终用户提供控制网络上设备的编程方式。目前，在这个方向上已经有一些典型的应用，包括为智能家居的物联网设备编程。例如，物联网编程语言IFTTT采用了IF语句作为基础编程单元，主要表达不同条件满足的时候设备应该采用的动作。很多主流的智能家居企业，例如，小米、华为都采用了这种编程模型。但目前编程模型的能力还有较大局限性，一些需求无法完全表达；同时在程序变得比较复杂的时候，基于IFTTT的编程方式也容易带来预期之外的交互，引起较难调试的问题。
|
||||
|
||||
|
||||
\subsection{程序设计框架和程序设计开发环境}\label{2_3_2_7}
|
||||
程序设计语言与编程环境、程序设计框架、程序设计工具需要协同发展。近几十年来程序设计的努力主要体现在框架及工具等方面。例如.NET Framework里有超过一万个类及十万个方法，现有的编译器和解释器之间的界限越来越模糊。类似的，现在的IDE包含了无数强大的功能，例如语法提示，重构，调试器等。上述程序设计框架、工具等支撑着高层语言的普及和使用。因此，需要设计与开发与程序设计语言相匹配的程序设计框架和程序设计环境，支撑多范型程序设计，并集成程序搜索、推荐、自动修复等功能，以支持程序员轻易地开发出更强大的应用\cite{ DBLP:journals/ftpl/VechevY16}。
|
||||
程序设计语言与编程环境、程序设计框架、程序设计工具需要协同发展。近几十年来程序设计的努力主要体现在框架及工具等方面。例如，.NET Framework里有超过一万个类及十万个方法，现有的编译器和解释器之间的界限越来越模糊。类似的，现在的IDE包含了无数强大的功能，例如，语法提示，重构，调试器等。上述程序设计框架、工具等支撑着高层语言的普及和使用。因此，需要设计与开发与程序设计语言相匹配的程序设计框架和程序设计环境，支撑多范式程序设计，并集成程序搜索、推荐、自动修复等功能，以支持程序员轻易地开发出更强大的应用\cite{ DBLP:journals/ftpl/VechevY16}。
|
||||
|
||||
\subsection{特定领域语言的元编程和开发环境}\label{2_3_2_8}
|
||||
程序设计语言方面另一个研究内容是构建支持特定领域语言的定义和实现的开发环境。这个环境需支持高效而正确地设计和实现众多的领域特定语言，抓住不同领域的计算特征，便于领域专家使用。同时，为了高效组合不同领域的计算特征，需要构建“面向语言”的程序设计环境。面向语言的程序设计明确鼓励开发人员构建自己的领域特定语言，或者将具有特定领域概念的现有语言作为方法的一部分进行扩展。利用这个环境，程序员在软件开发时不是只使用一种语言，而是使用最适合每项任务的语言，然后把它们有机组合在一起。例如，MPS (Meta Programming System) 等语言工作台是面向语言方法的重要组成部分。使用MPS，可以为任何新语言定义编辑器，使得领域特定语言的使用更简便。即使是不熟悉传统程序设计的领域专家，也可以在MPS中使用领域特定语言。
|
||||
程序设计语言方面的一个研究内容是构建支持特定领域语言的定义和实现的开发环境。这个环境需支持高效而正确地设计和实现众多的领域特定语言，抓住不同领域的计算特征，便于领域专家使用。同时，为了高效组合不同领域的计算特征，需要构建“面向语言”的程序设计环境。面向语言的程序设计明确鼓励开发人员构建自己的领域特定语言，或者将具有特定领域概念的现有语言作为方法的一部分进行扩展。利用这个环境，程序员在软件开发时不是只使用一种语言，而是使用最适合每项任务的语言，然后把它们有机组合在一起。例如，MPS (Meta Programming System) 等语言工作台是面向语言方法的重要组成部分。使用MPS，可以为任何新语言定义编辑器，使得领域特定语言的使用更简便。即使是不熟悉传统程序设计的领域专家，也可以在MPS中使用领域特定语言。
|
||||
|
||||
\subsection{程序设计语言的生态及其演化规律}\label{2_3_2_9}
|
||||
程序设计语言的流行与发展，离不开其生态的繁荣与发展。程序设计语言的生态是围绕各种程序设计语言，为了支持语言标准化、使用及扩展所形成的语言设施（包括语言标准、集成开发环境、编译器、虚拟机、标准库、扩展功能支持库等）、语言涉众（包含语言的学习者、使用者、维护者、标准委员会和用户社区等）和知识体系（帮助文档和知识库、资源下载网站、教程和培训等），及在此基础上形成的相互依赖和相互作用的网络。生态提供了对程序设计语言更广泛的支持。然而，针对程序设计语言生态的研究还不多。仍需要对程序设计语言生态进行大量研究，研究如何定义/描述一个程序设计语言及其生态系统，以及研究如何将一个既有项目从一个语言生态迁移至另一个语言生态等。此外，需要分析生态系统的利益相关者及生态中蕴含的海量知识/数据等，以更好发现程序设计语言与生态、利益相关者的伴生、共同演化与发展的规律。
|
||||
|
|
|
|||
BIN
fig1-2/2-2.png
BIN
fig1-2/2-2.png
Binary file not shown.
|
Before Width: | Height: | Size: 173 KiB After Width: | Height: | Size: 172 KiB |
BIN
fig1-2/2-4.png
BIN
fig1-2/2-4.png
Binary file not shown.
|
Before Width: | Height: | Size: 135 KiB After Width: | Height: | Size: 116 KiB |
BIN
fig2-2/2-1.png
BIN
fig2-2/2-1.png
Binary file not shown.
|
Before Width: | Height: | Size: 44 KiB After Width: | Height: | Size: 46 KiB |
102
references.bib
102
references.bib
|
|
@ -1441,7 +1441,7 @@ year = {1937}
|
|||
}
|
||||
|
||||
@Article{Deutsch99,
|
||||
author = {L. Peter Deutsch, Ronald B. Finkbine},
|
||||
author = {Deutsch, L. Peter and Finkbine, Ronald B.},
|
||||
title = {{ACM} {Fellow} profile},
|
||||
journal = {ACM SIGSOFT Software Engineering Notes},
|
||||
year = {1999},
|
||||
|
|
@ -1550,13 +1550,7 @@ year = {1937}
|
|||
year = {1969},
|
||||
issn = {0001-0782},
|
||||
pages = {576--580},
|
||||
numpages = {5},
|
||||
url = {http://doi.acm.org/10.1145/363235.363259},
|
||||
doi = {10.1145/363235.363259},
|
||||
acmid = {363259},
|
||||
publisher = {ACM},
|
||||
address = {New York, NY, USA},
|
||||
keywords = {axiomatic method, formal language definition, machine-independent programming, program documentation, programming language design, theory of programming' proofs of programs},
|
||||
numpages = {5}
|
||||
}
|
||||
|
||||
@inproceedings{Rosu15,
|
||||
|
|
@ -1581,12 +1575,7 @@ year = {1937}
|
|||
year = {1992},
|
||||
issn = {0004-5411},
|
||||
pages = {95--146},
|
||||
numpages = {52},
|
||||
url = {http://doi.acm.org/10.1145/147508.147524},
|
||||
doi = {10.1145/147508.147524},
|
||||
acmid = {147524},
|
||||
publisher = {ACM},
|
||||
address = {New York, NY, USA},
|
||||
numpages = {52}
|
||||
}
|
||||
|
||||
@book{hoare1998unifying,
|
||||
|
|
@ -3527,4 +3516,89 @@ author = {CIO Staff}
|
|||
number={10},
|
||||
pages={1100--1126},
|
||||
year={2006}
|
||||
}
|
||||
|
||||
@book{herlihy2011art,
|
||||
title={The art of multiprocessor programming},
|
||||
author={Herlihy, Maurice and Shavit, Nir},
|
||||
year={2011},
|
||||
publisher={Morgan Kaufmann}
|
||||
}
|
||||
|
||||
@book{lunze2009handbook,
|
||||
title={Handbook of hybrid systems control: theory, tools, applications},
|
||||
author={Lunze, Jan and Lamnabhi-Lagarrigue, Fran{\c{c}}oise},
|
||||
year={2009},
|
||||
publisher={Cambridge University Press}
|
||||
}
|
||||
|
||||
@article{chen2014data,
|
||||
title={Data-intensive applications, challenges, techniques and technologies: A survey on Big Data},
|
||||
author={Chen, CL Philip and Zhang, Chun-Yang},
|
||||
journal={Information sciences},
|
||||
volume={275},
|
||||
pages={314--347},
|
||||
year={2014},
|
||||
publisher={Elsevier}
|
||||
}
|
||||
|
||||
@article{koopman2017autonomous,
|
||||
title={Autonomous vehicle safety: An interdisciplinary challenge},
|
||||
author={Koopman, Philip and Wagner, Michael},
|
||||
journal={IEEE Intelligent Transportation Systems Magazine},
|
||||
volume={9},
|
||||
number={1},
|
||||
pages={90--96},
|
||||
year={2017},
|
||||
publisher={IEEE}
|
||||
}
|
||||
|
||||
@inproceedings{arpteg2018software,
|
||||
title={Software engineering challenges of deep learning},
|
||||
author={Arpteg, Anders and Brinne, Bj{\"o}rn and Crnkovic-Friis, Luka and Bosch, Jan},
|
||||
booktitle={2018 44th Euromicro Conference on Software Engineering and Advanced Applications (SEAA)},
|
||||
pages={50--59},
|
||||
year={2018},
|
||||
organization={IEEE}
|
||||
}
|
||||
|
||||
@inproceedings{sewell2013translation,
|
||||
title={Translation validation for a verified OS kernel},
|
||||
author={Sewell, Thomas Arthur Leck and Myreen, Magnus O and Klein, Gerwin},
|
||||
booktitle={Proceedings of the 34th ACM SIGPLAN conference on Programming language design and implementation},
|
||||
pages={471--482},
|
||||
year={2013}
|
||||
}
|
||||
|
||||
@book{ying2016foundations,
|
||||
title={Foundations of Quantum Programming},
|
||||
author={Ying, Mingsheng},
|
||||
year={2016},
|
||||
publisher={Morgan Kaufmann}
|
||||
}
|
||||
|
||||
@article{montanaro2016quantum,
|
||||
title={Quantum algorithms: An overview},
|
||||
author={Montanaro, Ashley},
|
||||
journal={npj Quantum Information},
|
||||
volume={2},
|
||||
number={1},
|
||||
pages={1--8},
|
||||
year={2016},
|
||||
publisher={Nature Publishing Group}
|
||||
}
|
||||
|
||||
@InProceedings{huang2017,
|
||||
author="Huang, Xiaowei
|
||||
and Kwiatkowska, Marta
|
||||
and Wang, Sen
|
||||
and Wu, Min",
|
||||
editor="Majumdar, Rupak
|
||||
and Kun{\v{c}}ak, Viktor",
|
||||
title="Safety Verification of Deep Neural Networks",
|
||||
booktitle="Computer Aided Verification",
|
||||
year="2017",
|
||||
publisher="Springer International Publishing",
|
||||
address="Cham",
|
||||
pages="3--29"
|
||||
}
|
||||
Loading…
Reference in New Issue