Advanced Programming and Algorithms I

Winter 2022/2023

Anja Rey

31th October 2021

Recap Last Week

insertion_sort(A[0..n], n):
1 def insertio n_sort ( sequence ) :

1 for j Ω 1 to n ≠ 1 do 2 for j in range (1 , len ( sequence ) ) :

2 key Ω A[j] 3 key = sequence [ j ]

insert_key ( sequence , j , key )

3 insert key into A[0..j ≠ 1] 4

Running Time:

• RAM model, count steps • measuring time (seconds)

• asymptotic worst-case analysis • programme optimisation

27/50 Advanced Programming and Algorithms I – Efficiency Anja Rey



Correctness & Code Quality I

Algorithm Correctness Proof

How do we know whether our algorithm works?

28/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey


Algorithm Correctness Proof

How do we know whether our algorithm works?

Intuition: Derive statements from axioms or previously shown statements using logical implications.

28/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey


Algorithm Correctness Proof

How do we know whether our algorithm works?

Intuition: Derive statements from axioms or previously shown statements using logical implications.

What do we know? What do we want to show?

28/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey


Algorithm Correctness Proof

How do we know whether our algorithm works?

Intuition: Derive statements from axioms or previously shown statements using logical implications.

What do we know? What do we want to show?

Correctness of an Algorithm

An algorithm is correct ≈∆

each input generates the output as sepcified in the computation problem.

28/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey


Algorithm Correctness Proof

How do we know whether our algorithm works?

Intuition: Derive statements from axioms or previously shown statements using logical implications.

What do we know? What do we want to show?

Correctness of an Algorithm

An algorithm is correct ≈∆

each input generates the output as sepcified in the computation problem.

How can we show this?

Axiom

a basic operation in pseudocode works according to the specification

(e.g. x Ω x + 1: 1 is added to the value of x and the sum is assigned to variable x .)

XENA

28/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey


Algorithm Correctness Proof Example

model input integer a bez threshold KEIN

output Boolean True Es la b t

correct es Einputofthisform

ist jut threshold

is_distance_below_threshold(a, b, t):

1 d Ω |a ≠ b| axiom computation la b assignment

2 if d < t then

return True condition holds

4 return False
run
if

la blat then returns True

If

claim

Lied d is la b

Proof assuela blct.in assyd

d la b at d and holds 1.3 run Truerot

dein E show contraposihon show if la blzt
sretwusFals assela

blzt.lt d la bl dit
prog continues to line 4

29/50
rot True
Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey


Loop Invariant

factorial(n):

What if the proof depends on a (variable) number

x Ω1
of runs of the loop?
1

2 for i Ω 1 to n do

3 x Ωx ·i

4 return x

30/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey


Loop Invariant

factorial(n):

What if the proof depends on a (variable) number

x Ω1
of runs of the loop?
1

2 for i Ω 1 to n do

3 x Ωx ·i Tool: a statement that holds at the beginning (and

4 return x end) of each loop iteration.

30/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey


Loop Invariant

factorial(n):

What if the proof depends on a (variable) number

x Ω1
of runs of the loop?
1

2 for i Ω 1 to n do

3 x Ωx ·i Tool: a statement that holds at the beginning (and

4 return x end) of each loop iteration.

Loop invariant

• statement A(i) that depends on iteration i

30/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey


Loop Invariant

factorial(n):

What if the proof depends on a (variable) number

x Ω1
of runs of the loop?
1

2 for i Ω 1 to n do

3 x Ωx ·i Tool: a statement that holds at the beginning (and

4 return x end) of each loop iteration.

Loop invariant

• statement A(i) that depends on iteration i

• initialisation: A(1) holds at the beginning of the first loop iteration.

30/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey


Loop Invariant

factorial(n):

What if the proof depends on a (variable) number

x Ω1
of runs of the loop?
1

2 for i Ω 1 to n do AG
x Ωx ·i Tool: a statement that holds at the beginning (and
LEANN

4 return x end) of each loop iteration.

Loop invariant

• statement A(i) that depends on iteration i

• initialisation: A(1) holds at the beginning of the first loop iteration.

• maintenance: assuming A(i) holds at the beginning of loop iteration i,

then A(i + 1) holds at the end of loop iteration i,

and, thus, at the beginning of iteration i + 1.

30/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey


Loop Invariant

factorial(n):

What if the proof depends on a (variable) number

x Ω1

2
µ
for j Ω 2 to n do
I un
of runs of the loop?

3 x Ωx ·j Tool: a statement that holds at the beginning (and

4 return x end) of each loop iteration.

Loop invariant (for loop variable j Ω a to b)

• statement A(j) that depends on iteration j, a Æ j Æ b

• initialisation: A(a) holds at the beginning of the first loop iteration.

• maintenance: assuming A(j) holds at the beginning of loop iteration j,

then A(j + 1) holds at the end of loop iteration j,

and, thus, at the beginning of iteration j + 1.

30/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey


Loop Invariant

factorial(n):

What if the proof depends on a (variable) number

x Ω1
of runs of the loop?
1

for j Ω 2 to n do
jena

3 x Ωx ·j Tool: a statement that holds at the beginning (and

4 return x end) of each loop iteration.

Loop invariant (for loop variable j Ω a to b)

• statement A(j) that depends on iteration j, a Æ j Æ b

• initialisation: A(a) holds at the beginning of the first loop iteration.

0

• maintenance: assuming A(j) holds at the beginning of loop iteration j,

then A(j + 1) holds at the end of loop iteration j,

and, thus, at the beginning of iteration j + 1.

termination: implication for end of loop: for j = b + 1, loop condition not satisfied.

Statement A(b + 1) holds after the whole loop.

30/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey


Loop Invariant

factorial(n):

What if the proof depends on a (variable) number

x Ω1
of runs of the loop?
1

2 for j Ω 2 to n do

3 x Ωx ·j Tool: a statement that holds at the beginning (and

4 return x end) of each loop iteration.

Loop invariant (for loop variable j Ω a to b)

• statement A(j) that depends on iteration j, a Æ j Æ b

• initialisation: A(a) holds at the beginning of the first loop iteration.

• maintenance: assuming A(j) holds at the beginning of loop iteration j,

then A(j + 1) holds at the end of loop iteration j,

and, thus, at the beginning of iteration j + 1.

termination: implication for end of loop: for j = b + 1, loop condition not satisfied.

Statement A(b + 1) holds after the whole loop.

30/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey


dein

iteration with loop reichte

ä

j
2ejencoud.h

enH

inaiiFxi

Proof Init 2

before the first

Meint us
Aljte look at loop

AG jagen
mit

lassen Alp
then 1.3
Iii

in x

x
j Aljtikolds

dofjusbergofthend

D loopino

use this AG

Termination the loopljnt17 A

nkold IisxYIii

after

n returned in14 Direct

Loop Invariant Continued

Insertion sort solves the Sorting problem.

31/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey
 Claim Insertion sort solves
the song probt
input segnen u output
sorted
aserdy

i
genau an
uns
adai.az
auanzjs

invariant for the inner while top 3 6

Prof
inveret for the outer for top
implicate for the whole algorithm

ftp.kjen adkey AT loop in

Sati beging of each iterate of Rechte
at the loop
Laith vor
i is the index s.tk all values in AEitz 1
are j
Key

Fft see
and

Proof init i
ja
123in

meint
II Tutu
im i
assenAlita j0
1 A key lead
14 candies i Ky
1.5 ATADEAE
AEHM also
MAE
sky Cory is edged
AEHM D D SEIN
We know now Safi after loop O ALT IM
Tor AE Key AEthj

z Key AG

Clan of the originally

Sali tausists canted dents
in ascending oder
Proof init inbeging mehende
je 1 de is soled
malt
jusjtlloop as.sn
1.2 Key
Sag AT
1.3 6 5 holds
Key AG composition
17 key is inserted
corn insehed aft
j into ATO
g
j SzEnIhold OwholeATO.n
Iorig.dem.edissated
Loop Invariant Continued

Insertion sort solves the Sorting problem.

Teaser: Correctness of recursive functions in Part II

Now: Understanding loop invariants can also help to refactor code (and vice versa).

31/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey
Python: Code Quality I

https://xkcd.com/844 (CC BY-NC 2.5)

32/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey
Python: Code Quality I

Goals
• readability
• maintainability

https://xkcd.com/844 (CC BY-NC 2.5)

32/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey
Python: Code Quality I

Goals
• readability
• maintainability
How do we achieve that?
• consistency (e. g. spacing conventions)
• expressivity (e. g. variable names)
• functions:
• extendability
• unique purpose
• brevity
• testability
• avoiding redundancy

https://xkcd.com/844 (CC BY-NC 2.5)

32/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey
Python: Code Quality I

Goals
• readability
• maintainability
How do we achieve that?
• consistency (e. g. spacing conventions)
• expressivity (e. g. variable names)
• functions:
• extendability
• unique purpose
• brevity
• testability
• avoiding redundancy
; Refactoring
https://xkcd.com/844 (CC BY-NC 2.5)

32/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey
Testing

How do we find out whether our code works practically?

33/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey
Testing

How do we find out whether our code works practically?

Idea: test driven development

1. First write a test function

33/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey
Testing

How do we find out whether our code works practically?

Idea: test driven development

1. First write a test function

• asserts a specific input-output relationship

33/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey
Testing

How do we find out whether our code works practically?

Idea: test driven development

1. First write a test function

• asserts a specific input-output relationship
• ideally, one test for one purpose

33/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey
Testing

How do we find out whether our code works practically?

Idea: test driven development

1. First write a test function

• asserts a specific input-output relationship
• ideally, one test for one purpose
• no proof, but verification for representative case or edge case

33/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey
Testing

How do we find out whether our code works practically?

Idea: test driven development

1. First write a test function

• asserts a specific input-output relationship
• ideally, one test for one purpose
• no proof, but verification for representative case or edge case

2. Then implement the function that fulfils the test

33/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey
Testing

How do we find out whether our code works practically?

Idea: test driven development

1. First write a test function

• asserts a specific input-output relationship
• ideally, one test for one purpose
• no proof, but verification for representative case or edge case

2. Then implement the function that fulfils the test

continuous process of testing, programming, and refactoring

33/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey
Testing

How do we find out whether our code works practically?

Idea: test driven development

1. First write a test function

• asserts a specific input-output relationship
• ideally, one test for one purpose
• no proof, but verification for representative case or edge case

2. Then implement the function that fulfils the test

continuous process of testing, programming, and refactoring

simulate in jupyter notebook, e. g., using assert

1 assert [1 ,2 ,3] == insert ion_sort ([2 ,3 ,1])

33/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey
Coding Style Guidelines Overview

Most common: PEP 8 style guide https://peps.python.org/pep-0008/

Conventions for spacing, code layout, . . . : example:

1 x =1 1 x = 1
2

3
for i in range ( 1 , 100 ) :
x = 2 * x+i
An 2

3
for i in range (1 , 100) :
x = 2* x + i

Naming conventions: expressive, recognisable, searchable

e. g. variables (lower_case_with_underscores): left_index, edge_weight,
functions (verbs) is_sorted, find_shortest_distance

Functions: properties:
• short (Æ 6 lines),
• one purpose (otherwise extract a substep)
• testable (well-defined input–output relation, return value)
• as general as possible (extendable, reusable, easy to adapt in the future)

34/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey
Coding Style Guidelines Overview

Most common: PEP 8 style guide https://peps.python.org/pep-0008/

Conventions for spacing, code layout, . . . : example:

1 x =1 1 x = 1
2

3
for i in range ( 1 , 100 ) :
x = 2 * x+i
An 2

3
for i in range (1 , 100) :
x = 2* x + i

Naming conventions: expressive, recognisable, searchable

e. g. variables (lower_case_with_underscores): left_index, edge_weight,
functions (verbs) is_sorted, find_shortest_distance

Functions: properties:
• short (Æ 6 lines),
• one purpose (otherwise extract a substep)
• testable (well-defined input–output relation, return value)
• as general as possible (extendable, reusable, easy to adapt in the future)

34/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey
Coding Style Guidelines Overview

Most common: PEP 8 style guide https://peps.python.org/pep-0008/

Conventions for spacing, code layout, . . . : example:

1 x =1 1 x = 1
2

3
for i in range ( 1 , 100 ) :
x = 2 * x+i
An 2

3
for i in range (1 , 100) :
x = 2* x + i

Naming conventions: expressive, recognisable, searchable

e. g. variables (lower_case_with_underscores): left_index, edge_weight,
functions (verbs) is_sorted, find_shortest_distance

Functions: properties:
• short (Æ 6 lines),
• one purpose (otherwise extract a substep)
• testable (well-defined input–output relation, return value)
• as general as possible (extendable, reusable, easy to adapt in the future)

34/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey
quiz

35/50 Advanced Programming and Algorithms I – Correctness & Code Quality I Anja Rey