# Programming: The derivation of algorithms(Kaldewaij)

Aug 16, 2020

Just the logic.

## Notes in Section 2 (The Guarded Command Language)

### Rules

1. Termination
1. {P} S {false} is eq to [P === false]
2. Strengthen and Weaken.
1. {P} S {Q} and [P_0 => P] implies {P_0} S {Q}
2. {P} S {Q} and [Q => Q_0] implies {P} S {Q_0}
3. And of Post-condition
1. {P} S {Q} and {P} S {R} is eq to {P} S {Q /\ R}
4. Or of Pre-condition
1. {P} S {Q} and {R} S {Q} is eq to {P \/ R} S {Q}
5. Inner Block Rule
1. For predicates P and Q in which y does not occur {P} [| var y: int; S |] {Q} is eq to {P} S {Q}

### Statements or Commands

1. abort: failed to terminate
2. skip: nil
3. assignment: :=
1. Also, expressions may not defined for all values. Then E is defined is denotes as def.E
4. selection: if B.0 -> S.0 || ... || B.n -> S.n fi
1. guarded command: B.i -> S.0
2. the guards that has the value true is chosen non-deterministically and the corresponding statement is executed(?)
5. repetition: do B.0 -> S.0 || ... || B.n -> S.n od
1. until all guards are false, otherwise the statements will be executed repeatedly.
6. arrays: an abbreviation of a set of variables
1. f: array [p..q) of int
2. f: array [0..N) of array [0..M) of int. === f: array (0..N] x (0..M] of int.

### Questions

1. {P} S {false} is equivalent to [P === false ]. Why? How to understand?
1. If S is arbitrary, then it’s easy to understand. Only false leads to false all the time.
2. chosen non-deterministically. Meaning? Why? (In Repetition and Selection)
1. The order does not matter?
3. How to prove terminate? Step by step? May be infeasible.

## Notes in Section 3 (Quantifications)

### Definitions

1. Many practical programming problems involve the computation of a function over a sequence.
1. for a binary operator ⊕ commutative, associative and has e as identity.
2. denote x.0 ⊕ ... ⊕ x.(n-1) as (⊕ i: 0 <= i < n: x.i)
2. a quantification
1. (⊕ x . R : F)
2. x is a list of variables.
3. R is a predicate, the range of the quantification.
4. F is the term
5. (⊕ x . false : F) = e, the identity of ⊕
3. Some examples:
1. (+ x y: 0 <= x < 3 /\ 0 <= y < 3: x * y) = 9
2. (* x: false: F.x) = 1
3. (max i: false: F.i) = -\infinity
4. Some theorems:
1. (⊕ i: false : F) = e
2. (⊕ i: i = x : F) = F(i := x)
3. (⊕ i: R : F) ⊕ (⊕ i : S : F) = (⊕ i : R \/ S : F) ⊕ (⊕ : R /\ S : F)
4. (⊕ i : R : F ) ⊕ (⊕ i : R : G) = (⊕ : R : F ⊕ G)
5. (⊕ i : R.i : (⊕ j : S.j : F.i.j)) = (⊕ j : S.j : (⊕ i : R.i : F.i.j) )
6. When ⊕ is idempotent(幂等的) (x ⊕ x = x), (⊕ i : R \/ S : F) = (⊕ i : R : F) ⊕ (⊕ i : S : F)
7. and x ⊕ (⊕ i : R : F) = (⊕ i : R : x ⊕ F) for R non-empty
8. When ⊗ distributes over ⊕ and e as zero, x ⊗ (⊕ i : R : F) = (⊕ i : R : x ⊗ F)
9. and (⊕ i : R.i : F.i) ⊗ (⊕ i: S.i : G.i) = (⊕ i, j : R.i /\ S.j : F.i ⊗ G.j)
5. A quite different quantifier: the number of, #

## Notes in Section 4 (General Programming Techniques)

### Prepare

1. efficiency: O-notation
2. bound function: the function focused to change the conditions of variables
3. Others are trivial

### Techniques

1. taking conjuncts as invariant
1. the post-condition is of the form P /\ Q
2. take one of the conjuncts as an invariant
3. the other one as negation of the guard of a repetition
4. leading to {P} do ~Q -> S od {P /\ Q}
5. 我的理解：先把一个条件固定满足(established by sth.)，然后写一个循环来更改状态，使得另外的条件也满足。
2. replacing constants by variables
1. for example, use mult to compute exponentiation, need to set a counter
2. replace the Constant (the power) to a variable (the mutable counter)
3. strengthening invariants
1. introduce new invariants and variables
4. tail invariants
1. tail recursion