## Section 0-1

Just the logic.

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

### Rules

- Termination
`{P} S {false} is eq to [P === false]`

- Strengthen and Weaken.
`{P} S {Q} and [P_0 => P] implies {P_0} S {Q}`

`{P} S {Q} and [Q => Q_0] implies {P} S {Q_0}`

- And of Post-condition
`{P} S {Q} and {P} S {R} is eq to {P} S {Q /\ R}`

- Or of Pre-condition
`{P} S {Q} and {R} S {Q} is eq to {P \/ R} S {Q}`

- Inner Block Rule
- For predicates P and Q in which y does not occur
`{P} [| var y: int; S |] {Q} is eq to {P} S {Q}`

- For predicates P and Q in which y does not occur

### Statements or Commands

**abort**: failed to terminate**skip**: nil**assignment**:`:=`

- Also, expressions may not defined for all values. Then E is defined is denotes as
`def.E`

- Also, expressions may not defined for all values. Then E is defined is denotes as
**selection**:`if B.0 -> S.0 || ... || B.n -> S.n fi`

- guarded command:
`B.i -> S.0`

- the guards that has the value true is chosen
**non-deterministically**and the corresponding statement is executed(?)

- guarded command:
**repetition**:`do B.0 -> S.0 || ... || B.n -> S.n od`

- until all guards are false, otherwise the statements will be executed repeatedly.

**arrays**: an abbreviation of a set of variables`f: array [p..q) of int`

`f: array [0..N) of array [0..M) of int. === f: array (0..N] x (0..M] of int.`

### Questions

`{P} S {false} is equivalent to [P === false ].`

Why? How to understand?- If S is arbitrary, then it’s easy to understand. Only false leads to false all the time.

- chosen
*non-deterministically*. Meaning? Why? (In**Repetition**and**Selection**)- The order does not matter?

- How to prove terminate? Step by step? May be infeasible.

## Notes in Section 3 (Quantifications)

### Definitions

- Many practical programming problems involve the computation of a function over a sequence.
- for a binary operator ⊕ commutative, associative and has e as identity.
- denote
`x.0 ⊕ ... ⊕ x.(n-1)`

as`(⊕ i: 0 <= i < n: x.i)`

- a quantification
`(⊕ x . R : F)`

- x is a list of
*variables*. - R is a
*predicate*, the range of the quantification. - F is the
*term* `(⊕ x . false : F) = e`

, the identity of ⊕

- Some examples:
`(+ x y: 0 <= x < 3 /\ 0 <= y < 3: x * y) = 9`

`(* x: false: F.x) = 1`

`(max i: false: F.i) = -\infinity`

- Some theorems:
`(⊕ i: false : F) = e`

`(⊕ i: i = x : F) = F(i := x)`

`(⊕ i: R : F) ⊕ (⊕ i : S : F) = (⊕ i : R \/ S : F) ⊕ (⊕ : R /\ S : F)`

`(⊕ i : R : F ) ⊕ (⊕ i : R : G) = (⊕ : R : F ⊕ G)`

`(⊕ i : R.i : (⊕ j : S.j : F.i.j)) = (⊕ j : S.j : (⊕ i : R.i : F.i.j) )`

- When ⊕ is idempotent(幂等的)
`(x ⊕ x = x), (⊕ i : R \/ S : F) = (⊕ i : R : F) ⊕ (⊕ i : S : F)`

- and
`x ⊕ (⊕ i : R : F) = (⊕ i : R : x ⊕ F)`

for R non-empty - When ⊗ distributes over ⊕ and e as zero,
`x ⊗ (⊕ i : R : F) = (⊕ i : R : x ⊗ F)`

- and
`(⊕ i : R.i : F.i) ⊗ (⊕ i: S.i : G.i) = (⊕ i, j : R.i /\ S.j : F.i ⊗ G.j)`

- A quite different quantifier: the number of, #

## Notes in Section 4 (General Programming Techniques)

### Prepare

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

### Techniques

- taking conjuncts as invariant
- the post-condition is of the form
`P /\ Q`

- take one of the conjuncts as an invariant
- the other one as negation of the guard of a repetition
- leading to
`{P} do ~Q -> S od {P /\ Q}`

- 我的理解：先把一个条件固定满足(established by sth.)，然后写一个循环来更改状态，使得另外的条件也满足。

- the post-condition is of the form
- replacing constants by variables
- for example, use mult to compute exponentiation, need to set a counter
- replace the Constant (the power) to a variable (the mutable counter)

- strengthening invariants
- introduce new invariants and variables

- tail invariants
- tail recursion