计算机数理逻辑-程序验证-顺序程序

1. Program

A computer program is not very different from a logical formula. It consists of a sequence of symbols constructed according to formal syntactical rules and it has a meaning which is assigned by an interpretation of the elements of the language. In programming, the symbols are called statements or commands and the intended interpretation is the execution of the program on a computer. The syntax of programming languages is specified using formal systems such as BNF, but the semantics is usually informally specified.

一个计算机程序与一个逻辑公式没有什么不同。它由一连串的符号组成，这些符号是根据正式的句法规则构建的，它有一个意义，这个意义是通过对语言元素的解释而赋予的。在编程中，这些符号被称为语句或命令，预期的解释是程序在计算机上的执行。编程语言的语法是用BNF这样的形式化系统指定的，但语义通常是非正式地指定的

1.1. 考虑一门语言的设计

• A program is a statement S, where statements are defined recursively using the concepts of variables and expressions
  • 程序本身就是一个抽象的大statement

• A statement in a programming language can be considered to be a function that transforms the state of a computation
  • 编程语言可以被视作状态转换函数

Let $S$ be a program with $n$ variables $(x1,…,xn)$. A state $s$ of $S$ consists of an $n+1$-tuple of values $(lc,x_1,…,x_n )$, where $lc$ is the value of the location counter(sometimes called the instruction pointer，存储下一个指令的地址) and $x_i$ is the value of the variable $xi$.

• we aim to verify the program by proving: if the input to the program satisfies the precondition, then the output of the program will satisfy the postcondition

example

• If the variables (x,y) have the values (8,7) in a state, then the result of executing the statement x = 2*y+1 is the state in which (x,y)=(15,7) and the location counter is incremented

2. Correctness Formulas

• A correctness formula is a triple ${ p } S { q }$ , where $S$ is a program, and $p$ and $q$ are formulas called the precondition and postcondition, respectively. S is partially correct with respect to p and q，$⊧ { p } S { q }$,iff

  • If $S$ is started in a state where $p$ is true and if the computation of $S$ terminates, then it terminates in a state where $q$ is true

• correctness formulas also call inductive expressions

只要 P 在 C 执行前的状态下成立，则在执行之后 Q 也成立。注意如果 C 不终止，也就没有”之后”了，所以 Q 在根本上可以是任何语句。实际上，你可以选择 Q 为假来表达 C 不终止。事实上，这种情形叫做 “部分正确（partial correctness）”。如果 C 终止并且在终止时 Q 是真，则表达式被称作 “全部正确性（total correctness）”。终止必须被单独证明。

example

2.1. characteristic predicate

Let U be the set of all n-tuples of values over some domain(s), and let U′⊆U be a relation over U. The n-ary predicat $P_{U′}$ is the characteristic predicate特征谓词 of U′ if it is interpreted over the domain U by the relation U′. That is, $v(P_{U′}($x_1$,…,$x_n$))=T iff ($x_1$,…,$x_n$)∈U′$.

• We can write {(x 1,…,x n )∣(x 1,…,x n )∈U′} as {(x 1,…,x n )∣ $P_{U′}$ }
• 即：如果变量都在domain上，则为T

2.2. semantics of programming language

• 编程语言的语义是通过指定语言中的每个语句如何将一种状态转化为另一种状态而给出的

example

• Let S be the statement x = 2*y+1.
  • If started in an arbitrary state (x,y), the statement terminates in the state (x′,y′) where x′=2y′+1.
  • Another way of expressing this is to say that S transforms the set of states {(x,y)∣true} into the set {(x,y)∣x=2y+1}.
  • The statement S also transforms the set of states {(x,y)∣y≤3} into the set {(x,y)∣(x≤7)∧(y≤3)}, because if y≤3 then 2y+1≤7

3. Deductive System HL 霍尔逻辑

• Instead, we will simply take all true formulas in the domain as axioms. For example, (x≥y)→(x+1≥y+1) is true in arithmetic and will be used as an axiom. This is reasonable since we wish to concentrate on the verification that a program S is correct without the complication of verifying arithmetic formulas that are well known.

example

• The formula p in the loop rule is called an invariant不变量: it describes the behavior of a single execution of the statement S in the body of the while-statement.
• 感觉有点类似sed

4. Program Verification