2019-10-23 19:24:45 +08:00
% !TEX root = main.tex
2019-12-04 17:32:33 +08:00
\section { 概述}
%概念的界定，怎么展开
软件工程师在开发软件系统时，不可避免地要用到某种程序设计语言。顾名思义，程序设计语言\index { 程序设计语言} 是程序员用来描述程序行为的语言。一般来说， ， ， ， ， ， ： \# 、JavaScript、PHP等。Sebesta~\cite { sebesta2012concepts} 从高级语言机制的设计角度对程序设计语言进行了深入细致的介绍和比较。大多数新程序设计语言的创建都受以前语言概念的启发，而新出现的程序设计语言往往通过规则的简化，使程序员的工作变得更加简单。
2019-10-23 19:24:45 +08:00
%程序设计语言的定义可分为语法、语义等方面。语义表示程序的含义，由静态语义和动态语义组成。静态语义指程序编译时可以确定的语法成分的含义；建立在转换/迁移系统上的动态语义则描述程序如何执行。
2019-12-08 15:01:16 +08:00
%
2019-10-23 19:24:45 +08:00
\section { 程序设计语言}
在计算机发展的早期，人们往往是用二进制(0/1序列)给计算机发指令。这显然很不方便。后来，逐渐出现了汇编语言\index { 汇编语言} 以及各种高级语言。一般来说，提高软件开发本身的效率与质量需要更抽象更高级的程序设计语言；而提高现实计算机硬件系统的利用率和执行效率，则需要使用较低级的程序设计语言，这样程序可以更直接地控制硬件资源。较通用的程序设计语言适用于广泛的应用领域和应用场景，可吸引大量的语言使用者，积累充足的遗产代码，便于培训与推广共享资源；但高度通用的语言设计上难以兼顾开发效率与执行效率。很多针对特定应用领域的程序设计语言更容易通过合适的语言机制同时改善软件开发与执行的效率。多样化的编程接口具有程序设计语言功能，但缺乏相应的编程框架甚至程序库等。这类接口反映了相应的编程模型的特点，实质上起到了程序设计语言的作用。
2019-12-04 17:32:33 +08:00
程序设计语言的发展因计算机系统发展的驱动和行业应用需求发展的推动，不同语言不同程度地受这些因素推动。新出现的程序设计语言通常是应对新兴应用或者新兴计算机体系结构的需要。但从程序设计语言发展历史角度看，应用需求的影响明显处于主导地位。
2019-10-23 19:24:45 +08:00
\subsection { 语言的设计、实现及生命期}
\subsubsection { 设计}
2019-12-04 17:32:33 +08:00
一般说来，程序语言的设计应该遵守以下原则\footnote { http://people.cs.aau.dk/$ \sim $ bt/DAT5E07/PrgLDesign.pdf} ：
2019-10-23 19:24:45 +08:00
\begin { itemize}
\item 可读性：能够很容易的理解；
\item 可写性：能够清晰、准确地表达计算意图；
\item 可靠性：确保程序不会导致意外；
\item 正交性(Orthogonality)：每种语言构造的组合都是合法的；
\item 一致性：相似的特点有相似的表示和行为；
\item 可维护性：能够很容易发现错误并纠正；
\item 通用性：若干结构可以组合成更通用的结构；
\item 可扩展性：能够给用户提供加入新结构的机制；
\item 标准化性(Standardability)：允许程序在不同机器和系统间的移植；
\item 可实现性：能够编写对应的转换器\index { 转换器} 或解释器\index { 解释器} 。
\end { itemize}
语言设计在实践中有三个角度： ， ； ， ；
某些语言如数据库查询语言SQL简洁地表示数据表格间的代数关系\index { 代数关系} ，大幅简化了对数据库\index { 数据库} 的查询；深度学习编程框架\index { 编程框架} TensorFlow~\cite { abadi2016tensorflow} 、PyTorch等辅助编程者方便地生成神经网络结构\index { 神经网络结构} 并根据学习算法自动生成反向网络。这些语言或框架追求编程简单性，虽然简化了循环和递归这样的图灵可计算性的关键语句，但仍然反映了一定的程序设计模型\index { 程序设计模型} 。
\subsubsection { 实现}
2019-12-04 17:32:33 +08:00
语言的传统实现方式分为从高级语言\index { 高级语言} 到机器代码\index { 机器代码} 的静态编译与直接对高级语言程序解释执行\index { 解释执行} 两种方式。如果存在中间语言，在不同层次可能分别采用不同方式混合实现，如避免在运行时的编译性能消耗和内存消耗的运行前编译(Ahead of Time， \index { 运行时编译} (Just-in-time， \index { 静态程序分析} 均在编译阶段实施；另一方面，代码生成过程中的优化技术是对程序员屏蔽硬件复杂性的主要手段。
2019-10-23 19:24:45 +08:00
近年来，随着计算机系统结构\index { 计算机系统结构} 的多样化和复杂化，程序设计语言出现了许多新的形式。例如，并行编程模型\index { 并行编程模型} OpenMP使用预编译制导语句插在C或Fortran的代码中， ， ，
通用语言的程序可以像OpenMP那样插入新的语言机制的语句， ， ， ， ， ，
\subsubsection { 发展}
\begin { figure} [htbp]
\centering
2019-12-04 17:32:33 +08:00
\includegraphics [width=0.95\textwidth] { fig1-2/2-1.png}
2019-10-23 19:24:45 +08:00
\caption { 常见程序设计语言的发展脉络
\label { fig:2-1} }
\end { figure}
自20世纪60年代以来的发展历程看， ：
\begin { enumerate} [1)]
\item 机器语言\index { 机器语言} ： ， ，
\item 汇编语言\index { 汇编语言} ：汇编语言指令可以直接访问系统接口。由汇编程序翻译成的机器语言程序效率高。但同样难以使用与维护。
\item 高级语言：它是面向用户的，独立于计算机种类与结构。因此易学易用，通用性强，应用广泛。图\ref { fig:2-1} 给出了常见高级程序设计语言的发展脉络\footnote { https://exploring-data.com/vis/programming-languages-influence-network/} ，其中箭头指向的程序设计语言借鉴了前驱的设计思想。
2019-12-04 17:32:33 +08:00
\item 声明式语言\index { 非过程化语言} ：使用这种语言编码时只需说明“做什么”，不需描述算法细节。数据库查询语言是其中的一种，用户可以对数据库中的信息进行复杂的操作。
2019-10-23 19:24:45 +08:00
\end { enumerate}
2019-12-04 17:32:33 +08:00
在程序设计语言发展最初阶段，程序设计语言按照主要编程范型\index { 编程范型} ，可以被归类为过程式、面向对象、函数式~\cite { hu2015functional} 等。随着C++、C\# 等语言的出现，传统分类之间的界限逐渐变得模糊。现代的编程语言往往具有若干种类编程语言的元素，这就是所谓的多范型编程语言。而多范型程序设计语言\index { 多范型程序设计语言} 也是一个越来越明显的趋势。
2019-10-23 19:24:45 +08:00
一个成功的程序设计语言从探索到推广、接受和最终成为行业标准往往经历以下四个阶段：第一阶段，新兴应用与系统的软件开发在早期开发过程只能采用已有的程序设计语言配以一定的软件工程方法；第二阶段，为提高软件生产率，多种语言工具开始出现；第三阶段，行业标准的形成有助于积累遗产代码资源和培训与推广资源；第四阶段，随着大量遗产代码开始积累，行业商业模式成型，倾向于使用成熟的程序设计语言。分析程序设计语言所处的发展阶段有助于我们了解甚至预测其发展规律。
\subsection { 应用驱动的程序设计语言发展}
\begin { figure} [htbp]
\centering
2019-12-04 17:32:33 +08:00
\includegraphics [width=0.99\textwidth] { fig1-2/2-2.png}
2019-10-23 19:24:45 +08:00
\caption { 程序设计语言的发展及分类}
\label { fig:2-2}
\end { figure}
2019-12-04 17:32:33 +08:00
%这里以多个有代表性的语言为例，分析其应用背景、设计特点与发展规律，从而展现程序设计语言发展的历史与现状。
按照程序设计语言的类型与应用，图\ref { fig:2-2} 给出了以时间为主线的不同类别语言的发展过程与分类关系。从不同角度来看，一种程序设计语言既可能属于系统编程语言，又是面向对象语言。从发展过程来看，一种语言在发展过程中会不断进行扩充，融入不同的范型，进而趋近于多范型语言。计算机产业的发展往往是新的产业应用从已有的应用模式中成长出来而不是取而代之。新语言的出现往往标志着信息技术在新的应用领域的扩张。本节主要以应用驱动来组织。
2019-10-23 19:24:45 +08:00
\begin { itemize}
2019-12-04 17:32:33 +08:00
\item 科学与工程计算(1954$ \sim $ )
2019-10-23 19:24:45 +08:00
\end { itemize}
早期计算机系统硬件结构简单， ， ， ， ， ， ，
2019-12-04 17:32:33 +08:00
早期语言的准确语义往往依赖于编译器的实现， ， ， ， ，
2019-10-23 19:24:45 +08:00
科学与工程性质的计算， ， ， ， ， ，
\begin { itemize}
2019-12-04 17:32:33 +08:00
\item 商用计算(1960$ \sim $ )
2019-10-23 19:24:45 +08:00
\end { itemize}
信息技术的应用逐渐从专业领域扩展到广阔的商业领域信息化。COBOL语言的出现标志着商业化的事务处理如金融、财会有了强有力的语言技术支持。该时期计算系统往往是大型机或小型机服务器。COBOL拥有庞大的用户群， \footnote { http://cobolcowboys.com/cobol-today/} 。由于商业计算的多样性， ， ， ， ， \index { 过程式语言} 的PASCAL语言则是由程序设计语言理论研究者设计的更加安全和规范的语言。数据库查询语言\index { 数据库查询语言} SQL是较早出现的领域专用语言。它不具有完整的程序设计语言功能， \index { 关系数据库} 应用的编程模型。
随着商用计算而来的是软件大规模化。1960年代末出现了一系列旨在有效控制大规模软件开发过程复杂性的程序设计思想。面向对象的思想及其第一个语言Simula 67试图对不同程序模块访问共享变量的方式进行限制， \index { 结构化程序设计} 思想~\cite { dijkstra1968go} ，对程序的控制流进行限制。
\begin { itemize}
2019-12-04 17:32:33 +08:00
\item 人工智能(1960$ \sim $ )
2019-10-23 19:24:45 +08:00
\end { itemize}
2019-12-04 17:32:33 +08:00
人工智能\index { 人工智能} 自诞生以来， ， ， ，
2019-10-23 19:24:45 +08:00
2019-10-30 15:12:58 +08:00
符号主义就是以符号逻辑系统\index { 符号逻辑系统} 为基础来表示知识。二十世纪七十年代， ， ， ， \cite { Tang2002} 。
2019-10-23 19:24:45 +08:00
连接主义的代表是试图模拟人脑的人工神经网络。近十年来， ， ，
\begin { itemize}
2019-12-04 17:32:33 +08:00
\item 个人计算与系统编程(1981$ \sim $ )
2019-10-23 19:24:45 +08:00
\end { itemize}
在摩尔定律背景下， ， ， ， ，
2019-12-04 17:32:33 +08:00
作为一种新的多范型语言， ， ， ， ，
2019-10-23 19:24:45 +08:00
\begin { itemize}
2019-12-04 17:32:33 +08:00
\item Web服务与移动计算(1990$ \sim $ )
2019-10-23 19:24:45 +08:00
\end { itemize}
伴随互联网的出现， ， ， ， ， ，
1990年代后智能手机的出现与普及将计算拓展到个人随身携带的新模式。一些为Web服务设计的语言仍然适用， ， ，
\begin { itemize}
2019-12-04 17:32:33 +08:00
\item 大数据分析与处理(2004$ \sim $ )
2019-10-23 19:24:45 +08:00
\end { itemize}
平台系统的大规模数据分析与处理需求，首先来自于互联网的搜索服务。其特点是大量采集的数据需要多台服务器的集群通过并行计算高速处理。分布式并行计算带来了性能优化与可靠性的挑战。但是，在平台建设期无法预知随时可能出现的各种数据分析需求。应用开发人员需要随时针对应用需求快速、灵活地编程，而不必为系统级的性能与可靠性问题所困扰。
设计易用而且高效的并行程序设计语言， \cite { lammel2008google} ， ， \index { 分布式操作系统} 角色的运行时系统负责执行。Hadoop和Spark是基于MapReduce的主要开源工具。尽管此类语言工具不具有独立的语法系统， ，
%增加语言的专用性有助于在保证易编程性的前提下优化性能，但如果一个编程模型不能涵盖同一应用领域多种相互联系的计算需求，其专用性会影响行业标准的形成。
%%to be confirmed
%基本的Map与Reduce命令还不能涵盖一般的并行计算步骤的数据依赖关系。
\begin { itemize}
2019-12-04 17:32:33 +08:00
\item 互联网金融(2009$ \sim $ )
2019-10-23 19:24:45 +08:00
\end { itemize}
2019-10-30 15:12:58 +08:00
以软件为核心的互联网金融指的是以互联网为载体的金融服务形式， ， ，
2019-10-23 19:24:45 +08:00
\section { 程序理论}
2019-12-04 17:32:33 +08:00
程序设计语言都具有语法和语义。语义表示程序的含义。程序理论涵盖程序设计语言的设计、实现，以及程序正确性的分析方法等。本节将介绍程序设计语言的语法与语义基础，并给出描述程序设计规范的形式化方法，如图\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}
2019-10-23 19:24:45 +08:00
\subsection { 程序设计语言的词法与语法}
2019-12-04 17:32:33 +08:00
程序设计语言都有自己的词法和语法，而词法和语法的定义是一系列规则的集合，这些规则的基础就是形式语言。文法\index { 文法} 是形式语言中十分重要的基本概念，是描述语言的语法结构的一组形式规则。文法有四种分类，其中最常用的为正则语言\index { 正则语言} 和上下文无关语言\index { 上下文无关语言} 。正则语言可以用正规式定义，上下文无关语言可以用上下文无关文法(元素和规则的集合)定义。程序设计语言中的大多数算术表达式可用上下文无关文法\index { 上下文无关文法} 生成。正则语言是最简单的语言类，是上下文无关语言类的一个真子类。对程序设计语言编写的程序进行分析和处理(编译)时，需要判断对应的句子是否合法，可以通过对应语言的自动机进行判断。自动机是语言的另一种表示方法。其中，正则语言可以转换成有限状态自动机\index { 有限状态自动机} 、上下文无关语言可转换成下推自动机\index { 下推自动机} 表示，反之亦然。针对某种特定输入的一系列有限的规则，对不同的输入元素，自动机依据自身的状态会做出不同的响应，最后达到某种特定的状态。
2019-10-23 19:24:45 +08:00
\subsection { 程序设计语言的类型系统}
2019-12-04 17:32:33 +08:00
在很多程序设计语言中，变量与数据是带类型的；而类型之间有一定的关联。人们在研究程序设计语言理论时，可以借鉴类型论\index { 类型论} (Type theory, 也称“类型理论”)来研究程序设计语言的类型系统\index { 类型系统} 。类型论是数理逻辑中的一个分支，其中的马丁洛夫类型理论用规则来刻画类型及行为，是程序构造的形式理论。类型理论\index { 类型理论} 研究的是程序设计语言的类型系统，用于定义如何将编程语言中的数值和表达式等短语归类为许多不同的类型，如何操作这些类型，这些类型如何互相作用。类型通过预测程序部件的某些执行行为来协调这些部件间的交互。在类型化的程序设计语言中，语言构造分为引入和消去两种形式。类型的引入形式确定该类型的值或范型，而消去形式则确定如何操作该类型的值以形成另一种（可能是相同的）类型的计算。例如，可以使用类型系统中的归纳类型定义如自然数、表、树等数据结构\index { 数据结构} ；使用多态类型处理程序的特定型与参数型这些不同的输入类型；使用记录类型定义一组记录的命名类型等；自然数类型的引入形式是自然数，消去形式是加法和乘法等。
2019-10-23 19:24:45 +08:00
\subsection { 程序的语义}
给定一个程序，如何判断它是否正确？这是很早以前人们就关注的问题。简单来说，如果一个程序恰当地实现了设计者与用户的意图，它就是正确的。严格意义上，程序的正确性~\cite { turing1989checking} 需要数学证明，不仅需要形式描述设计者与用户的意图，而且要形式描述程序的含义，并推导程序的行为满足设计者与用户的意图。程序含义的形式化描述就是形式语义学。基于形式语义，不仅可以构建描述程序含义的基础，还可以用于验证程序的正确性。
程序设计语言的语法是符号化的，语义是该语言程序所描述的计算或过程。根据语义，程序设计语言的解释器或编译器可以将该语言程序编译成计算机可处理的机器语言程序。在程序设计语言的早期，人们使用自然语言解释语义。这种自然语言解释的语义不精确、有歧义，无法分析和证明程序的正确性。为了提高程序设计语言的可理解性、支持语言标准化、指导语言设计、辅助编译器开发、证明程序的性质和程序之间的等价性，需要对程序设计语言的语义进行抽象，给出严格的定义。为此，人们开始研究使用数学结构定义程序设计语言的语义，并扩展出各类形式规约(Specification)语言~\cite { Wang2019} ，形成了形式语义学\index { 形式语义学} ~\cite { Zhou2018} 。
它的基本方法是用一种元语言将程序加工数据的过程及其结果形式化，从而定义程序的语义。根据所用数学工具和研究重点，形式语义学可分为操作语义、公理语义、代数语义和指称语义四大类。
\begin { itemize}
\item 操作语义
\end { itemize}
2019-10-30 15:12:58 +08:00
操作语义(Operational Semantics)\index { 操作语义} 使用结构化的归约规则，着重描述程序运行中变量赋值的变化、行为的变迁。它将语言中各个成分翻译成计算机系统中相应的一组操作。目前最为常见的操作语义是标号迁移系统\index { 标号迁移系统} (Labeled Transition System， ， ， ， ， ； ， ， \{ x++;\} 的操作语义为：
2019-10-23 19:24:45 +08:00
\lstset { language=C}
\begin { lstlisting}
loop: if (x>=y) goto out;
if (x<y) { x=x+1; goto loop;}
out: …
\end { lstlisting}
其中， ，
在由操作语义描述的串行程序的语义中，状态是一些简单的数据结构，迁移规则一般都是确定的、离散的，也不需要考虑标号间的通信和同步。为了定义复杂程序的操作语义，例如面向对象程序、并发程序、实时程序、概率程序\index { 概率程序} 、混成系统\index { 混成系统} 等，人们对迁移系统进行了各种扩充，或扩充它的状态，或扩充它的迁移关系，亦或两者同时扩充。例如，为了定义面向对象程序，人们对程序状态进行扩充，引入堆和栈等复杂数据结构；为了处理并发程序，人们对标号迁移关系进行扩充，使用标号描述通信和同步；为了描述概率和随机程序\index { 随机程序} ，允许以给定的概率或者随机选取迁移规则等。
基于抽象机的操作语义可描述实现方面的执行细节，操作性比较强，适合于语言编译器的开发与编译的优化。操作语义中的状态是显式的、可操作的。因此，在基于状态搜索的模型检验\index { 模型检验} 方法中，操作语义比较适合描述模型的语义，即状态的变化序列。然而，抽象机上的推理系统比较弱，不易对大规模或无穷状态的系统进行基于演绎推理\index { 演绎推理} 的形式验证。
\begin { itemize}
\item 公理语义
\end { itemize}
2019-10-30 15:12:58 +08:00
公理语义(Axiomatic Semantics)\index { 公理语义} 运用数学中的公理化方法给出计算机语言的语义。
2019-10-23 19:24:45 +08:00
%程序的语义不仅可以使用操作语义描述，还可以使用形式逻辑来描述。而形式逻辑是公理语义(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\} }
\]
来规定顺序语句的语义。该推理规则表示当横向上方的命题都成立时，则横线下方的命题也成立。
%若条件语句if(y==1) then x=1; else x=2; 的前置断言为\{y==1\}，则该语句执行后，后置断言为\{x==1\}。
在该形式系统中可以直接进行程序性质的规约和验证。程序逻辑的表达能力、可靠性、完备性以及可判定性都可归结为数理逻辑上的元性质，程序逻辑的解释模型通常就是程序设计语言的指称语义或操作语义。
2019-10-30 15:12:58 +08:00
常见的公理语义有基于一阶逻辑\index { 一阶逻辑} 扩展的Floyd-Hoare 逻辑\index { Floyd-Hoare 逻辑} ~\cite { Hoare1969} 、谓词转换器(Predicate Transformer)等。其中，
2019-12-04 17:32:33 +08:00
Floyd-Hoare 逻辑最初是面向串行程序\index { 串行程序} 的，并扩展至并发程序、实时系统\index { 实时系统} 、混成系统甚至量子系统\index { 量子系统} 等。针对指针程序\index { 指针程序} 和面向对象程序， ， \index { 程序验证} 。公理语义在形式验证中应用比较多。
2019-10-23 19:24:45 +08:00
\begin { itemize}
\item 代数语义
\end { itemize}
2019-10-30 15:12:58 +08:00
面向对象程序设计语言具有抽象数据类型、多态性等特点。在抽象数据类型的基础上发展起来的代数语义(Algebraic Semantics)\index { 代数语义} ，用代数方法研究计算机语言的语义。它把程序设计语言形式地定义为满足某种公理体系的抽象代数结构，然后利用这种代数结构的性质来证明用该语言编写的程序的正确性。
2019-10-23 19:24:45 +08:00
抽象数据类型\index { 抽象数据类型} 将数据对象及对象上的操作封装、数据类型的特性与实现分离，具有模块化和可复用的性质。它与软件开发过程匹配比较自然，因此也可以用于程序的自动构造：首先设计较小的抽象数据类型，然后逐步扩充形成较大的抽象数据类型体系；这个过程中，抽象数据类型间可讨论层次一致和充分完备等性质。
\begin { itemize}
\item 指称语义
\end { itemize}
2019-10-30 15:12:58 +08:00
指称语义(Denotational Semantics)\index { 指称语义} 关注代表程序所做所为的数学对象，用数学对象上的运算来定义语言的语义。建立指称语义首先要确定程序设计语言的解释域(论域理论)。论域理论是指称语义的数学基础，讨论各种语言成分的指称(意义)的数学结构，并在各种数学结构之上定义语言语义，推导语言成分特性。例如，将程序设计语言的基本语法实体的指称定义为程序状态空间上的函数和泛函，复合语法实体的指称由构成它的子成分的指称复合得到。基于指称语义的相关理论，可以推导不同语言形式语义间的关系，也可以分析同一语言不同语义间的转换关系。%其中，基于一阶关系演算的程序统一理论(unifying theories of programming，
2019-10-23 19:24:45 +08:00
2019-12-04 17:32:33 +08:00
\subsection { 程序的规约}
2019-10-23 19:24:45 +08:00
%基于程序逻辑系统的性质规约刻画了所期望的系统行为，这些性质是通过逻辑公式来描述的。
直接使用程序设计语言及其语义，难以描述和证明软件从需求文档到程序代码的开发过程各阶段创建的不同抽象层次的制品及其正确性。针对这一问题，人们开始研究高层抽象的形式规约语言的设计。形式规约语言\index { 形式规约语言} 是指由严格的递归语法规则所定义的语言，满足语法规则的句子称为合式或良构(Well-formed)规约。
2019-10-30 10:38:02 +08:00
串行程序设计早期的程序逻辑是Floyd-Hoare逻辑。通过在一阶谓词系统基础上添加关于程序的公理和推理规则， ， ， ， ， ， \index { 不变式} (Invariance)规则替换为框架(Frame)规则。
2019-10-23 19:24:45 +08:00
并发程序的规约在Floyd-Hoare 逻辑的基础上， ， ， %除了这些针对串行一致性内存模型上的并发程序的程序逻辑外， ， （ ）
Floyd-Hoare逻辑中， ， ， $ \mu $ -演算。作为模态$ \mu $ -演算的真子集，
%形式规约可以自顶向下逐步精化形成软件开发的规约序列， ， ，
%20世纪七十年代后，
2019-12-04 17:32:33 +08:00
%\vspace{5pt}
\subsection { 程序设计理论框架}
2019-10-23 19:24:45 +08:00
不同的形式语义有各自特点与适用范围。学者们试图在这些语义的基础上构建一个统一的理论。
%软件工程界认识到数学可以为程序正确性保证提供技术基础。
相应的出现了一些程序设计理论框架。例如， ， ， \index { XYZ系统} ~\cite { Tang2002} 。Joseph A. Goguen 和Rod M. Burstall提出了一种抽象模型理论， \cite { Goguen92} 。 C.A.R. Hoare和何积丰提出了统一程序设计理论框架UTP， \cite { hoare1998unifying} 。
\section { 程序正确性构造}
基于形式语义，我们可以确保程序的正确性，有两类方法，一类是先编写程序，再按照规约{ \bf { 验证} } 它的正确性 ； （ ） ， { \bf { 综合} } 与{ \bf { 精化} } ， %程序的正确性分析存在不同的方法
如图\ref { fig:2-3} 所示。%,程序的正确性分析过程可以通过构建程序需满足的性质到规约的映射，程序行为与形式语义的映射，再使用相应的形式化分析方法实现。
\begin { figure} [htbp]
\centering
\includegraphics [width=0.50\textwidth] { fig1-2/2-3.png}
\caption { 程序的形式化分析方法
\label { fig:2-3} }
\end { figure}
\subsection { 程序的分析与验证}
2019-10-30 15:12:58 +08:00
定理证明（ ） （ ） %， ， ； ； ；
2019-10-23 19:24:45 +08:00
\begin { itemize}
\item 定理证明\index { 定理证明}
\end { itemize}
这类方法将程序正确性验证问题看成是数学定理证明，试图通过严格的逻辑推导来验证程序是否满足规约。
%基于定理证明的验证大部分是以程序逻辑为理论基础的。除此以外，我们还可以基于程序的操作语义，直接表达程序执行的安全性、正确性等各种性质，并证明相关定理。
对串行程序进行验证， ， ， %另一个方面的工作使用关系型程序逻辑验证两个程序之间的关系，或者一个程序在两种输入下的行为之间的关系。前者可用于程序精化的验证，而后者则可用于信息安全性质，如信息流控制(information flow control)机制的验证。
2019-10-31 16:31:16 +08:00
基于定理证明的验证工具可以分为两类，即基于自动定理证明器的自动验证和基于人机交互的半自动验证。常见的程序自动证明器(Program Verifier)， ， ， ， ， ， ， ， ， ，
2019-10-23 19:24:45 +08:00
近期提出的K框架提供了基于重写的语言~\cite { Rosu15} ， ， ， （ ）
目前， ， ， ， ， ， ， ， ， ，
\begin { itemize}
\item 软件模型检验
\end { itemize}
%由Edmund M. Clarke、E. Allen Emerson和Joseph Sifakis提出的
2019-12-04 17:32:33 +08:00
模型检验\index { 模型检验} 方法通过自动遍历系统模型的有穷状态空间，来检验系统的语义模型与其性质规约之间的满足关系。软件系统属于无穷状态系统，即使状态有穷，其状态空间规模通常远超当前计算机可处理的范围。在硬件系统模型检验取得巨大成功的时候，软件模型检验所面临严峻的挑战。对于无穷状态系统，符号化可达性分析可能不终止。软件模型检验的核心问题是如何建立可检验规模的软件模型(抽象)。一种方法是采用上近似(Over-approximation或下近似(Under-approximation)对模型进行抽象，另一种方法是使用限界模型检验，将模型空间爆炸涉及的参数(例如循环次数、并发数等)限制在一定范围内，验证系统模型在此深度内是否满足系统规约。在软件模型检验中，利用静态分析、符号执行\index { 符号执行} 等方法抽取程序模型，以及基于路径的模型检验等静态和动态结合的方法，也是有效提高模型检验扩展性的重要途径。%近年来，将模型检验与定理证明有效地结合也是一个有前景的研究方向。
2019-10-23 19:24:45 +08:00
\subsection { 程序的自动综合}
按照某种形式规约表达的用户意图，程序综合\index { 程序综合} 能够使用指定的编程语言自动生成符合规约的程序代码。程序综成器通常在程序空间上执行某种形式的搜索，以生成与各种类型一致的程序约束(例如输入输出示例，演示，自然语言，部分程序和断言)。程序综合是编程理论中最核心的问题之一~\cite { pnueli1989synthesis} 。早期的想法是通过组合子问题生成带有证明的、可解释的实现。一个分支是使用定理证明器首先证明用户提供的规约，再使用这个证明提取相应的程序逻辑。而另一个较为流行的方法是从一个高层规约开始，不断的进行转换，直到实现目标程序。近期的程序综合方法中，用户提供规约的同时，还可以提供目标程序的语法。这样使得基于语法结构进行的综合过程更加高效，得到的程序的可解释性更高。
\subsection { 程序的精化}
程序精化\index { 程序精化} 是将抽象（ ） （ ） ， （ ） ， ， ，
2019-12-04 17:32:33 +08:00
\section { 本章小结}
开发软件，离不开程序设计语言。
在计算机发展的不同阶段，为了应对一些典型应用，各种不同的程序设计语言应运而生。
第一， ， ， ； ， （ ） ， （ ） ； ， ， ； ， ， ， ， ， ， ， ； ， ； ， ， ； ， ， ， ，
正是由于在程序设计语言和相关理论领域的先驱工作，
2019-10-23 19:24:45 +08:00
%\section{参考文献}
%
%\begin{itemize}
% \item [] [1]. Sebesta R.W. Concepts of Programming Languages. (7th ed.) Pearson, 2006.
% \item [] [2]. Abadi M. et al. TensorFlow: A System for Large-Scale Machine Learning. Proc. OSDI 2016: 265-283.
% \item [] [3]. Hu Z, Hughes J, Wang M. How functional programming mattered, National Science Review, Oxford Journal, 2015, 2(3):349-270.
% \item [] [4]. Dijkstra E.W. Go To Statement Considered Harmful. Communications of the ACM. 11(3): 147-148, 1968.
% \item [] [5]. 唐稚松等. 时序逻辑程序设计与软件工程. 科学出版社, 2002.
% \item [] [6]. L?mmel R. Google's MapReduce programming model — Revisited. Science of Computer Programming. 70: 1-30, 2008.
% \item [] [7]. Turing A. Checking a large routine. Report of a Conf. on High Speed Automatic Calculating Machines, Cambridge University Math. Lab., 1949. 67~69.
% \item [] [8]. 王戟,詹乃军,冯新宇,刘志明.形式化方法概貌.软件学报,2019,30(1):33-61
% \item [] [9]. 周巢尘，詹乃军. 形式语义学引论(第二版). 科学出版社, 2018.
% \item [] [10]. Hoare CAR. An axiomatic basis for computer programming. Communications of the ACM, 1969,12(10):576-580.
% \item [] [11]. Ro?u, Grigore. From rewriting logic, to programming language semantics, to program verification. Logic, Rewriting, and Concurrency. Springer, Cham, 2015. 598-616.
% \item [] [12]. Goguen JA, Burstall RM. Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery, 1992,39(1):95-146.
% \item [] [13]. Hoare CAR, He J. Unifying Theories of Programming. Prentice Hall, 1998,14:184-203.
% \item [] [14]. Amir Pnueli and Roni Rosner. On the synthesis of a reactive module. In POPL, 1989:179–
2019-10-14 15:05:49 +08:00
%\end{itemize}
