光阴冢

We make choices and life has a way of making us pay for them.

Programming: The derivation of algorithms(Kaldewaij)

Jul 7, 2020  

Section 0-1

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