6. Program Correctness

6.1 About this chapter

6.2 An introduction to algorithms

A description inlcudes:

• A name for the algorithm
• A brief description of the task performed by the algorithm
• A description of the input
• A description of the output
• A sequence of steps to follow

Pseudocode: a language in between written English and a computer language
Assignment: a varaible is given a value

6.3 Greatest common divisor and Euclid’s algorithm

GCD Theorem:
For any positive integers $x$, $y$, $\gcd (x,y)=\gcd (y\mathrm{mod}x,x)$.

Proof:
Let $r=y\mathrm{mod}x=y-jx$, where $j=y\mathrm{div}x$.
If $k\mid x$ and $k\mid y$, then $k\mid (y-jx)$, so $k\mid r$.
Conversely, if $k\mid x$ and $k\mid r$, then $k\mid (r+jx)$, so $k\mid y$.
Thus, $(x,y)$ and $(x,r)$ have the same common divisors. Therefore, $\gcd (x,y)=\gcd (y\mathrm{mod}x,x)$. $\mathrm{QED}$

Input: two positive integers, $x$ and $y$
Output: $\gcd (x,y)$

If (x < y)
    Swap x and y.
r := y mod x.

While (r != 0)
    y := x
    x := r.
    r := y mod x.
End-while

Return (x)

Extendeed Euclidean algorithm:
Finds integers $s,t$ such that $\gcd (x,y)=sx+ty$.
In each iteration, $r=y\mathrm{mod}x=y-dx$, where $d=y\mathrm{div}x$.
The last nonzero remainder is $\gcd (x,y)$. Use back-substitution to find $s$ and $t$.

Multiplicative inverse: $s\in \{1,2,\dots ,n-1\}$ such that $sx\equiv 1(\mathrm{mod}n)$, exists if and only if $\gcd (x,n)=1$

Extended Euclidean Algorithm:
For any integers $x,y$, there exist integers $s,t$, $\gcd (x,y)=sx+ty$.

Proof:
Let $r=y\mathrm{mod}x=y-jx$, where $j=y\mathrm{div}x$.
By the GCD Theorem, $\gcd (x,y)=\gcd (r,x)$. Suppose recursively that $\gcd (r,x)=sr+tx$.
Substituting $r=y-jx$, we get $\gcd (x,y)=s(y-jx)+tx=(t-js)x+sy$.
Thus, the coefficients are updated by $s_{\text{new}}=t-js$ and $t_{\text{new}}=s$.
At the base case $x=0$, $\gcd (0,y)=0\cdot x+1\cdot y$.
Therefore, back-substitution produces integers $s,t$ satisfying $\gcd (x,y)=sx+ty$. $\mathrm{QED}$

6.4 Fast exponentiation

Input: positive integers $x$, $y$, and $n$.
Output: $x^y\mathrm{mod}n$

p := 1
s := x
r := y
While (r > 0)
    If (r mod 2 = 1)
        p := p * s mod n
    s = s * s mod n
    r = r div 2
End-while

6.5 Loop invariants

NOTE: SLIGHTLY DIFFERENT APPROACH TAUGHT IN CLASS

Program verification: formally proving that programs perform correctly
A program’s correct behavior:

• Precondition is true before program starts
• The program will end after a finite number of steps
• Postcondition is true after the program ends

If the loop condition for a while loop is true, the instructions inside the loop are executed.
Loop invariant: an assertation that is true before each iteration of a loop

Let $C$ indicate loop condition and $I$ indicate loop invariant. Using a loop invariant:

1. The precondition is true before the loop begins, then $I$ is also true
2. $C$ and $I$ are both true before an iteration of the loop, then $I$ is true after the iteration
3. The condition $C$ will eventually be false
4. Show that if $\neg C$ and $I$ are both true, then the postcondition is true

Example:
Precondition: $n\ge 0,j=0,power=1$
Postcondition: $power=x^n$
Loop Invariant: $j\le n,power=x^j$, and $j$ is an integer.

Step 1: Initialization
Since $j=0\le n$ and $power=1=x^0$, the invariant is true.

Step 2: Maintenance
After one iteration:

• $j_2=j_1+1\le n$
• $powe{r}_2=powe{r}_{1}x=x^{j_1+1}=x^{j_2}$
  $j_2$ is an integer. Thus, the invariant holds.

Step 3: Termination
$j$ increases by 1 each time. When $j=n$, the loop stops.

Step 4: Correctness
Loop ends: $j\ge n$.
Invariant: $j\le n$.
Thus, $j=n$, so $power=x^j=x^n$.