The Science of Programming

Posted on 2013-08-08 Edited on 2015-12-27

Chp 1. Propositions

conjunction: b ^ c

disjunction: b V c

implication: b => c

1.4 Precedence Rules for Operators

The order of evaluation of different, adjacent operators is given by the list: not (has highest precedence and binds tightest), and， or， imp，equals

1.6 Propositions as Sets of States

A proposition represents, or describes，the set of states in which it is true.

Weak & Strong

Proposition b is weaker than c if c =>b. Correspondingly, c is said to be stronger than b. The weakest proposition is T (or any tautology), because it represents the set of all states; the strongest is F.

Chp 2. Reasoning using Equivalence Transformations

An equivalence is an equality that is a tautology.

12条law，所有证明的基础

1. Commutative Laws (These allow us to reorder the operands of and, or and equality):

(E1 ^ E2) = (E2 ^ E1)
(E1 v E2) = (E2 v E1)
(E1 = E2 ) = (E2 = E1)

2. Associative Laws (These allow us to dispense with parentheses when dealing with sequences of and and sequences of or):

E1 ^ (E2 ^ E3) = (E1 ^ E2)^E3 (so write both as E1^E2^E3)
E1 v (E2 v E3) = ( E1 v E2 ) v E3

3. Distributive Laws (These are useful in factoring a proposition, in the same way that we rewrite 2*(3+4) as (2*3)+(2*4)):

E1 v ( E2 ^ E3 ) = (E1 v E2) ^ (E1 v E3 )
E1 ^ (E2 v E3) = ( E1 ^ E 2 ) v ( E1 ^ E3 )

4. De Morgan’s Laws (After Augustus De Morgan, a 19th century English mathematician who，along with Boole，laid much of the foundations for mathematical logic):

┐(E1 ^ E2 ) = ┐E1 v ┐E2
┐(E1 v E2) = ┐E1 ^ ┐E2

5. Law of Negation: ┐(┐E1) = E1
6. Law of the Excluded Middle: E1 v ┐E1 = T
7. Law of Contradiction: E1 ^ ┐El = F
8. Law of Implication: E1 =>E2 = ┐E1 v E2
9. Law of Equality: (El = E2) = (E1 => E2)^(E2=>E1)
10. Laws of or-simplification:

E1 v E1 = E1
E1 v T = T
E1 v F = E1
E1 v (E1 ^ E2 ) = El

11. Laws of and-simplification:

E1 ^ E1 = E1
E1 ^ T = E1
E1 ^ F = F
E1 ^ (E1 v E2) = E1

12. Law of Identity: E1 = E1
比较不容易想到的是第8条和第9条，要牢记，之后的证明会经常用到。另外从上面的基本定理中还可以推导出以下的引理。
重要引理：(E1=>E2) => (E1^E2=>E1)
证明：1) E1^E2=>E1=T 2) E1=>E1^E2=T
= ┓(E1^E2)VE2 = ┓E1V(E1^E2)
= ┓E1V┓E2VE2 = (┓E1VE1)^(┓E1VE2)
= T = T ^ T = T
这个不是那么容易能看出来，所以给出证明。这个推导表示: 如果E1=>E2，表示E1是E2的一个子集

Chp 3. A Natural Deduction System (skip)

Chp 4. Predicates

cand & cor

The operands of these new operators can be any of three values: F, T and U (for Undefined).

cand/cor 支持以下定理

2. Associativity:
E1 cand (E2 cand E3) = (E1 cand E2) cand E3
E1 cor (E2 cor E3) = (E1 cor E2) cor E3
3. Distributivity:
E1 cand (E2 cor E3) = (E1 cand E2) cor (E1 cand E3)
E1 cor (E2 cand E3) = (E1 cor E2) cand (E1 cor E3)

4. De Morgan:
┐(E1 cand E2) = ┐E1 cor ┐E2
┐(El cor E2) = ┐E1 cand ┐E2
6. Excluded Middle: E1 cor ┐E1 = T (provided E1 is well-defined)
7. Contradiction: E1 cand ┐E1 = F (provided E1 is well-defined)
10. cor-simplification
E1 cor E1 = E1
E1 cor T = T (provided El is well-defined)
E1 cor F = E1
E1 cor (E1 cand E2) = E1
11. cand-simplification
E1 cand E1 = E1
E1 cand T = E1
E1 cand F = F (provided El is well-defined)
E1 cand (E1 cor E2) = E1

4.2 Quantification

summarize: (∑: i: 0<i<n:xi)

连乘积: (∏: i: 0<i<n:xi)

exist one: (E: i: 0<i<n: xi)

for all: (A: i: 0<i<n: xi)

free & bound

(A i:m ( i < n : x*i >0)

m, n and x are free identifiers of the predicate. Identifier i is bound.

4.4 Textual Substitution

什么叫bound字符？看下面的例子

But this is not the desired predicate，because the i in y —i has become bound to the quantifier A, since it now occurs within the scope of A.

要这样替换，把bound字符先替换成其他的字符，以免造成confuse。

Chp 5. Notations and Conventions for Arrays

Array b is considered to be a (partial) function: b is a simple variable that contains a function from subscript values to integers.

However, when developing a program to meet the specification it is often advantageous to expand the abbreviations into their full form，because the full form can give more insight into program development.

Chp 6. Using Assertions To Document Programs

{Q}S{R}

Q is called the precondition or input assertion of S; R the postcondition, output assertion or result assertion.

6.3 Proof Outlines

A predicate placed in a program is called an assertion, we assert it is true at that point of execution. A program together with an assertion between each pair of statements is called a proof outline.

Part II The Semantics of a Small Language

Chapter 7 The Predicate Transformer wp

wp( S, R)

The set of all states such that execution of S begun in any one of them is guaranteed to terminate in a finite amount of time in a state satisfying R.

We call wp( S, R ) the weakest precondition of S with respect to R，since it represents the set of all states such that execution begun in any one of them will terminate with R true.

weakest表示更容易达到的条件，所以表示最大子集，一般我们只要找到符合Q=>wp(S, R)的Q。理解这点对未来的推导很重要。

Some properties of wp

Law of the Excluded Miracle: wp ( S, F) = F

Distributivity of Conjunction: wp ( S,Q ) ^ wp ( S,R ) = wp(S, Q ^ R )

Law of Monotonicity: if Q=>R then wp ( S, Q ) ^ w p ( S, R)

证明：利用引理Q=>R => Q^R=Q，则有wp(S,Q)=wp(S, Q^R)=wp(S,Q)^wp(S,R)，

┓wp(S,Q)=┓(wp(S,Q)^wp(S,R))=┓wp(S,Q)V┓wp(S,R)
┓wp(S,Q)Vwp(S,R)=┓wp(S,Q)V┓wp(S,R)Vwp(S,R)=T，得证

Distributivity of Disjunction: wp(S,Q) V wp(S,R) = wp(S,QVR)

证明：原式等价于

(wp(S,Q)=>wp(S,QVR))^(wp(S,R)=>wp(S,QVR))
可以证明Q=>QVR，则上式根据7.5有左右半部分
均为T，即T^T=T，得证

wp( S, Q ) ^ wp ( S, R) = w p ( S, Q ^ R) (for deterministic S)

Chapter 8 The Commands skip，abort and Composition

skip & abort

wp(skip, R) = R

wp(abort, R) = F

(8.3) Definition. wp(“S1; S2”，R) = wp(S1, wp(S2, R)).

Chapter 9 The Assignment Command

*因为编辑器的问题，本笔记所有的

Definition: wp( "x:= e", R) = domain(e) cand Rx/e

domain(e) is a predicate that describes the set of all states in which e may be evaluated - i.e. is well-defined. It must exclude all states in which evaluation of e would be undefined.

Execution of an assignment may change only the variable indicated and evaluation of an expression may change no variable. The ban on side effects is extremely important, for it allows us to consider expressions as conventional mathematical entities.

The definition of wp was used to derive the assignment，and not only to show that the assignment was correct. 这句话很重要，后面第三部分的应用很多时候都是对这句话的阐释。

P137页的Remark，思路很独特，没有在本书后面发现对该例子的使用，罗列如下，目前还不是很理解

9.3 Assignment to an Array Element

本节用到之前章节提出的数组的函数表示法，对该方法的使用可以参看P140 Example 3。展开时，使用到两分法，=i的情况，和≠i的情况

Chapter 10 The Alternative Command

IF：

BB: B1 v B2 v...v Bn

① BB is well-defined

② at least one guard is true

③ Bi =>wp(Si, R)

题目: S = (10.4), R = i<=m ^ p=(N j: 0<=j<i: b[j]>0)

证明（chp10_eg2_prove.txt）:

考虑下面这个式子
(b[i]>0 => i+1<=m ^ p+1=(N j:0<=j<i+1: b[j]>0)) ^ (b[i]<0 => i+1<=m ^ p=(N j:0<=j<i+1: b[j]>0))
1.因为有b[i]>0，所以上式左半边等价于(b[i]>0 => i<m ^ p=(N j:0<=j<i: b[j]>0))
2.同理上式右边等价为(b[i]<0 => i<m ^ p=(N j:0<=j<i: b[j]>0))
所以example 2的证明等价如下：
b[i]≠0 ^ (b[i]>0 => i<m ^ p=(N j:0<=j<i: b[j]>0)) ^ (b[i]<0 => i<m ^ p=(N j:0<=j<i: b[j]>0))
= b[i]≠0 ^ (b[i]≤0 V (i<m ^ p=(N j:0<=j<i: b[j]>0))) ^ (b[i]≥0 V (i<m ^ p=(N j:0<=j<i: b[j]>0)))
= b[i]≠0 ^ ((b[i]≤0 ^ b[i]≥0) V (i<m ^ p=(N j:0<=j<i: b[j]>0)))
= b[i]≠0 ^ (b[i]=0 V (i<m ^ p=(N j:0<=j<i: b[j]>0))
= b[i]≠0 ^ i<m ^ p=(N j:0<=j<i: b[j]>0)

* For purposes of efficiency the programmer could strengthen the guards to excise the nondeterminism. 程序员通常通过加强条件，来消除不确定性以提高程序效率。

Chapter 11 The Iterative Command

Choosing a true guard executing its command is called performing an iteration of the loop.

H0(R) = ┐BB ^ R

The following predicate H0(R) represents the set of states in which execution of DO terminates in 0 iterations with R true, because the guards are initially false.

Iteration: Choosing a true guard executing its command is called performing an iteration of the loop.

Hk(R) = H0(R) v wp (IF，Hk-1(R))，for k>0.

Invariant

A predicate P that is true before and after each iteration of a loop is called an invariant relation, or simply an invariant, of the loop.

Checklist for understanding a loop

1. Show that P is true before execution of the loop begins.
2. Show that {P ^ Bi}Si{P}, for 1≤i≤n. That is，execution of each guarded command terminates with P true, so that P is indeed an invariant of the loop.
3. Show that P^┐BB => R , i.e. upon termination the desired result is true.
4. Show that P^BB =>t>0，so that t is bounded from below as long as the loop has not terminated.
5. Show that {P^Bi } t1:=t; Si {t<t1}, for 1≤i≤n, so that each loop iteration is guaranteed to decrease the bound function.

2,3两条很重要，一般会先得到P,再通过3得到BB，再通过2得到Si。1用来获得初始条件。4,5用来获得bound function，用来验证loop的正确性。纵观整书来说，这个check list应该就是本书的核心。

Chapter 12 Procedure Call (skip)

Part III The Development of Programs

第一部分是理论推导的基础定理，第二部分将该基础定理上升到对程序特征的推导，第三部分将此推导应用到开发程序以及验证程序的正确性。

Chapter 13 Introduction

It is just too difficult to prove an already existing program correct, and it is far better to use the proof-of-correctness ideas throughout the programming process for insight.

formality & common sense

What is needed is a fine balance between the two.

Principle: Use theory to provide insight; use common sense and intuition where it is suitable, but fall back on the formal theory for support when difficulties and complexities arise. 理解这段话很重要

Principle: Know the properties of the objects that are to be manipulated by a program.

Chapter 14 Programming as a Goal-Oriented Activity

Principle: Programming is a goal-oriented activity.

Principle: Before attempting to solve a problem, make absolutely sure you know what the problem is.

Principle: Before developing a program, make precise and refine the pre- and postconditions.

这三条要好好理解，很重要

Strategy for developing an alternative command:

①find a command C whose execution will establish postcondition R in at least some cases.

②find a Boolean B satisfying B=>wp(C, R)

③repeat ①② ---> B1vB2v...vBn = T

关于推导的两个例子如下：eg1 (P186) & eg2 (P189)