==。 最近刚刚把sf大概的读了一下，虽说coq练习的练习还是写了挺多的，但是还是发现对于考试的要求还是不够的， 在这里大概的整理以下吧。最近的笔记主要是针对第二卷的内容。我实在是比较蠢基本就是抄书啦。

0X00 问题引入

在学习程序的形式验证过程中，第一步是得到AST之后，对于程序具有的一些比较理论的性质，比如值deterministic的，两段程序在行为上是不相等， 程序会不会终止等。
但是这个讨论还是太粗糙了，对于程序运行中的一些比较具体的行为我们还是无法进行验证。比如在循环过程过后一个变量的值不会改变之类的问题，在我们日常的编程中其实还是经常会用到的。所以在此引入霍尔逻辑(Hoare Logic).
为了证明程序正确，一种很自然的想法就是在程序开始前基于一些初始条件，或者初始需要满足的东西， 在程序结束的时候再加上另外一个验证条件，如果我们能够证明在程序运行的过程中，初始条件和最终的条件都能依然能够被满足，那么验证通过。 其实和软件测试的过程非常的相似，只不过我们不再给出具体的测试用例，直接给出逻辑断言给我们的一阶逻辑系统的看最后是不是符合要求。

0X01 定义

Definition:
霍尔逻辑由一个霍尔三元组表达(Hoare Triple).

 {{P}} c {{Q}}

语义：

如果命令c以一个满足断言(Assertation)P的状态开始，并且在执行过程中能够正常的结束，那么其结束的状态满足断言Q。其中P称为前条件(precondition), Q被称为后条件(postcondition)

需要注意的是这里的断言说的是能满足某种状态（上下文）的一种表达式，也就是一种表达状态的谓词逻辑命题

例子：

{{X = m}} c {{X = m + 5)}}

从定义中可以看出霍尔三元组是一个命题(Propostion), 那么其自然有存在是否有效(Valid)的问题，也就是说是不是任何情况下都是真.

Example:
如下命题

{{ X = 3 }}
WHILE True DO c END
{{ X = 3 }}

就是一个valid的命题， 因为while true意味着命令并不会终止，这时候我们无论给什么样子的后续条件都能成立，个人理解，相当于中间部分有一个 , false implies everthing.最后结果显然是.当然这只是为了方便自己记忆的方法，是不能这么说的。

{{ Y = X }}
IFB X = 0 THEN
SKIP
ELSE
WHILE X > 0 DO c END
{{ Y > 0 }}

这就是一个invalid的命题， 因为前条件只有，而这个显然是无法满足上述命题的逻辑的，因为x的状态未知，如果那么命题为假，如果, 那么c的不同是可能可以满足命题的，所以推不出，命题为invalid.

Corollary:

通过上述对霍尔三元组的讨论有如下显而易见的结论

• 
• 

用人话说，如果后条件为真，那么命题成立；如果前条件为假那么命题成立。证明很简单，后条件既然能满足状态为真，那也没啥好证明了。。。。因为三元组命题最后一步就是后条件满足； 前条件存在无法满足，false implies everything.

0x02 关于命令式编程的一些推论

赋值

首先定义一下替换(substitution)，这里的替换的定义和谓词逻辑中的完全替换定义类似，毕竟霍尔逻辑中的断言都是Propostion.

表示命题P中的变量X 全部使用 a来代替

对于赋值符号 ::= 有如下规则

这个很直接，赋值本质就是对状态中某个变量对应的值做替换，这个操作实际发生在求值的时候

因果

很多时候我们是不能直接得到前条件的，它可能蕴含在别的条件当中，这个时候我们需要一些逻辑推论之间的inference rule
简单定义以下符号

P —>> P' : 断言P能推出P'
P  <<—>> P' 断言P逻辑等价与P'

推论成立，那么原命题也成立

SKIP 语句

顺序结构

这条性质非常非常有用，表达了一个命令式的程序可以拆分成一系列的霍尔逻辑，这样能够让证明变得比较清晰有效

条件语句

这个也挺好理解，一个if可以拆成两种情况分开讨论，如果不论是b如何都成立，那么命题肯定就成立

循环

循环结构是最为复杂的，因为霍尔逻辑对于程序是否能终止是有要求的，而死循环也是我们必须要考虑到的。

首先分情况讨论，如果循环条件为假，也就是说相当于跳过这个语句，这就是一个比较平凡的case了,会出现

{{P /\ b}} WHILE b DO c END {{P}}.

循环条件为真那么循环体语句会得到执行，反之，如果循环体得到了执行，那么条件为真。
之前的讨论对第一个case的讨论中我们可以看到如果前后条件需要对整个语句成立，那么必须存在有条件P在循环过程中一直成立！所以对与非b情况也需要有如下表达式

{{P}} WHILE b DO c END {{P ∧ ¬b}}

我们之前说了，在非b的情况中c是会得到执行的，对照霍尔逻辑的定义，那么此时也应该有

{{P ∧ ¬b}} c {{P}

ok,nice

其中P被成为循环的不变量(invariant)

---

喝口水。。。。。

---

下面给出完整的证明：
Proof:
首先 review以下 while的定义

| E_WhileFalse : ∀b st c,
      beval st b = false →
      st =[ WHILE b DO c END ]⇒ st
  | E_WhileTrue : ∀st st' st'' b c,
      beval st b = true →
      st =[ c ]⇒ st' →
      st' =[ WHILE b DO c END ]⇒ st'' →
      st =[ WHILE b DO c END ]⇒ st''

{{fun st => P st /\ bassn b st}} c {{P}} ->
  {{P}} WHILE b DO c END {{fun st => P st /\ not (bassn b st)}}.

假设st 是一个满足前条件P的state, 并且有st =[ WHILE b DO c END ]⇒ st'
我们对st =[ WHILE b DO c END ]⇒ st'进行归纳证明，归纳过程中由while 求值的定义可以看出，有两种可能性一种是E_WhileFalse,一种是E_WhileTrue,接下来分情况讨论。

• E_WhileFasle: 这种情况下 有beval st b = false, P st. goal为P st /\ not (bassn b st) ，这个conjuction 左侧是前条件，已经在条件中，右侧根据beval st b = false，计算得True，左右都为真，这个case得证
• E_WhileTrue: 这种情况下有beval st b = false ，
  IHHe1: c = WHILE b DO c END -> P st -> P st' /\ not (bassn b st)
  IHHe2: WHILE b DO c END = WHILE b DO c END -> P st' -> P st'' /\ not (bassn b st'')
  而此时goal为P st'' /\ not (bassn b st'')
  根据归纳假设2，容易得到若P st'成立则有结论成立.因为条件有 {{fun st => P st /\ bassn b st}} c {{P}} 可以帮助我们给出P st'. 得证。

Q.E.D.