example for axiomatic semantics

Ch1-2-ProgrammingLanguage.tex

@@ -9,7 +9,7 @@
 
 在计算机发展的早期，人们往往是用二进制(0/1序列)给计算机发指令。这显然很不方便。后来，逐渐出现了汇编语言以及各种高级语言。一般来说，提高软件开发本身的效率与质量需要更抽象更高级的程序设计语言；而提高现实计算机硬件系统的利用率和执行效率，则需要使用较低级的程序设计语言，这样程序可以更直接地控制硬件资源。较通用的程序设计语言适用于广泛的应用领域和应用场景，可吸引大量的语言使用者，积累充足的遗产代码，便于培训与推广共享资源；但高度通用的语言设计上难以兼顾开发效率与执行效率。很多针对特定应用领域的程序设计语言更容易通过合适的语言机制同时改善软件开发与执行的效率。多样化的编程接口具有程序设计语言功能，但缺乏相应的编程框架甚至程序库等。这类接口反映了相应的编程模型的特点，实质上起到了程序设计语言的作用。
 
-程序设计语言的发展既要遵循自身理论与模型的内在规律，也受到计算机系统发展的驱动和行业应用需求发展的推动。不同语言不同程度地受这些因素推动。但从程序设计语言发展历史角度看，应用需求的影响明显处于主导地位。新出现的程序设计语言通常是应对新兴应用或者新兴计算机体系结构的需要。  
+程序设计语言的发展既要遵循自身理论与模型的内在规律，也受到计算机系统发展的驱动和行业应用需求发展的推动。不同语言不同程度地受这些因素推动。但从程序设计语言发展历史角度看，应用需求的影响明显处于主导地位。新出现的程序设计语言通常是应对新兴应用或者新兴计算机体系结构的需要。
 
 \subsection{语言的设计、实现及生命期}
 \subsubsection{设计}
@@ -142,6 +142,7 @@
 \begin{itemize}
 	\item 操作语义
 \end{itemize}
+
 操作语义(operational semantics)使用结构化的归约规则，着重描述程序运行中变量赋值的变化、行为的变迁。它将语言中各个成分翻译成计算机系统中相应的一组操作。目前最为常见的操作语义是标号迁移系统(labeled transition system)，将程序执行描述成标号迁移系统，其中的状态是程序执行期间任意时刻观察到的变量取值。迁移规则规定如何从一个状态转换到下一个状态，每条迁移规则对应一个语句，称为标号。一条语句的语义由一组以其为标号的规则定义；标号规则具有组合性，即一个复合语句的规则可以由其成分语句的规则组合而成。例如，针对一个C程序中的循环语句while(x<y) do\{x++;\}的操作语义为：
 \lstset{language=C}
 \begin{lstlisting}
@@ -158,13 +159,24 @@
 \begin{itemize}
 	\item 公理语义
 \end{itemize}
-程序的语义不仅可以使用操作语义描述，还可以使用形式逻辑来描述。而形式逻辑是公理语义(axiomatic semantics)的基础。公理语义直接使用形式逻辑来描述程序的语义，在已有的形式逻辑系统基础上增加所有程序必须满足的基本命题(程序公理)。动态逻辑、模态逻辑、时序逻辑等用来作为定义程序公理语义的形式系统。每个程序的基本语句都有一组公理和推理规则，它们与断言逻辑一起构成程序逻辑的证明系统。例如，若条件语句if(y==1) then x=1; else x=2; 的前置条件为\{y==1\}，则该语句执行后，后置条件为\{x==1\}。在该形式系统中可以直接进行程序性质的规约和验证。程序逻辑的表达能力、可靠性、完备性以及可判定性都可归结为数理逻辑上的元性质，程序逻辑的解释模型通常就是程序设计语言的指称语义或操作语义。
 
-常见的形式逻辑有基于一阶逻辑扩展的Floyd-Hoare 逻辑[10]、谓词转换器(predicate transformer)等。其中，Floyd-Hoare 逻辑最初是面向串行程序的，并扩展至并发程序、实时系统、混成系统甚至量子系统等。针对指针程序和面向对象程序，产生了分离逻辑及其变种，从而把Floyd-Hoare 逻辑的应用推进到实际的程序验证。公理语义在形式验证中的应用是比较多的。
+公理语义(axiomatic semantics)运用数学中的公理化方法给出计算机语言的语义。
+%程序的语义不仅可以使用操作语义描述，还可以使用形式逻辑来描述。而形式逻辑是公理语义(axiomatic semantics)的基础。公理语义直接使用形式逻辑来描述程序的语义，在已有的形式逻辑系统基础上增加所有程序必须满足的基本命题(程序公理)。
+动态逻辑、模态逻辑、时序逻辑等可以用来作为定义程序公理语义的形式系统。每个程序的基本语句都有一组公理和推理规则，它们与断言逻辑一起构成程序逻辑的证明系统。例如，
+对于顺序语句$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\}。
+在该形式系统中可以直接进行程序性质的规约和验证。程序逻辑的表达能力、可靠性、完备性以及可判定性都可归结为数理逻辑上的元性质，程序逻辑的解释模型通常就是程序设计语言的指称语义或操作语义。
+常见的公理语义有基于一阶逻辑扩展的Floyd-Hoare 逻辑[10]、谓词转换器(predicate transformer)等。其中，
+Floyd-Hoare 逻辑最初是面向串行程序的，并扩展至并发程序、实时系统、混成系统甚至量子系统等。针对指针程序和面向对象程序，产生了分离逻辑及其变种，从而把Floyd-Hoare 逻辑的应用推进到实际的程序验证。公理语义在形式验证中的应用是比较多的。
 
 \begin{itemize}
 	\item 代数语义
 \end{itemize}
+
 面向对象程序设计语言具有抽象数据类型、多态性等特点。在抽象数据类型的基础上发展起来的代数语义(algebraic semantics)，用代数方法研究计算机语言的语义。它把程序设计语言形式地定义为满足某种公理体系的抽象代数结构，然后利用这种代数结构的性质来证明用该语言编写的程序的正确性。
 
 抽象数据类型将数据对象及对象上的操作封装、数据类型的特性与实现分离，具有模块化和可复用的性质。它与软件开发过程匹配比较自然，因此也可以用于程序的自动构造：首先设计较小的抽象数据类型，然后逐步扩充形成较大的抽象数据类型体系；这个过程中，抽象数据类型间可讨论层次一致和充分完备等性质。
@@ -172,6 +184,7 @@
 \begin{itemize}
 	\item 指称语义
 \end{itemize}
+
 指称语义(denotational semantics)关注代表程序所做所为的数学对象，用数学对象上的运算来定义语言的语义。建立指称语义首先要确定程序设计语言的解释域(论域理论)。论域理论是指称语义的数学基础，讨论各种语言成分的指称(意义)的数学结构，并在各种数学结构之上定义语言语义，推导语言成分特性。例如，将程序设计语言的基本语法实体的指称定义为程序状态空间上的函数和泛函，复合语法实体的指称由构成它的子成分的指称复合得到。基于指称语义的相关理论，可以推导不同语言形式语义间的关系，也可以分析同一语言不同语义间的转换关系。%其中，基于一阶关系演算的程序统一理论(unifying theories of programming，简称UTP)，可以通过伽罗瓦连接(Galois connection)给出同一语言不同语义间的转换关系。
 
 
@@ -183,7 +196,7 @@
 
 
 
-串行程序设计早期的程序逻辑是Floyd-Hoare逻辑。通过在一阶谓词系统基础上添加关于程序的公理和推理规则，构成了Floyd-Hoare 逻辑的推理系统。类似的规约语言还有Dijkstra 的卫式命令语言的最弱前置条件演算。然而，早期的基于Floyd-Hoare 逻辑的推理系统无法描述带指针和内存数据结构的程序规约，也无法描述并发程序的规约。分离逻辑是对Floyd-Hoare 逻辑的扩展，以支持带有指针和内存数据结构的程序的验证。分离逻辑最大的特点是对内存和数据结构的抽象描述，能够更方便、更模块化地支持类似C程序的指针程序的验证。它在断言语言中引入方便描述内存使用和分离特性的分离合取和分离蕴含谓词，并在规则中将Floyd-Hoare 逻辑的不变式(invariance)规则替换为框架(frame)规则。
+串行程序设计早期的程序逻辑是Floyd-Hoare逻辑。通过在一阶谓词系统基础上添加关于程序的公理和推理规则，构成了Floyd-Hoare 逻辑的推理系统。类似的规约语言还有Dijkstra 的卫式命令语言的最弱前置断言演算。然而，早期的基于Floyd-Hoare 逻辑的推理系统无法描述带指针和内存数据结构的程序规约，也无法描述并发程序的规约。分离逻辑是对Floyd-Hoare 逻辑的扩展，以支持带有指针和内存数据结构的程序的验证。分离逻辑最大的特点是对内存和数据结构的抽象描述，能够更方便、更模块化地支持类似C程序的指针程序的验证。它在断言语言中引入方便描述内存使用和分离特性的分离合取和分离蕴含谓词，并在规则中将Floyd-Hoare 逻辑的不变式(invariance)规则替换为框架(frame)规则。
 并发程序的规约在Floyd-Hoare 逻辑的基础上，引入了行为轨迹的变量或不变式。与分离逻辑类似，并发分离逻辑也支持并发程序验证。后续有大量工作对并发分离逻辑进行扩充，例如将Rely-Guarantee 和并发分离逻辑结合，从而支持细粒度并发或者无锁并发程序的规约和验证。%除了这些针对串行一致性内存模型上的并发程序的程序逻辑外，还有一些工作对并发分离逻辑进行扩展，以支持弱内存模型（如C11）下的并发程序的正确性分析。
 
 Floyd-Hoare逻辑中，程序与断言是分离的，而且也无法表达活性。针对这些不足，相继出现了基于模态逻辑的动态逻辑、基于动态逻辑的模态$\mu$-演算。作为模态$\mu$-演算的真子集，线性时序逻辑(LTL)和计算树逻辑(CTL)是并发系统规约和验证的常用语言。除了这些经典的逻辑，还有用于数理逻辑计算和并发系统正确性验证的动作时序逻辑(TLA)、用于有限序列中命题与一阶逻辑推理的区间时序逻辑(ITL)。为了处理一些非功能性质，还出现了各种扩充，如度量时序逻辑(MTL)、时段演算(DC)等。
@@ -219,7 +232,7 @@ 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框架提供了基于重写的语言[11]，用于定义编程语言的正式操作语义。K语言的语义是可执行的。结合K语言语义及相应的逻辑推理过程，可以分析和验证各种程序，而无需为语言提供任何其他语言（公理或指称或动态等）语义。
 

Ch2-2-SoftwareTheory.tex

@@ -66,7 +66,7 @@
 近年来，新的体系结构和计算平台大量涌现，包括多核处理器、GPU和异构芯片、分布式云计算平台等。它们对程序设计有各自特定的要求，也对相应的程序验证带来了重要的机遇和挑战。
 
 
-首先，多处理器架构对程序本身的内存模型分析与设计带来新的挑战。多核处理器的流行让并发编程由一种高级编程技巧变为一种基本的编程技能。然而，并发编程自身的困难并未随之消失，特别是经典的共享内存的多任务并发模型及其基于锁的同步机制，为并发程序设计带来了数据竞争、原子性违背、死锁、活锁等各种问题。针对这些问题，新的易用、可靠的并发编程模型一度成为研究的热点，提出的新型编程模型包括软件事务型内存（Software Transactional Memory，简称STM）、事件驱动的并发模型、基于消息传递的并发模型等。然而，从易用程度和程序效率的需求看，现有编程模型仍然无法替代经典的共享内存并发模型。并发编程的另一大挑战是内存模型问题。编译器和处理器的优化导致每个并发任务的执行并不是严格按照代码顺序逐条指令运行。虽然这些指令执行顺序的改变不会影响单个任务的串行行为，但会对多任务的程序行为产生影响。相应的，并发程序行为呈现出所谓的弱内存模型。任何一个并发编程语言需要都需要描述其内存模型，然而由于编译器优化的复杂性，为高级语言定义内存模型的工作仍然是一个开放性问题。例如Java和C++现有的内存模型仍然存在各种问题。因此，对这些模型的形式化定义和改善成为当前研究的一大热点。
+首先，多处理器架构对程序本身的内存模型分析与设计带来新的挑战。多核处理器的流行让并发编程由一种高级编程技巧变为一种基本的编程技能[3]。然而，并发编程自身的困难并未随之消失，特别是经典的共享内存的多任务并发模型及其基于锁的同步机制，为并发程序设计带来了数据竞争、原子性违背、死锁、活锁等各种问题。针对这些问题，新的易用、可靠的并发编程模型一度成为研究的热点，提出的新型编程模型包括软件事务型内存（Software Transactional Memory，简称STM）、事件驱动的并发模型、基于消息传递的并发模型等。然而，从易用程度和程序效率的需求看，现有编程模型仍然无法替代经典的共享内存并发模型。并发编程的另一大挑战是内存模型问题。编译器和处理器的优化导致每个并发任务的执行并不是严格按照代码顺序逐条指令运行。虽然这些指令执行顺序的改变不会影响单个任务的串行行为，但会对多任务的程序行为产生影响。相应的，并发程序行为呈现出所谓的弱内存模型。任何一个并发编程语言需要都需要描述其内存模型，然而由于编译器优化的复杂性，为高级语言定义内存模型的工作仍然是一个开放性问题。例如Java和C++现有的内存模型仍然存在各种问题。因此，对这些模型的形式化定义和改善成为当前研究的一大热点。
 
 
 其次，多处理架构引发了并发程序数据一致性分析的挑战。多核平台中存在多线程并发程序对共享资源的访问冲突。多线程并发程序已经成为现代程序设计的趋势。并发软件应用中的并发数据结构提供支持多线程并发访问。但并发线程的执行存在不确定性,传统的测试方法很难发现这类错误。多核平台下的弱内存模型则使得多线程间数据访问的一致性难以保证。并发数据结构实现的可线性化（或其量化松弛）验证问题已经取得了一定进展，可线性化条件对有界多并发线程是可判定的，但对无界多并发线程是不可判定的。
@@ -176,3 +176,5 @@
 [1].	L. Peter Deutsch, Ronald B. Finkbine. ACM Fellow profile. ACM SIGSOFT Software Engineering Notes 24(1): 21 (1999).
 
 [2].	Xiaowei Huang, Daniel Kroening, Wenjie Ruan, James Sharp, Youcheng Sun, Emese Thamo, Min Wu, Xinping Yi. A Survey of Safety and Trustworthiness of Deep Neural Networks. arXiv:1812.08342.
+
+[3].   Herlihy, Maurice, and Nir Shavit. The art of multiprocessor programming. Morgan Kaufmann, 2011.