1. Correctness

A program is correct if it produces correct output for every valid input.

• Partial correctness: if the program terminates ⇒ output is correct
• Termination: program always terminates

2. Hoare Triple

Notation:

$$p\{S\}q$$

• $p$: initial assertion
• $q$: final assertion
• $S$: program

Meaning:

If $p$ is true and $S$ terminates, then $q$ is true.

3. Partial Correctness

$$(p\wedge \text{S terminates})\Rightarrow q$$

Note: does NOT guarantee termination.

4. Composition Rule

If:

$$p\{S_1\}q$$$$q\{S_2\}r$$

Then:

$$p\{S_1;S_2\}r$$

5. Conditional Statements

5.1 If (no else)

if condition then S

Rule:

$$(p\wedge condition)\{S\}q$$$$(p\wedge \mathrm{\neg }condition)\Rightarrow q$$

Therefore:

$$p\{\text{if condition then }S\}q$$

5.2 If-Else

if condition then S1 else S2

Rule:

$$(p\wedge condition)\{S_1\}q$$$$(p\wedge \mathrm{\neg }condition)\{S_2\}q$$

Therefore:

$$p\{\text{if condition then }{S}_1\text{ else }{S}_2\}q$$

5.3 Rule of Inference: If – Else If – ... – Else

if condition1 then S1
else if condition2 then S2
...
else Sn

Rule

Để chứng minh:

$$p\{\text{if-else chain}\}q$$

Ta cần chứng minh các điều sau:

$$(p\wedge conditio{n}_1)\{S_1\}q$$$$(p\wedge \mathrm{\neg }conditio{n}_1\wedge conditio{n}_2)\{S_2\}q$$$$(p\wedge \mathrm{\neg }conditio{n}_1\wedge \mathrm{\neg }conditio{n}_2\wedge conditio{n}_3)\{S_3\}q$$$$⋮$$$$(p\wedge \mathrm{\neg }conditio{n}_1\wedge \cdots \wedge \mathrm{\neg }conditio{n}_{n-1})\{S_n\}q$$

Kết luận

$$p\{\text{if condition1 then }{S}_1\text{else if condition2 then }{S}_2\cdots \text{else }{S}_n\}q$$

6. Loop Invariant (While)

while condition do S

Definition

$p$ is a loop invariant if:

$$(p\wedge condition)\{S\}p$$

While Rule

If:

$$(p\wedge condition)\{S\}p$$

Then:

$$p\{\text{while condition }S\}(\mathrm{\neg }condition\wedge p)$$

7. Intuition

• Invariant = something always true during the loop
• When loop ends:
  • condition = false
  • invariant still true

⇒ derive final result

8. Proof Checklist for While

1. Initialization:

$$p\text{ holds before loop}$$

2. Maintenance:

$$(p\wedge condition)\{S\}p$$

3. Termination:

$$\mathrm{\neg }condition\wedge p\Rightarrow q$$