software-strategy-1/Ch1-2-ProgrammingLanguage.tex

% !TEX root =  main.tex
\section{引言} 
	
软件工程师在开发软件系统时，不可避免地要用到某种程序设计语言。顾名思义，程序设计语言是程序员用来描述程序行为的语言。在计算机科学领域，曾出现过数百种程序设计语言。TIOBE给出目前常用程序设计语言的流行度排序，从高到低有：Java、C、Python、C++、C\#、JavaScript、PHP等[23]。Sebesta[1]从高级语言机制的设计角度对程序设计语言进行了深入细致的介绍和比较。大多数新程序设计语言的创建都受以前语言概念的启发。较旧的语言仍然是新语言的坚实基础，而新出现的程序设计语言使程序员的工作变得更加简单。

程序设计语言的定义可分为语法、语义等方面。语义表示程序的含义，由静态语义和动态语义组成。静态语义指程序编译时可以确定的语法成分的含义；建立在转换/迁移系统上的动态语义则描述程序如何执行。
	
\section{程序设计语言}

在计算机发展的早期，人们往往是用二进制(0/1序列)给计算机发指令。这显然很不方便。后来，逐渐出现了汇编语言以及各种高级语言。一般来说，提高软件开发本身的效率与质量需要更抽象更高级的程序设计语言；而提高现实计算机硬件系统的利用率和执行效率，则需要使用较低级的程序设计语言，这样程序可以更直接地控制硬件资源。较通用的程序设计语言适用于广泛的应用领域和应用场景，可吸引大量的语言使用者，积累充足的遗产代码，便于培训与推广共享资源；但高度通用的语言设计上难以兼顾开发效率与执行效率。很多针对特定应用领域的程序设计语言更容易通过合适的语言机制同时改善软件开发与执行的效率。多样化的编程接口具有程序设计语言功能，但缺乏相应的编程框架甚至程序库等。这类接口反映了相应的编程模型的特点，实质上起到了程序设计语言的作用。

程序设计语言的发展既要遵循自身理论与模型的内在规律，也受到计算机系统发展的驱动和行业应用需求发展的推动。不同语言不同程度地受这些因素推动。但从程序设计语言发展历史角度看，应用需求的影响明显处于主导地位。新出现的程序设计语言通常是应对新兴应用或者新兴计算机体系结构的需要。

\subsection{语言的设计、实现及生命期}
\subsubsection{设计}
一般说来，程序语言的设计应该遵守以下原则：能够很容易的理解；能够清晰、准确地表达计算意图；确保程序不会导致意外；每种语言构造的组合都是合法的；相似的特点有相似的表示和行为；能够很容易发现错误并纠正；能够给用户提供加入新结构的机制；允许程序在不同机器和系统间的移植；能够编写对应的转换器或解释器。 

语言设计在实践中有三个角度：从程序设计语言理论角度出发设计的语言如Pascal、Ocaml、X10等十分关注语言语义的清晰性、灵活性、简洁性，往往直接反映了理论领域的创新成果；从系统软件与体系结构角度出发设计的语言如图形处理器支持的CUDA，关注如何充分利用系统结构的特点来优化性能；从应用角度出发设计的语言如XML、PHP、Julia等关注与目标应用的契合度以及编程的便易性。

某些语言如数据库查询语言SQL简洁地表示数据表格间的代数关系，大幅简化了对数据库的查询；深度学习编程框架TensorFlow[5]、PyTorch等辅助编程者方便地生成神经网络结构并根据学习算法自动生成反向网络。这些语言或框架追求编程简单性，虽然简化了循环和递归这样的图灵可计算性的关键语句，但仍然反映了一定的程序设计模型。

\subsubsection{实现}

语言的传统实现方式分为从高级语言到机器代码的静态编译与直接对高级语言程序解释执行两种方式。如果存在中间语言，在不同层次分别可能采用不同方式混合实现，如避免在运行时的编译性能消耗和内存消耗的运行前编译(ahead of time，简称为AOT)与根据当前硬件情况实时编译生成机器指令的运行时编译(just-in-time，简称为JIT)。编译技术仍然是语言实现的关键技术。一方面类型检查等静态程序分析均在编译阶段实施，另一方面代码生成过程中的优化技术是对程序员屏蔽硬件复杂性的主要手段。

近年来，随着计算机系统结构的多样化和复杂化，程序设计语言出现了许多新的形式。例如，并行编程模型OpenMP使用预编译制导语句插在C或Fortran的代码中，描述了多线程并行。尽管OpenMP本身不具有完整的独立语法，但因为反映了与串行C语言不同的共享变量式并行编程模型，我们也可以称之为新的“语言”或者至少是新的“语言机制”。

通用语言的程序可以像OpenMP那样插入新的语言机制的语句，也可以反过来在新风格的程序中插入通用语言的子程序。这一方式在大数据处理编程框架MapReduce、Hadoop、Spark中得以应用，不仅简化了分布式并行数据处理编程，而且允许程序员设计灵活高效的程序用于数据处理。一些编程模型的实现甚至不引入任何新的语法扩展，仅仅以子程序库的形式出现。比如，科学计算中广泛使用的MPI由C和Fortran程序库实现，支持多种形式的消息传递通讯。
	
\subsubsection{发展}

\begin{figure}[htbp]
	\centering	
	\includegraphics[width=0.80\textwidth]{fig1-2/2-1.png}
	\caption{常见程序语言的发展脉络
	\label{fig:2-1}}
\end{figure}

自20世纪60年代以来的发展历程看，程序设计语言的抽象级别显著提高。历史上曾出现过将程序设计语言分为四代的提法：

\begin{enumerate}[1)]
	\item 机器语言：由二进制0、1代码指令构成，不同的处理器具有不同的指令系统。由于机器语言难编写和维护，人们已很少直接使用这种语言。
	\item 汇编语言：汇编语言指令可以直接访问系统接口。由汇编程序翻译成的机器语言程序效率高。但同样难以使用与维护。
	\item 高级语言：它是面向用户的，独立于计算机种类与结构。因此易学易用，通用性强，应用广泛。图\ref{fig:2-1}给出了常见高级程序设计语言的发展脉络，其中箭头指向的程序设计语言借鉴了前驱的设计思想。
	\item 非过程化语言：使用这种语言编码时只需说明“做什么”，不需描述算法细节。数据库查询语言是其中的一种，用户可以对数据库中的信息进行复杂的操作。
\end{enumerate}

在程序设计语言发展最初阶段，程序设计语言按照主要编程范式，可以被归类为面向过程式的、面向对象式的、逻辑式的、函数式[22]的等。随着C++、C\#等语言的出现，传统分类之间的界限逐渐变得模糊。现代的编程语言往往具有若干种类编程语言的元素，这就是所谓的多范式编程语言。而多范式程序设计语言也是一个越来越明显的趋势。

一个成功的程序设计语言从探索到推广、接受和最终成为行业标准往往经历以下四个阶段：第一阶段，新兴应用与系统的软件开发在早期开发过程只能采用已有的程序设计语言配以一定的软件工程方法；第二阶段，为提高软件生产率，多种语言工具开始出现；第三阶段，行业标准的形成有助于积累遗产代码资源和培训与推广资源；第四阶段，随着大量遗产代码开始积累，行业商业模式成型，倾向于使用成熟的程序设计语言。分析程序设计语言所处的发展阶段有助于我们了解甚至预测其发展规律。

\subsection{应用驱动的程序设计语言发展}

\begin{figure}[htbp]
	\centering	
	\includegraphics[width=0.80\textwidth]{fig1-2/2-2.png}
	\caption{程序设计语言的发展及分类}
	\label{fig:2-2}
\end{figure}

这里以多个有代表性的典型语言为例，分析其应用背景、设计特点与发展规律，从而展现程序语言发展的现状、预测未来发展趋势。按照程序语言的类型与应用，图\ref{fig:2-2}给出了以时间为主线的不同类别语言的发展过程与分类关系。从不同角度来看，一种程序语言既可能属于系统编程语言，又是面向对象语言。从发展过程来看，一种语言在发展过程中会不断进行扩充，融入不同的范式，进而趋近于多范式语言。本节主要以应用驱动来组织。计算机产业的发展往往是新的产业应用从已有的应用模式中成长出来而不是取而代之。新语言的出现往往标志着信息技术在新的应用领域的扩张。
	
\begin{itemize}
	\item 科学与工程计算(1954~) 
\end{itemize}	

早期计算机系统硬件结构简单，软件专用性强，主要用于核反应计算、密码破译这样专业性强的科学与工程计算领域，直接服务对象往往是政府与军工。1956年发布的Fortran语言标志着具有完整工具链的程序设计语言出现。Fortran语言符合典型的过程式语言的特征，由从事系统结构和系统软件的研究人员设计，采取编译的方式实现，反映了程序设计与计算机系统之间的紧密联系。尽管串行的科学计算软件开发方法已成熟，积累的大量遗产代码保证了Fortran这样的语言在其适用领域仍然具有生命力。

早期语言的准确语义往往依赖于编译器的实现，针对特定体系结构由编译器的开发者设计。1950年代末期出现了一些由计算机逻辑理论与程序语义研究者设计和实现的程序设计语言，如ALGOL和LISP语言。此后出现的大量函数式语言如Haskell、ML往往具有清楚而简洁的数学表示，设计出发点上更多地考虑如何优美地表示计算，但由于缺乏工业级应用的针对性以及性能上对常见体系结构的适配性，其接受范围受到限制。

科学与工程性质的计算，尤其是高性能计算往往与计算机体系结构密切相关，发展了多种形式的编程接口。OpenMP是共享内存的并行计算所常用的编程接口。其特点是在C或Fortran中插入指导语句，希望不改变原有串行程序语义的条件下利用共享存储器的多线程并行加速计算。MPI是跨平台的消息传递通讯程序库，完全不增加额外的语法机制。图形处理器语言CUDA在C基础上扩展了一些语法机制，用以区分在CPU、GPU上运行的程序片段，作出不同的编译。并行程序设计模型一直是程序设计理论研究的一个重点 。

\begin{itemize}
	\item 商用计算(1960~) 
\end{itemize}

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

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

\begin{itemize}
	\item 人工智能(1960~) 
\end{itemize}

人工智能自诞生以来，广受关注。在该领域也出现了若干专用语言。人工智能有符号主义、连接主义等流派。

符号主义就是以符号逻辑系统为基础来表示知识。二十世纪七十年代，Robert Kowalski 等人提出了逻辑可以作为程序设计语言的基本思想，把逻辑和计算这两个截然不同的概念统一在一起。这就是逻辑程序设计(logic programming)，而Prolog语言就是典型的逻辑程序设计语言。对经典的逻辑程序设计语言，可以进行各种扩充。例如，将状态转移的控制机制引入到时序逻辑系统的XYZ/E是世界上第一个可执行的时序逻辑程序设计语言[9]。

连接主义的代表是试图模拟人脑的人工神经网络。近十年来，深度学习显示出了强大的学习能力和广泛的应用前景。TensorFlow、PyTorch等工具针对深度神经网络学习算法的特点，利用高级语言展开生成神经网络结构然后以高性能方式运行学习算法。这些多样的领域特定语言工具不具备完整的通用程序设计语言功能，但十分适合特定的应用场景。

\begin{itemize}
	\item 个人计算与系统编程(1981~) 
\end{itemize}

在摩尔定律背景下，计算机硬件系统的价格不断下降，个人使用计算机的情形越来越普遍。随个人计算而来的是软件的多样化，应用形式从事务处理和业务处理扩展到教育与娱乐。软件的开发与销售形式从硬件捆绑式发展到专业软件企业发行软件拷贝的销售形式。软件开发团队与人员的数目大量增加。C++是C语言的面向对象扩展，逐渐成为实施传统软件工程的主流语言。

作为一种新的多范式语言，Rust不仅能够提供友好的编译器和清晰的错误提示信息，而且速度快、内存利用率高，同时具有丰富的类型系统保证内存安全和线程安全。目前从初创公司到大型企业，已有很多公司都在使用 Rust，应用范围不仅包括嵌入式设备，也包括可扩展的 Web 服务。

\begin{itemize}
	\item Web服务与移动计算(1990~) 
\end{itemize}

伴随互联网的出现，Web服务软件一改拷贝销售形式，直接通过互联网向终端用户提供服务。其服务形式多样，方式多变。服务的反应速度往往受限于互联网的带宽与延迟，而不是计算的速度。因此，客户端与服务器端交互程序设计语言重点关注软件的开发效率，而不是程序的性能。典型的支持此类应用的脚本语言如JavaScript、PHP已然形成工业标准。

1990年代后智能手机的出现与普及将计算拓展到个人随身携带的新模式。一些为Web服务设计的语言仍然适用，但新的应用形式也带来了新的挑战。许多项目需要同时以网页、平板以及智能手机形式提供服务。由于应用需求与服务逻辑的易变性，软件的任何更新希望在不同平台上一致地更新。针对这些挑战，出现了新的语言如HTML5。它们不仅需要支持复杂的功能，还需要解决跨平台、跨设备、跨操作系统兼容可移植的难题。

\begin{itemize}
	\item 大数据分析与处理(2004~) 
\end{itemize}

平台系统的大规模数据分析与处理需求，首先来自于互联网的搜索服务。其特点是大量采集的数据需要多台服务器的集群通过并行计算高速处理。分布式并行计算带来了性能优化与可靠性的挑战。但是，在平台建设期无法预知随时可能出现的各种数据分析需求。应用开发人员需要随时针对应用需求快速、灵活地编程，而不必为系统级的性能与可靠性问题所困扰。

设计易用而且高效的并行程序设计语言，是数十年来计算机科学的一个难题。2004年谷歌公司发布MapReduce[1]，标志着工具化的大数据编程框架出现。其设计思想是将数据集的操作限制为并行函数式语言中最基本和常用的Map和Reduce两个命令。对个体数据项的处理由应用开发人员使用C和Java这样的通用语言来编程，而数据集层次的操作由担任分布式操作系统角色的运行时系统负责执行。Hadoop和Spark是基于MapReduce的主要开源工具。尽管此类语言工具不具有独立的语法系统，但其功能和语义直接反映了并行函数式语言与过程式语言混合的编程模型，实质上起到了程序设计语言的作用。

增加语言的专用性有助于在保证易编程性的前提下优化性能，但如果一个编程模型不能涵盖同一应用领域多种相互联系的计算需求，其专用性会影响行业标准的形成。基本的Map与Reduce命令还不能涵盖一般的并行计算步骤的数据依赖关系。

\begin{itemize}
	\item 互联网金融(2009~) 
\end{itemize}

以软件为核心的互联网金融指的是以互联网为载体的金融服务形式，而并非仅仅将互联网作为连接客户的信息系统。开源软件技术主导的金融服务形式始于2009年出现的第一个数字货币--比特币。数字货币以去中心化共识的区块链记账技术为基础，提供类似法定货币的金融功能，具有特殊的金融服务属性。以太坊数字货币扩展了记账技术，支持区块链中记录完整的程序并以可验证的方式执行这样的程序：合同即是程序，程序即是合同。这就是所谓的智能合约(smart contract)。Solidity是目前最流行的合约编程语言。Solidity语法类似于JavaScript，支持继承、类和复杂的用户定义类型，通过编译的方式生成以太坊虚拟机中的代码。

\section{程序设计语言及相关理论}
程序设计语言都具有语法和语义。同时，程序的行为可以描述为状态的转移过程。这里将讨论程序设计语言的语法与语义基础，并给出保证程序正确性的分析方法。

\subsection{类型论}
在很多程序设计语言中，变量与数据是带类型的；而类型之间有一定的关联。人们在研究程序设计语言理论时，可以借鉴类型论(type theory, 也称“类型理论”)来研究程序语言的类型系统。类型论是数理逻辑中的一个分支，其中的马丁洛夫类型理论用规则来刻画类型及行为，是程序构造的形式理论。类型理论研究的是程序语言的类型系统，用于定义如何将编程语言中的数值和表达式等短语归类为许多不同的类型，如何操作这些类型，这些类型如何互相作用。类型通过预测程序部件的某些执行行为来协调这些部件间的交互。在类型化的程序语言中，语言构造分为引入和消去两种形式。类型的引入形式确定该类型的值或范式，而消去形式则确定如何操作该类型的值以形成另一种（可能是相同的）类型的计算。例如，可以使用类型系统中的归纳类型定义如自然数、表、树等数据结构；使用多态类型处理程序的特定型与参数型这些不同的输入类型；使用记录类型定义一组记录的命名类型等；自然数类型的引入形式是自然数，消去形式是加法和乘法等。

\subsection{形式语言}
程序设计语言都有自己的词法和语法，而词法和语法的定义是一系列规则的集合，这些规则的基础就是形式语言。文法是形式语言中十分重要的基本概念，是定义描述语言的语法结构的一组形式规则。文法有四种分类，其中最常用的为正则语言和上下文无关语言。正则语言可以用正规式定义，上下文无关语言可以用上下文无关文法(元素和规则的集合)定义。程序设计语言中的大多数算术表达式可用上下文无关文法生成。正则语言是最简单的语言类，是上下文无关语言类的一个真子类。正则语言已应用于计算机程序语言编译的词法分析、开关电路设计等方面。对程序设计语言编写的程序进行分析和处理(编译)时，需要判断对应的句子是否合法，可以通过对应语言的自动机进行判断。自动机是语言的另一种表示方法。其中，正则语言可以转换成有限状态自动机、上下文无关语言可转换成下推自动机表示，反之亦然。针对某种特定输入的一系列有限的规则，对不同的输入的元素，自动机依据自身的状态会做出不同的响应，最后达到某种特定的状态。

\subsection{形式语义学}
给定一个程序，如何判断它是否正确？这是很早以前人们就关注的问题。简单来说，如果一个程序恰当地实现了设计者与用户的意图，它就是正确的。严格意义上，程序的正确性[6]需要数学证明，不仅需要形式描述设计者与用户的意图，而且要形式描述程序的含义，并推导程序的行为满足设计者与用户的意图。程序含义的形式化描述就是形式语义学。基于形式语义，不仅可以构建描述程序含义的基础，还可以用于验证程序的正确性。

程序设计语言的语法是符号化的，语义是该语言程序所描述的计算或过程。根据语义，程序设计语言的解释器或编译器可以将该语言程序编译成计算机可处理的机器语言程序。在程序设计语言的早期，人们使用自然语言解释语义。这种自然语言解释的语义不精确、有歧义，无法分析和证明程序的正确性。为了提高程序设计语言的可理解性、支持语言标准化、指导语言设计、辅助编译器开发、证明程序的性质和程序之间的等价性，需要对程序设计语言的语义进行抽象，给出严格的定义。为此，人们开始研究使用数学结构定义程序设计语言的语义，并扩展出各类形式规约(specification)语言[19]，形成了形式语义学[8]。

\begin{itemize}
	\item 操作语义
\end{itemize}
程序运行中变量赋值的变化、行为的变迁可以通过操作语义进行描述。操作语义(operational semantics)将语言中各个成分翻译成计算机系统中相应的一组操作。目前最为常见的操作语义是标号迁移系统(labeled transition system)，将程序执行描述成标号迁移系统，其中的状态是程序执行期间任意时刻观察到的变量取值。迁移规则规定如何从一个状态转换到下一个状态，每条迁移规则对应一个语句，称为标号。一条语句的语义由一组以其为标号的规则定义；标号规则具有组合性，即一个复合语句的规则可以由其成分语句的规则组合而成。例如，针对一个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是描述程序执行的迁移系统中的迁移规则。

在由操作语义描述的串行程序的语义中，状态是一些简单的数据结构，迁移规则一般都是确定的、离散的，也不需要考虑标号间的通信和同步。为了定义复杂程序的操作语义，例如面向对象程序、并发程序、实时程序、概率程序、混成系统等，人们对迁移系统进行了各种扩充，或扩充它的状态，或扩充它的迁移关系，亦或两者同时扩充。例如，为了定义面向对象程序，人们对程序状态进行扩充，引入堆和栈等复杂数据结构；为了处理并发程序，人们对标号迁移关系进行扩充，使用标号描述通信和同步；为了描述概率和随机程序，允许以给定的概率或者随机选取迁移规则等。

基于抽象机的操作语义可描述实现方面的执行细节，操作性比较强，适合于语言编译器的开发与编译的优化。操作语义中的状态是显式的、可操作的。因此，在基于状态搜索的模型检验方法中，操作语义比较适合描述模型的语义，即状态的变化序列。然而，抽象机上的推理系统比较弱，不易对大规模或无穷状态的系统进行基于演绎推理的形式验证。

\begin{itemize}
	\item 公理语义
\end{itemize}
程序的语义不仅可以使用操作语义描述，还可以使用形式逻辑来描述。而形式逻辑是公理语义(axiomatic semantics)的基础。公理语义直接使用形式逻辑来描述程序的语义，在已有的形式逻辑系统基础上增加所有程序必须满足的基本命题(程序公理)。动态逻辑、模态逻辑、时序逻辑等用来作为定义程序公理语义的形式系统。每个程序的基本语句都有一组公理和推理规则，它们与断言逻辑一起构成程序逻辑的证明系统。例如，若条件语句if(y==1) then x=1; else x=2的前置条件为{y==1}，则该语句执行后，后置条件为{x==1}。在该形式系统中可以直接进行程序性质的规约和验证。程序逻辑的表达能力、可靠性、完备性以及可判定性都可归结为数理逻辑上的元性质，程序逻辑的解释模型通常就是程序设计语言的指称语义或操作语义。

常见的形式逻辑有基于一阶逻辑扩展的Floyd-Hoare 逻辑[15]、谓词转换器(predicate transformer)等。其中，Floyd-Hoare 逻辑最初是面向串行程序的，并扩展至并发程序、实时系统、混成系统甚至量子系统等。针对指针程序和面向对象程序，产生了分离逻辑及其变种，从而把Floyd-Hoare 逻辑的应用推进到实际的程序验证。公理语义在形式验证中的应用是比较多的。

\begin{itemize}
	\item 代数语义
\end{itemize}
面向对象程序设计语言具有抽象数据类型、多态性等特点。在抽象数据类型的基础上发展起来的代数语义(algebraic semantics)，用代数方法研究计算机语言的语义。它把程序设计语言形式地定义为满足某种公理体系的抽象代数结构，然后利用这种代数结构的性质来证明用该语言编写的程序的正确性。

抽象数据类型将数据对象及对象上的操作封装、数据类型的特性与实现分离，具有模块化和可复用的性质。它与软件开发过程匹配比较自然，因此也可以用于程序的自动构造：首先设计较小的抽象数据类型，然后逐步扩充形成较大的抽象数据类型体系；这个过程中，抽象数据类型间可讨论层次一致和充分完备等性质。

\begin{itemize}
	\item 指称语义
\end{itemize}
指称语义(denotational semantics)关注代表程序所做所为的数学对象，用数学对象上的运算来定义语言的语义。建立指称语义首先要确定程序设计语言的解释域(论域理论)。论域理论是指称语义的数学基础，讨论各种语言成分的指称(意义)的数学结构，并在各种数学结构之上定义语言语义，推导语言成分特性。例如，将程序设计语言的基本语法实体的指称定义为程序状态空间上的函数和泛函，复合语法实体的指称由构成它的子成分的指称复合得到。基于指称语义的相关理论，可以推导不同语言形式语义间的关系，也可以分析同一语言不同语义间的转换关系。其中，基于一阶关系演算的程序统一理论(unifying theories of programming，简称UTP)，可以通过伽罗瓦连接(Galois connection)给出同一语言不同语义间的转换关系。

除了这几类经典的语义，近期由Grigore Rosu提出的K框架提供了基于重写的语言[21]，用于定义编程语言的正式操作语义。K语言的语义是可执行的。结合K语言语义及相应的逻辑推理过程，可以分析和验证各种程序，而无需为语言提供任何其他语言（公理或指称或动态等）语义。

\subsection{形式规约}
直接使用程序设计语言及其语义，难以描述和证明软件从需求文档到程序代码的开发过程各阶段创建的不同抽象层次的制品及其正确性。针对这一问题，人们开始研究高层抽象的形式规约语言的设计。形式规约语言是指由严格的递归语法规则所定义的语言，满足语法规则的句子称为合式或良构(well-formed)规约。形式规约可以自顶向下逐步精化形成开发的规约序列，在足够的实现细节完成后，可以通过代码自动生成得到程序。以形式规约语言为基础的形式化开发方法，有VDM、Z、Event-B、RAISE、CafeOBJ、TLA、SOFL等。20世纪七十年代后，软件工程界认识到数学可以为程序正确性保证提供技术基础。相应的出现了一系列程序设计理论框架。例如，八十年代初，唐稚松提出以时序逻辑作为软件开发过程的统一基础，并着手建立XYZ系统[9]。Goguen 和Burstall提出了一种抽象模型理论，以实现不同形式逻辑基础上的各种形式化方法的理论统一、技术和工具的集成与使用[10]。Hoare和何积丰提出了统一程序设计理论框架UTP，提供了在一种程序(如串行程序)语义模型理论基础上构建扩展程序(如并发)的语义理论，从而保证原来的理论在扩展的理论中能够重用[11]。

基于程序逻辑系统的性质规约刻画了所期望的系统行为，这些性质是通过逻辑公式来描述的。

串行程序设计早期的程序逻辑是Floyd-Hoare逻辑。通过在一阶谓词系统基础上添加关于程序的公理和推理规则，构成了Floyd-Hoare 逻辑的推理系统。类似的规约语言还有Dijkstra 的卫士命令语言的最弱前置条件演算。然而，早期的基于Floyd-Hoare 逻辑的推理系统无法描述带指针和内存数据结构的程序规约，也无法描述并发程序的规约。分离逻辑是对Floyd-Hoare 逻辑的扩展，以支持带有指针和内存数据结构的程序的验证。分离逻辑最大的特点是对内存和数据结构的抽象描述，能够更方便、更模块化地支持类似C程序的指针程序的验证。它在断言语言中引入方便描述内存使用和分离特性的分离合取和分离蕴含谓词，并在规则中将Floyd-Hoare 逻辑的不变式(invariance)规则替换为框架(frame)规则。

并发程序的规约在Floyd-Hoare 逻辑的基础上，引入了行为轨迹的变量或不变式。与分离逻辑类似，并发分离逻辑也支持并发程序验证。后续有大量工作对并发分离逻辑进行扩充，例如将Rely-Guarantee 和并发分离逻辑结合，从而支持细粒度并发或者无锁并发程序的规约和验证。除了这些针对串行一致性内存模型上的并发程序的程序逻辑外，还有一些工作对并发分离逻辑进行扩展，以支持弱内存模型下的并发程序。例如，在C11 内存模型上的程序逻辑(如文献[13])， 来证明C11 内存模型(子集)上的程序的正确性。

Floyd-Hoare逻辑中，程序与断言是分离的，而且也无法表达活性。针对这些不足，相继出现了基于模态逻辑的动态逻辑、基于动态逻辑的模态$\mu$-演算[14]。作为模态$\mu$-演算的真子集，线性时序逻辑(LTL)和计算树逻辑(CTL)是并发系统规约和验证的常用语言。除了这些经典的逻辑，还有用于数理逻辑计算和并发系统正确性验证的动作时序逻辑(TLA)、用于有限序列中命题与一阶逻辑推理的区间时序逻辑(ITL)。为了处理一些非功能性质，还出现了各种扩充，如微分动态逻辑、度量时序逻辑(MTL)、时段演算(DC)等。

\section{程序正确性分析方法}
程序的正确性分析存在不同的方法。如图\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{基于验证的分析方法}
定理证明、模型检验是形式化验证的两种主要方法，并逐渐被IT产业界所接受和采纳。例如，使用形式化验证工具如Z3、SLAM等，分析软件的正确性；基于分离逻辑的验证工具Infer用于Android应用的开发过程中；使用SMT求解器去验证Web服务的正确性；使用定理证明辅助工具来验证操作系统内核的正确性和安全性。

\begin{itemize}
	\item 定理证明
\end{itemize}

基于定理证明的验证大部分是以程序逻辑为理论基础的。除此以外，我们还可以基于程序的操作语义，直接表达程序执行的安全性、正确性等各种性质，并证明相关定理。

对串行程序进行验证，可以通过一组与程序设计语言语句对应的Floyd-Hoare逻辑公理和规则，将对程序的验证转化为一组数学命题的证明。基于这种逻辑，一方面的工作通过并发任务的无干扰性(non-interference) [12]、并发任务间接口的抽象[17]、程序逻辑的化简[16]等不同方面，实现并发程序的验证。另一个方面的工作使用关系型程序逻辑验证两个程序之间的关系，或者一个程序在两种输入下的行为之间的关系。前者可用于程序精化的验证，而后者则可用于信息安全性质，如信息流控制(information flow control)机制的验证。

基于定理证明的验证可以分为两类，即基于自动定理证明器的自动验证和基于人机交互的半自动验证。常见的程序自动证明器(program verifier)，如Dafny、Why3、VeriFast、Smallfoot等，大多都基于某种具体的程序逻辑。给定程序及其规约，证明器能够自动决定针对程序的每条语句使用程序逻辑中的何种公理或规则，并产生相应的验证条件作为证明义务。最终，由定理证明器完成对验证条件的证明。目前使用最广泛的定理证明器是Z3，其他常见的证明器还包括CVC4、Yices 2等。基于人机交互的半自动验证工具，如Coq和Isabelle/HOL等，利用类型系统和逻辑之间的Curry-Howard同构关系[1]，将构造证明的过程转化为编写程序的过程，而证明的正确性检查也变成了类型检查问题。这种方法的优点在于无需牺牲规约和代码的表达能力，程序规约可以用表达能力很强的逻辑(如在Coq 和Isabelle/HOL 中使用的高阶逻辑)来表示。而且证明自身在机器中有显式表示，其正确性可以被自动检查，因此无需依赖自动定理证明算法的正确性，验证的结论也就更加可信。seL4的ARM版本是第一个带有完整代码级的功能正确性证明的通用操作系统内核，可以应用于金融，医疗，汽车，航空电子设备和国防部门。它的验证使用了Isabelle/HOL定理证明，这意味着通过形式化方法证明了实现(用编写C语言)是满足其规约的。除了对程序的验证，还有对编译器的验证，保证程序从编写到产生的可执行程序的正确性。例如，适用于C99编程语言的大部分语法的CompCert是一个经过正式验证的优化编译器，支持PowerPC、ARM、RISC-V、x86和x86-64架构。

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

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

\subsection{程序的精化}
程序精化是将抽象（高级）形式规范可验证地转换为具体（低级）可执行程序的过程，是通过逐步细化分阶段完成。精化（Refinement）是一种数学表示法和若干规则的集合，它对Dijksart的卫式命令语言进行扩充，通过结合规约语句、精化规则和语言本身，从程序规约推导出命令式程序。程序精化(程序规约转换成可执行代码)可分为数据精化和算法精化两种，形式化将程序逐步转换为更加便于实现的形式：数据精化把抽象的数据结构转换为可以高效实现的形式；算法精化将程序逐步转换为更加便于实现的代码形式。

\section{小结}
开发软件，离不开程序设计语言。本章简要介绍了若干典型的程序设计语言。在计算机发展的不同阶段，为了应对一些典型应用，这些语言应运而生。本章还介绍了几类形式语义。它们有助于清晰地表达程序的含义，可用于验证程序的正确性。 
	
\section{参考文献}  
	
\begin{itemize}
	\item [] [1]. Sebesta R.W.  Concepts of Programming Languages. (7th ed.) Pearson, 2006.
	\item [] [2]. Bergin T. J.  A history of the history of programming languages. Comm. ACM 50(5): 69-74 (2007)
	\item [] [3]. Dijkstra E.W. Go To Statement Considered Harmful. Communications of the ACM. 11(3): 147-148, 1968.
	\item [] [4]. Lämmel  R. Google's MapReduce programming model — Revisited. Science of Computer Programming. 70: 1-30, 2008.
	\item [] [5]. Abadi  M. et al. TensorFlow: A System for Large-Scale Machine Learning. Proc. OSDI 2016: 265-283.
	\item [] [6]. Turing A. Checking a large routine. Report of a Conf. on High Speed Automatic Calculating Machines, Cambridge University Math. Lab., 1949. 67~69. 
	\item [] [7]. Roscoe AW. Understanding Concurrent Systems. Springer-Verlag, 2010.
	\item [] [8]. 周巢尘，詹乃军. 形式语义学引论(第二版). 科学出版社, 2018.  
	\item [] [9]. 唐稚松等. 时序逻辑程序设计与软件工程. 科学出版社, 2002.
	\item [] [10]. 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 [] [11]. Hoare CAR, He J. Unifying Theories of Programming. Prentice Hall, 1998,14:184-203.
	\item [] [12]. Owicki S, Gries D. An axiomatic proof technique for parallel programs I. Acta Informatica, 1976,6(4):319-340.
	\item [] [13]. Svendsen K, Pichon-Pharabod J, Doko M, Lahav O, Vafeiadis V. A separation logic for a promising semantics. In: Proc. of the European Symp. on Programming. Springer-Verlag, 2018. 357-384.
	\item [] [14]. Kozen D. Results on the propositional mu-calculus. Theoretical Computer Science, 1983,27(3):333-354.
	\item [] [15]. Hoare CAR. An axiomatic basis for computer programming. Communications of the ACM, 1969,12(10):576-580.
	\item [] [16]. Owicki S, Gries D. Verifying properties of parallel programs: An axiomatic approach. Communications of the ACM, 1976,19(5):279-285.
	\item [] [17]. Jones CB. Tentative steps toward a development method for interfering programs. ACM Trans. on Programming Languages and Systems, 1983,5(4):596-619.
	\item [] [18]. Howard WA. The formulae-as-types notion of construction. To HB Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, 1980,44:479-490.
	\item [] [19]. 王戟,詹乃军,冯新宇,刘志明.形式化方法概貌.软件学报,2019,30(1):33-61
	\item [] [20]. Amir Pnueli and Roni Rosner. On the synthesis of a reactive module. In POPL, 1989:179–190. 
	\item [] [21]. Roșu, Grigore. From rewriting logic, to programming language semantics, to program verification. Logic, Rewriting, and Concurrency. Springer, Cham, 2015. 598-616.
	\item [] [22]. Hu Z, Hughes J, Wang M. How functional programming mattered, National Science Review, Oxford Journal, 2015, 2(3):349-270. 
	\item [] [23]. https://www.tiobe.com/tiobe-index/
	
\end{itemize}