Algorithms and Data Structures Lecture Notes 2024/25 PDF
Document Details
Uploaded by HallowedEinstein
Technische Universität Hamburg-Harburg
2024
Matthias Mnich
Tags
Related
- TMF1434 Data Structure and Algorithms PDF
- DSA Notes - Data Structures and Algorithms PDF
- Data Structures & Algorithms - Topic 15 - Selection, Insertion, Bubble & Shell Sort - Lecture Slides
- Data Structures and Algorithms(All Sessions) PDF
- A Practical Introduction to Data Structures and Algorithms (Java) PDF
- Sorting Algorithms PDF
Summary
This document provides lecture notes on algorithms and data structures, specifically focusing on sorting. It includes a definition of the sorting problem, an overview of the insertion sort algorithm, and a framework for proving its correctness. The notes are part of a course for undergraduate students.
Full Transcript
1 Algorithms and Data Structures Winter Term 2024/25 1st Lecture Chapter 1: Sorting Prof. Dr. Matthias Mnich Institute for Algorithms and Complexity 2-1 Th...
1 Algorithms and Data Structures Winter Term 2024/25 1st Lecture Chapter 1: Sorting Prof. Dr. Matthias Mnich Institute for Algorithms and Complexity 2-1 The problem Given: an array A = ⟨a1 , a2 ,... , an ⟩ of n numbers 2-2 The problem Given: an array A = ⟨a1 , a2 ,... , an ⟩ of n numbers Wanted: a permutation ⟨a1′ , a2′ ,... , an′ ⟩ of A, such that a1′ ≤ a2′ ≤... ≤ an′ 2-3 The problem Given: an array A = ⟨a1 , a2 ,... , an ⟩ of n numbers Wanted: a permutation ⟨a1′ , a2′ ,... , an′ ⟩ of A, such that a1′ ≤ a2′ ≤... ≤ an′ 2-4 The problem input Given: an array A = ⟨a1 , a2 ,... , an ⟩ of n numbers Wanted: a permutation ⟨a1′ , a2′ ,... , an′ ⟩ of A, such that a1′ ≤ a2′ ≤... ≤ an′ output 2-5 The problem input Given: an array A = ⟨a1 , a2 ,... , an ⟩ of n numbers Wanted: a permutation ⟨a1′ , a2′ ,... , an′ ⟩ of A, such that a1′ ≤ a2′ ≤... ≤ an′ output 2-6 The problem input Given: an array A = ⟨a1 , a2 ,... , an ⟩ of n numbers Algorithm Wanted: a permutation ⟨a1′ , a2′ ,... , an′ ⟩ of A, such that a1′ ≤ a2′ ≤... ≤ an′ output 2-7 The problem input Given: an array A = ⟨a1 , a2 ,... , an ⟩ of n numbers Algorithm Wanted: a permutation ⟨a1′ , a2′ ,... , an′ ⟩ of A, such that a1′ ≤ a2′ ≤... ≤ an′ output Observe: Internal representation of numbers unimportant! 2-8 The problem input Given: an array A = ⟨a1 , a2 ,... , an ⟩ of n numbers Algorithm Wanted: a permutation ⟨a1′ , a2′ ,... , an′ ⟩ of A, such that a1′ ≤ a2′ ≤... ≤ an′ output Observe: Internal representation of numbers unimportant! Important: 2-9 The problem input Given: an array A = ⟨a1 , a2 ,... , an ⟩ of n numbers Algorithm Wanted: a permutation ⟨a1′ , a2′ ,... , an′ ⟩ of A, such that a1′ ≤ a2′ ≤... ≤ an′ output Observe: Internal representation of numbers unimportant! Important: Each pair of numbers is comparable. A comparison takes constant time“, ” i.e. the run time is independent of n. 2-1 The problem input Given: an array A = ⟨a1 , a2 ,... , an ⟩ of n numbers Algorithm Wanted: a permutation ⟨a1′ , a2′ ,... , an′ ⟩ of A, such that a1′ ≤ a2′ ≤... ≤ an′ output Observe: Internal representation of numbers unimportant! Important: Each pair of numbers is comparable. A comparison takes constant time“, ” i.e. the run time is independent of n. Remark: 0110011101 0000111111 2-1 The problem input Given: an array A = ⟨a1 , a2 ,... , an ⟩ of n numbers Algorithm Wanted: a permutation ⟨a1′ , a2′ ,... , an′ ⟩ of A, such that a1′ ≤ a2′ ≤... ≤ an′ output Observe: Internal representation of numbers unimportant! Important: Each pair of numbers is comparable. A comparison takes constant time“, ” i.e. the run time is independent of n. Remark: 0110011101 0000111111 2-1 The problem input Given: an array A = ⟨a1 , a2 ,... , an ⟩ of n numbers Algorithm Wanted: a permutation ⟨a1′ , a2′ ,... , an′ ⟩ of A, such that a1′ ≤ a2′ ≤... ≤ an′ output Observe: Internal representation of numbers unimportant! Important: Each pair of numbers is comparable. A comparison takes constant time“, ” i.e. the run time is independent of n. Remark: 0110011101 0000111111 2-1 The problem input Given: an array A = ⟨a1 , a2 ,... , an ⟩ of n numbers Algorithm Wanted: a permutation ⟨a1′ , a2′ ,... , an′ ⟩ of A, such that a1′ ≤ a2′ ≤... ≤ an′ output Observe: Internal representation of numbers unimportant! Important: Each pair of numbers is comparable. A comparison takes constant time“, ” i.e. the run time is independent of n. Remark: 0110011101 0000111111 2-1 The problem input Given: an array A = ⟨a1 , a2 ,... , an ⟩ of n numbers rearrangement Algorithm Wanted: a permutation ⟨a1′ , a2′ ,... , an′ ⟩ of A, such that a1′ ≤ a2′ ≤... ≤ an′ output Observe: Internal representation of numbers unimportant! Important: Each pair of numbers is comparable. A comparison takes constant time“, ” i.e. the run time is independent of n. Remark: 0110011101 0000111111 3-1 Question for all freshmen 3-2 Question for all freshmen How do you sort? 4-1 One solution InsertionSort Illustrations from: Algorithms: An Introduction“ (Cormen et al., MIT Press, 2. Aufl., 2001 ” 4-2 One solution InsertionSort Start with the left hand empty and all cards on the table. Illustrations from: Algorithms: An Introduction“ (Cormen et al., MIT Press, 2. Aufl., 2001 ” 4-3 One solution InsertionSort Start with the left hand empty and all cards on the table. Right hand takes up cards one after another and places them (starting from the right) at the correct position between the cards in the left hand. Illustrations from: Algorithms: An Introduction“ (Cormen et al., MIT Press, 2. Aufl., 2001 ” 4-4 One solution InsertionSort Start with the left hand empty and all cards on the table. Right hand takes up cards one after another and places them (starting from the right) at the correct position between the cards in the left hand. Cards are always kept in sorted order in the left hand. Illustrations from: Algorithms: An Introduction“ (Cormen et al., MIT Press, 2. Aufl., 2001 ” 4-5 One solution InsertionSort Start with the left hand empty and all cards on the table. Right hand takes up cards one after another and places them (starting from the right) at the correct position between the cards in the left hand. Cards are always kept in sorted order in the left hand. Illustrations from: Algorithms: An Introduction“ (Cormen et al., MIT Press, 2. Aufl., 2001 ” 4-6 One solution InsertionSort Start with the left hand empty and all cards on the table. Right hand takes up cards one after another and places them (starting from the right) at the correct position between the cards in the left hand. incremental alg. Cards are always kept in sorted order in the left hand. Illustrations from: Algorithms: An Introduction“ (Cormen et al., MIT Press, 2. Aufl., 2001 ” 4-7 One solution InsertionSort Start with the left hand empty and all cards on the table. Right hand takes up cards one after another and places them (starting from the right) at the correct position between the cards in the left hand. incremental alg. Cards are always kept in sorted order in the left hand. Illustrations from: Algorithms: An Introduction“ (Cormen et al., MIT Press, 2. Aufl., 2001 ” 4-8 One solution InsertionSort Start with the left hand empty and all cards on the table. Right hand takes up cards one after another and places them (starting from the right) at the correct position between the cards in the left hand. incremental alg. Cards are always kept in sorted order in the left hand. Invariant! Illustrations from: Algorithms: An Introduction“ (Cormen et al., MIT Press, 2. Aufl., 2001 ” 4-9 One solution InsertionSort Start with the left hand empty and all cards on the table. Right hand takes up cards one after another and places them (starting from the right) at the correct position between the cards in the left hand. incremental alg. Cards are always kept in sorted order in the left hand. Invariant! ⇓ Correctness Illustrations from: Algorithms: An Introduction“ (Cormen et al., MIT Press, 2. Aufl., 2001 ” 4-1 One solution InsertionSort Start with the left hand empty and all cards on the table. Right hand takes up cards one after another and places them (starting from the right) at the correct position between the cards in the left hand. incremental alg. Cards are always kept in sorted order in the left hand. Invariant! ⇓ Correctness: eventually all cards end up in the left hand – and thus are sorted! Illustrations from: Algorithms: An Introduction“ (Cormen et al., MIT Press, 2. Aufl., 2001 ” 5-1 An incremental algorithm // In pseudocode 5-2 An incremental algorithm // In pseudocode IncrementalAlg( array of... A ) 5-3 An incremental algorithm // In pseudocode IncrementalAlg( array of... A ) | {z } name of the alg. 5-4 An incremental algorithm // In pseudocode IncrementalAlg( array of... A ) | {z } | {z } name of the alg. input 5-5 An incremental algorithm // In pseudocode type of the input IncrementalAlg( array of... A ) | {z } | {z } name of the alg. input 5-6 An incremental algorithm // In pseudocode type of the input IncrementalAlg( array of... A ) | {z } | {z } variable name of the alg. input 5-7 An incremental algorithm // In pseudocode IncrementalAlg( array of... A ) 5-8 An incremental algorithm // In pseudocode IncrementalAlg( array of... A ) compute solution for A 5-9 An incremental algorithm // In pseudocode IncrementalAlg( array of... A ) compute solution for A // initialisation 5-1 An incremental algorithm // In pseudocode IncrementalAlg( array of... A ) compute solution for A // initialisation for j = 2 to A.length do 5-1 An incremental algorithm // In pseudocode IncrementalAlg( array of... A ) compute solution for A // initialisation for j = 2 to A.length do // loop head 5-1 An incremental algorithm // In pseudocode IncrementalAlg( array of... A ) compute solution for A // initialisation for j = 2 to A.length do // loop head assignment operator 5-1 An incremental algorithm // In pseudocode IncrementalAlg( array of... A ) compute solution for A // initialisation for j = 2 to A.length do // loop head assignment operator – in some languages j := 2 – in some books j ←2 5-1 An incremental algorithm // In pseudocode IncrementalAlg( array of... A ) compute solution for A // initialisation for j = 2 to A.length do // loop head assignment operator – in some languages j := 2 – in some books j ←2 – in Java and Python j = 2 5-1 An incremental algorithm // In pseudocode IncrementalAlg( array of... A ) compute solution for A // initialisation for j = 2 to A.length do // loop head number of elements in the array A assignment operator – in some languages j := 2 – in some books j ←2 – in Java and Python j = 2 5-1 An incremental algorithm // In pseudocode IncrementalAlg( array of... A ) compute solution for A // initialisation for j = 2 to A.length do // loop head // loop body; is executed (A.length − 1) times 5-1 An incremental algorithm // In pseudocode IncrementalAlg( array of... A ) compute solution for A // initialisation for j = 2 to A.length do // loop head // loop body; is executed (A.length − 1) times compute solution for A[1..j ] using soln. for A[1..j − 1] 5-1 An incremental algorithm // In pseudocode IncrementalAlg( array of... A ) compute solution for A // initialisation for j = 2 to A.length do // loop head // loop body; is executed (A.length − 1) times compute solution for A[1..j ] using soln. for A[1..j − 1] subarray of A with elements A, A,... , A[j ] 5-1 An incremental algorithm // In pseudocode IncrementalAlg( array of... A ) compute solution for A // initialisation for j = 2 to A.length do // loop head // loop body; is executed (A.length − 1) times compute solution for A[1..j ] using soln. for A[1..j − 1] return solution subarray of A with elements A, A,... , A[j ] 5-2 An incremental algorithm // In pseudocode IncrementalAlg( array of... A ) compute solution for A // initialisation for j = 2 to A.length do // loop head // loop body; is executed (A.length − 1) times compute solution for A[1..j ] using soln. for A[1..j − 1] return solution // output result subarray of A with elements A, A,... , A[j ] 5-2 An incremental algorithm IncrementalAlg( array of... A ) compute solution for A for j = 2 to A.length do compute solution for A[1..j ] using soln. for A[1..j − 1] return solution 5-2 An incremental algorithm InsertionSort IncrementalAlg( array of.int.. A ) // We will write this as: int[ ] A compute solution for A for j = 2 to A.length do compute solution for A[1..j ] using soln. for A[1..j − 1] return solution 5-2 An incremental algorithm InsertionSort IncrementalAlg( array of.int.. A ) // We will write this as: int[ ] A compute solution for A // nothing to do: A[1..1] ist sorted for j = 2 to A.length do compute solution for A[1..j ] using soln. for A[1..j − 1] return solution 5-2 An incremental algorithm InsertionSort IncrementalAlg( array of.int.. A ) // We will write this as: int[ ] A compute solution for A // nothing to do: A[1..1] ist sorted for j = 2 to A.length do // compute solution for A[1..j] using soln. for A[1..j − 1]... discussed later... return solution 5-2 An incremental algorithm InsertionSort IncrementalAlg( array of.int.. A ) // We will write this as: int[ ] A compute solution for A // nothing to do: A[1..1] ist sorted for j = 2 to A.length do // compute solution for A[1..j] using soln. for A[1..j − 1]... discussed later... return solution // not necessary – the overlying program has access to the sorted field A 5-2 An incremental algorithm InsertionSort IncrementalAlg( array of.int.. A ) // We will write this as: int[ ] A compute solution for A // nothing to do: A[1..1] ist sorted for j = 2 to A.length do // compute solution for A[1..j] using soln. for A[1..j − 1] // here: insert A[ j] into the sorted array A[1..j − 1] A[ j ] A[1..j − 1] z }| { 2 4 4 7 3 1 8 6 1 j 5-2 An incremental algorithm InsertionSort IncrementalAlg( array of.int.. A ) // We will write this as: int[ ] A compute solution for A // nothing to do: A[1..1] ist sorted for j = 2 to A.length do // compute solution for A[1..j] using soln. for A[1..j − 1] // here: insert A[ j] into the sorted array A[1..j − 1] key = A[ j ] A[ j ] A[1..j − 1] key = 3 z }| { 2 4 4 7 3 1 8 6 1 j 5-2 An incremental algorithm InsertionSort IncrementalAlg( array of.int.. A ) // We will write this as: int[ ] A compute solution for A // nothing to do: A[1..1] ist sorted for j = 2 to A.length do // compute solution for A[1..j] using soln. for A[1..j − 1] // here: insert A[ j] into the sorted array A[1..j − 1] key = A[ j ] i =j −1 A[ j ] A[1..j − 1] key = 3 z }| { 2 4 4 7 3 1 8 6 1 i j 5-2 An incremental algorithm InsertionSort IncrementalAlg( array of.int.. A ) // We will write this as: int[ ] A compute solution for A // nothing to do: A[1..1] ist sorted for j = 2 to A.length do // compute solution for A[1..j] using soln. for A[1..j − 1] // here: insert A[ j] into the sorted array A[1..j − 1] key = A[ j ] i =j −1 while i > 0 and A[i ] > key do A[i + 1] = A[i ] A[ j ] i =i −1 A[1..j − 1] key = 3 z }| { 2 4 4 7 3 1 8 6 1 i j 5-3 An incremental algorithm InsertionSort IncrementalAlg( array of.int.. A ) // We will write this as: int[ ] A compute solution for A // nothing to do: A[1..1] ist sorted for j = 2 to A.length do // compute solution for A[1..j] using soln. for A[1..j − 1] // here: insert A[ j] into the sorted array A[1..j − 1] key = A[ j ] i =j −1 while i > 0 and A[i ] > key do A[i do Ho + we 1] = A[ithe move ] entries A[ j ] larger i = i than − 1 key to the right? A[1..j − 1] key = 3 z }| { 2 4 4 7 3 1 8 6 1 i j 5-3 An incremental algorithm InsertionSort IncrementalAlg( array of.int.. A ) // We will write this as: int[ ] A compute solution for A // nothing to do: A[1..1] ist sorted for j = 2 to A.length do // compute solution for A[1..j] using soln. for A[1..j − 1] // here: insert A[ j] into the sorted array A[1..j − 1] key = A[ j ] i =j −1 while i > 0 and A[i ] > key do A[i + 1] = A[i ] A[ j ] i =i −1 A[1..j − 1] key = 3 z }| { 2 4 4 7 3 1 8 6 1 i j 5-3 An incremental algorithm InsertionSort IncrementalAlg( array of.int.. A ) // We will write this as: int[ ] A compute solution for A // nothing to do: A[1..1] ist sorted for j = 2 to A.length do // compute solution for A[1..j] using soln. for A[1..j − 1] // here: insert A[ j] into the sorted array A[1..j − 1] key = A[ j ] i =j −1 while i > 0 and A[i ] > key do A[i + 1] = A[i ] A[ j ] i =i −1 A[1..j − 1] key = 3 z }| { A[i + 1] = key 2 4 4 7 3 1 8 6 1 i j 6-1 Done? 6-2 Done? Not quite yet... Today (and for the remainder of the semester) we are interested in the following central questions: 6-3 Done? Not quite yet... Today (and for the remainder of the semester) we are interested in the following central questions: Is the algorithm correct? 6-4 Done? Not quite yet... Today (and for the remainder of the semester) we are interested in the following central questions: Is the algorithm correct? What is the run time of the algorithm? 6-5 Done? Not quite yet... Today (and for the remainder of the semester) we are interested in the following central questions: Is the algorithm correct? What is the run time of the algorithm? How much space does the algorithm need? 6-6 Done? Not quite yet... Today (and for the remainder of the semester) we are interested in the following central questions: Is the algorithm correct? What is the run time of the algorithm? How much space does the algorithm need? 7-1 Proving correctness InsertionSort(int[ ] A) for j = 2 to A.length do key = A[j ] i =j −1 while i > 0 and A[i ] > key do A[i + 1] = A[i ] i =i −1 A[i + 1] = key 7-2 Proving correctness InsertionSort(int[ ] A) for j = 2 to A.length do key = A[j ] i =j −1 while i > 0 and A[i ] > key do A[i + 1] = A[i ] i =i −1 A[i + 1] = key Idea of the loop invariant: 7-3 Proving correctness InsertionSort(int[ ] A) for j = 2 to A.length do key = A[j ] i =j −1 while i > 0 and A[i ] > key do A[i + 1] = A[i ] i =i −1 A[i + 1] = key Idea of the loop invariant: Where? What? 7-4 Proving correctness InsertionSort(int[ ] A) for j = 2 to A.length do key = A[j ] i =j −1 while i > 0 and A[i ] > key do A[i + 1] = A[i ] i =i −1 A[i + 1] = key Idea of the loop invariant: Where? at the beginning of every iteration of the for-loop... What? 7-5 Proving correctness InsertionSort(int[ ] A) for j = 2 to A.length do key = A[j ] i =j −1 while i > 0 and A[i ] > key do A[i + 1] = A[i ] i =i −1 A[i + 1] = key Idea of the loop invariant: Where? at the beginning of every iteration of the for-loop... What? 7-6 Proving correctness InsertionSort(int[ ] A) for j = 2 to A.length do key = A[j ] i =j −1 while i > 0 and A[i ] > key do A[i + 1] = A[i ] i =i −1 A[i + 1] = key Idea of the loop invariant: Where? at the beginning of every iteration of the for-loop... What? 7-7 Proving correctness InsertionSort(int[ ] A) for j = 2 to A.length do key = A[j ] i =j −1 while i > 0 and A[i ] > key do A[i + 1] = A[i ] i =i −1 A[i + 1] = key Idea of the loop invariant: Where? at the beginning of every iteration of the for-loop... What? WANTED: conditions that a) are always satisfied at this point, and b) give the correctness after loop termination 7-8 Proving correctness InsertionSort(int[ ] A) Here, A[1..j − 1] contains for j = 2 to A.length do key = A[j ] i =j −1 while i > 0 and A[i ] > key do A[i + 1] = A[i ] i =i −1 A[i + 1] = key Idea of the loop invariant: Where? at the beginning of every iteration of the for-loop... What? WANTED: conditions that a) are always satisfied at this point, and b) give the correctness after loop termination 7-9 Proving correctness InsertionSort(int[ ] A) Here, A[1..j − 1] contains for j = 2 to A.length do the same elements as in the key = A[j ] beginning of the algorithm— i =j −1 while i > 0 and A[i ] > key do but sorted. A[i + 1] = A[i ] i =i −1 A[i + 1] = key Idea of the loop invariant: Where? at the beginning of every iteration of the for-loop... What? WANTED: conditions that a) are always satisfied at this point, and b) give the correctness after loop termination 7-1 Proving correctness InsertionSort(int[ ] A) Here, A[1..j − 1] contains for j = 2 to A.length do the same elements as in the key = A[j ] beginning of the algorithm— i =j −1 while i > 0 and A[i ] > key do but sorted. A[i + 1] = A[i ] i =i −1 loop invariant A[i + 1] = key Proof by template“: we only need three more ingredients... ” 7-1 Proving correctness InsertionSort(int[ ] A) Here, A[1..j − 1] contains for j = 2 to A.length do the same elements as in the key = A[j ] beginning of the algorithm— i =j −1 while i > 0 and A[i ] > key do but sorted. A[i + 1] = A[i ] i =i −1 loop invariant A[i + 1] = key Proof by template“: we only need three more ingredients... ” 1.) Initialisation 7-1 Proving correctness InsertionSort(int[ ] A) Here, A[1..j − 1] contains for j = 2 to A.length do the same elements as in the key = A[j ] beginning of the algorithm— i =j −1 while i > 0 and A[i ] > key do but sorted. A[i + 1] = A[i ] i =i −1 loop invariant A[i + 1] = key Proof by template“: we only need three more ingredients... ” 1.) Initialisation Show: The invariant is satisfied at the first loop iteration. 7-1 Proving correctness InsertionSort(int[ ] A) Here, A[1..j − 1] contains for j = 2 to A.length do the same elements as in the key = A[j ] beginning of the algorithm— i =j −1 while i > 0 and A[i ] > key do but sorted. A[i + 1] = A[i ] i =i −1 loop invariant A[i + 1] = key Proof by template“: we only need three more ingredients... ” 1.) Initialisation Show: The invariant is satisfied at the first loop iteration. Here: 7-1 Proving correctness InsertionSort(int[ ] A) Here, A[1..j − 1] contains for j = 2 to A.length do the same elements as in the key = A[j ] beginning of the algorithm— i =j −1 while i > 0 and A[i ] > key do but sorted. A[i + 1] = A[i ] i =i −1 loop invariant A[i + 1] = key Proof by template“: we only need three more ingredients... ” 1.) Initialisation Show: The invariant is satisfied at the first loop iteration. Here: clear, because for j = 2 it holds that: A[1..j − 1] = A[1..1] is unchanged and sorted“. ” 7-1 Proving correctness InsertionSort(int[ ] A) Here, A[1..j − 1] contains for j = 2 to A.length do the same elements as in the key = A[j ] beginning of the algorithm— i =j −1 while i > 0 and A[i ] > key do but sorted. A[i + 1] = A[i ] i =i −1 loop invariant A[i + 1] = key Proof by template“: we only need three more ingredients... ” 1.) Initialisation 7-1 Proving correctness InsertionSort(int[ ] A) Here, A[1..j − 1] contains for j = 2 to A.length do the same elements as in the key = A[j ] beginning of the algorithm— i =j −1 while i > 0 and A[i ] > key do but sorted. A[i + 1] = A[i ] i =i −1 loop invariant A[i + 1] = key Proof by template“: we only need three more ingredients... ” 1.) Initialisation 2.) Maintenance 7-1 Proving correctness InsertionSort(int[ ] A) Here, A[1..j − 1] contains for j = 2 to A.length do the same elements as in the key = A[j ] beginning of the algorithm— i =j −1 while i > 0 and A[i ] > key do but sorted. A[i + 1] = A[i ] i =i −1 loop invariant A[i + 1] = key Proof by template“: we only need three more ingredients... ” 1.) Initialisation 2.) Maintenance Show: If the invariant is satisfied before the j th iteration, then it is also satisfied before the j + 1st. 7-1 Proving correctness InsertionSort(int[ ] A) Here, A[1..j − 1] contains for j = 2 to A.length do the same elements as in the key = A[j ] beginning of the algorithm— i =j −1 while i > 0 and A[i ] > key do but sorted. A[i + 1] = A[i ] i =i −1 loop invariant A[i + 1] = key Proof by template“: we only need three more ingredients... ” 1.) Initialisation 2.) Maintenance Show: If the invariant is satisfied before the j th iteration, then it is also satisfied before the j + 1st. Here: 7-1 Proving correctness InsertionSort(int[ ] A) Here, A[1..j − 1] contains for j = 2 to A.length do the same elements as in the key = A[j ] beginning of the algorithm— i =j −1 while i > 0 and A[i ] > key do but sorted. A[i + 1] = A[i ] i =i −1 loop invariant A[i + 1] = key Proof by template“: we only need three more ingredients... ” 1.) Initialisation 2.) Maintenance Show: If the invariant is satisfied before the j th iteration, then it is also satisfied before the j + 1st. Here: actually, formulate and prove an invariant for the while-loop! 7-2 Proving correctness InsertionSort(int[ ] A) Here, A[1..j − 1] contains for j = 2 to A.length do the same elements as in the key = A[j ] beginning of the algorithm— i =j −1 while i > 0 and A[i ] > key do but sorted. A[i + 1] = A[i ] i =i −1 loop invariant A[i + 1] = key Proof by template“: we only need three more ingredients... ” 1.) Initialisation 2.) Maintenance Show: If the invariant is satisfied before the j th iteration, then it is also satisfied before the j + 1st. Here: Observation: elements are moved to the right as long as necessary. Thus, key is inserted correctly. 7-2 Proving correctness InsertionSort(int[ ] A) Here, A[1..j − 1] contains for j = 2 to A.length do the same elements as in the key = A[j ] beginning of the algorithm— i =j −1 while i > 0 and A[i ] > key do but sorted. A[i + 1] = A[i ] i =i −1 loop invariant A[i + 1] = key Proof by template“: we only need three more ingredients... ” 1.) Initialisation 2.) Maintenance Show: If the invariant is satisfied before the j th iteration, then it is also satisfied before the j + 1st. Here: Observation: elements are moved to the right as long as necessary. Thus, key is inserted correctly. 7-2 Proving correctness InsertionSort(int[ ] A) Here, A[1..j − 1] contains for j = 2 to A.length do the same elements as in the key = A[j ] beginning of the algorithm— i =j −1 while i > 0 and A[i ] > key do but sorted. A[i + 1] = A[i ] i =i −1 loop invariant A[i + 1] = key Proof by template“: we only need three more ingredients... ” 1.) Initialisation 2.) Maintenance 7-2 Proving correctness InsertionSort(int[ ] A) Here, A[1..j − 1] contains for j = 2 to A.length do the same elements as in the key = A[j ] beginning of the algorithm— i =j −1 while i > 0 and A[i ] > key do but sorted. A[i + 1] = A[i ] i =i −1 loop invariant A[i + 1] = key Proof by template“: we only need three more ingredients... ” 1.) Initialisation 2.) Maintenance 3.) Termination 7-2 Proving correctness InsertionSort(int[ ] A) Here, A[1..j − 1] contains for j = 2 to A.length do the same elements as in the key = A[j ] beginning of the algorithm— i =j −1 while i > 0 and A[i ] > key do but sorted. A[i + 1] = A[i ] i =i −1 loop invariant A[i + 1] = key Proof by template“: we only need three more ingredients... ” 1.) Initialisation 2.) Maintenance 3.) Termination Show: Together, the invariant and the violation of the loop condition imply correctness. 7-2 Proving correctness InsertionSort(int[ ] A) Here, A[1..j − 1] contains for j = 2 to A.length do the same elements as in the key = A[j ] beginning of the algorithm— i =j −1 while i > 0 and A[i ] > key do but sorted. A[i + 1] = A[i ] i =i −1 loop invariant A[i + 1] = key Proof by template“: we only need three more ingredients... ” 1.) Initialisation 2.) Maintenance 3.) Termination Show: Together, the invariant and the violation of the loop condition imply correctness. Here: 7-2 Proving correctness InsertionSort(int[ ] A) Here, A[1..j − 1] contains for j = 2 to A.length do the same elements as in the key = A[j ] beginning of the algorithm— i =j −1 while i > 0 and A[i ] > key do but sorted. A[i + 1] = A[i ] i =i −1 loop invariant A[i + 1] = key Proof by template“: we only need three more ingredients... ” 1.) Initialisation 2.) Maintenance 3.) Termination Show: Together, the invariant and the violation of the loop condition imply correctness. Here: The violated loop condition is j > A.length. 7-2 Proving correctness InsertionSort(int[ ] A) Here, A[1..j − 1] contains for j = 2 to A.length do the same elements as in the key = A[j ] beginning of the algorithm— i =j −1 while i > 0 and A[i ] > key do but sorted. A[i + 1] = A[i ] i =i −1 loop invariant A[i + 1] = key Proof by template“: we only need three more ingredients... ” 1.) Initialisation 2.) Maintenance 3.) Termination Show: Together, the invariant and the violation of the loop condition imply correctness. Here: The violated loop condition is j > A.length. ⇒ j = A.length + 1 7-2 Proving correctness InsertionSort(int[ ] A) Here, A[1..j − 1] contains for j = 2 to A.length do the same elements as in the key = A[j ] beginning of the algorithm— i =j −1 while i > 0 and A[i ] > key do but sorted. A[i + 1] = A[i ] i =i −1 loop invariant A[i + 1] = key Proof by template“: we only need three more ingredients... ” 1.) Initialisation 2.) Maintenance 3.) Termination Show: Together, the invariant and the violation of the loop condition imply correctness. Here: The violated loop condition is j > A.length. ⇒ j = A.length + 1 ⇒ put into invariant 7-2 Proving correctness InsertionSort(int[ ] A) Here, A[1..j − 1] contains for j = 2 to A.length do the same elements as in the key = A[j ] beginning of the algorithm— i =j −1 while i > 0 and A[i ] > key do but sorted. A[i + 1] = A[i ] i =i −1 loop invariant A[i + 1] = key Proof by template“: we only need three more ingredients... ” 1.) Initialisation 2.) Maintenance 3.) Termination Show: Together, the invariant and the violation of the loop condition imply correctness. Here: The violated loop condition is j > A.length. ⇒ j = A.length + 1 ⇒ put into invariant ⇒ correct! 7-3 Proving correctness InsertionSort(int[ ] A) Here, A[1..j − 1] contains for j = 2 to A.length do the same elements as in the key = A[j ] beginning of the algorithm— i =j −1 while i > 0 and A[i ] > key do but sorted. A[i + 1] = A[i ] i =i −1 loop invariant A[i + 1] = key Proof by template“: we only need three more ingredients... ” 1.) Initialisation 2.) Maintenance 3.) Termination Show: Together, the invariant and the violation of the loop condition imply correctness. Here: The violated loop condition is j > A.length. ⇒ j = A.length + 1 ⇒ put into invariant ⇒ correct! 7-3 Proving correctness InsertionSort(int[ ] A) Here, A[1..j − 1] contains for j = 2 to A.length do the same elements as in the key = A[j ] beginning of the algorithm— i =j −1 while i > 0 and A[i ] > key do but sorted. A[i + 1] = A[i ] i =i −1 loop invariant A[i + 1] = key Proof by template“: we only need three more ingredients... ” 1.) Initialisation 2.) Maintenance 3.) Termination 8-1 Another example: factorial calculation Factorial(int k ) if k < 0 then error(... ) f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 8-2 Another example: factorial calculation Factorial(int k ) if k < 0 then error(... ) f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 8-3 Another example: factorial calculation Factorial(int k ) Correct? if k < 0 then error(... ) f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 8-4 Another example: factorial calculation Factorial(int k ) Correct? if k < 0 then error(... ) What happens if the loop does not f =1 get executed? j =2 while j ≤ k do f =f ·j j =j +1 return f 8-5 Another example: factorial calculation Factorial(int k ) Correct? if k < 0 then error(... ) What happens if the loop does not f =1 get executed? j =2 while j ≤ k do Then it holds j > k. As j = 2 ⇒ f =f ·j j =j +1 return f 8-6 Another example: factorial calculation Factorial(int k ) Correct? if k < 0 then error(... ) What happens if the loop does not f =1 get executed? j =2 while j ≤ k do Then it holds j > k. As j = 2 ⇒ f =f ·j k = 0 or k = 1. So k ! = 1. j =j +1 return f 8-7 Another example: factorial calculation Factorial(int k ) Correct? if k < 0 then error(... ) What happens if the loop does not f =1 get executed? j =2 while j ≤ k do Then it holds j > k. As j = 2 ⇒ f =f ·j k = 0 or k = 1. So k ! = 1. j =j +1 return f 8-8 Another example: factorial calculation Factorial(int k ) Correct? if k < 0 then error(... ) What happens if the loop does not f =1 get executed? j =2 while j ≤ k do Then it holds j > k. As j = 2 ⇒ f =f ·j k = 0 or k = 1. So k ! = 1. j =j +1 Return value is f = 1. return f 8-9 Another example: factorial calculation Factorial(int k ) Correct? if k < 0 then error(... ) What happens if the loop does not f =1 get executed? j =2 while j ≤ k do Then it holds j > k. As j = 2 ⇒ f =f ·j k = 0 or k = 1. So k ! = 1. j =j +1 Return value is f = 1. ⇒ correct. return f 8-1 Another example: factorial calculation Factorial(int k ) loop invariant: if k < 0 then error(... ) f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 8-1 Another example: factorial calculation Factorial(int k ) loop invariant: if k < 0 then error(... ) f = (j − 1)! f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 8-1 Another example: factorial calculation Factorial(int k ) loop invariant: if k < 0 then error(... ) f = (j − 1)! f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 1.) Initialisation 8-1 Another example: factorial calculation Factorial(int k ) loop invariant: if k < 0 then error(... ) f = (j − 1)! f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 1.) Initialisation Show: The invariant is satisfied at the first loop iteration. Here: 8-1 Another example: factorial calculation Factorial(int k ) loop invariant: if k < 0 then error(... ) f = (j − 1)! f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 1.) Initialisation Show: The invariant is satisfied at the first loop iteration. Here: Clear, as for j = 2 it holds: f = (2 − 1)! = 1! = 1 8-1 Another example: factorial calculation Factorial(int k ) loop invariant: if k < 0 then error(... ) f = (j − 1)! f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 1.) Initialisation Show: The invariant is satisfied at the first loop iteration. Here: Clear, as for j = 2 it holds: f = (2 − 1)! = 1! = 1 8-1 Another example: factorial calculation Factorial(int k ) loop invariant: if k < 0 then error(... ) f = (j − 1)! f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 1.) Initialisation 2.) Maintenance 8-1 Another example: factorial calculation Factorial(int k ) loop invariant: if k < 0 then error(... ) f = (j − 1)! f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 1.) Initialisation 2.) Maintenance Show: If the invariant is satisfied before the j th iteration then it is also satisfied before the j + 1st. Here: 8-1 Another example: factorial calculation Factorial(int k ) loop invariant: if k < 0 then error(... ) f = (j − 1)! f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 1.) Initialisation 2.) Maintenance Show: If the invariant is satisfied before the j th iteration then it is also satisfied before the j + 1st. Here: Before the j th iteration it holds INV, i.e. f = (j − 1)! 8-1 Another example: factorial calculation Factorial(int k ) loop invariant: if k < 0 then error(... ) f = (j − 1)! f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 1.) Initialisation 2.) Maintenance Show: If the invariant is satisfied before the j th iteration then it is also satisfied before the j + 1st. Here: Before the j th iteration it holds INV, i.e. f = (j − 1)! Then f is multiplied with j ⇒ 8-2 Another example: factorial calculation Factorial(int k ) loop invariant: if k < 0 then error(... ) f = (j − 1)! f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 1.) Initialisation 2.) Maintenance Show: If the invariant is satisfied before the j th iteration then it is also satisfied before the j + 1st. Here: Before the j th iteration it holds INV, i.e. f = (j − 1)! Then f is multiplied with j ⇒ f = j! 8-2 Another example: factorial calculation Factorial(int k ) loop invariant: if k < 0 then error(... ) f = (j − 1)! f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 1.) Initialisation 2.) Maintenance Show: If the invariant is satisfied before the j th iteration then it is also satisfied before the j + 1st. Here: Before the j th iteration it holds INV, i.e. f = (j − 1)! Then f is multiplied with j ⇒ f = j! Then j is incremented by 1 ⇒ 8-2 Another example: factorial calculation Factorial(int k ) loop invariant: if k < 0 then error(... ) f = (j − 1)! f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 1.) Initialisation 2.) Maintenance Show: If the invariant is satisfied before the j th iteration then it is also satisfied before the j + 1st. Here: Before the j th iteration it holds INV, i.e. f = (j − 1)! Then f is multiplied with j ⇒ f = j! Then j is incremented by 1 ⇒f = (j − 1)! 8-2 Another example: factorial calculation Factorial(int k ) loop invariant: if k < 0 then error(... ) f = (j − 1)! f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 1.) Initialisation 2.) Maintenance Show: If the invariant is satisfied before the j th iteration then it is also satisfied before the j + 1st. Here: Before the j th iteration it holds INV, i.e. f = (j − 1)! Then f is multiplied with j ⇒ f = j! Then j is incremented by 1 ⇒f = (j − 1)! ⇒ INV 8-2 Another example: factorial calculation Factorial(int k ) loop invariant: if k < 0 then error(... ) f = (j − 1)! f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 1.) Initialisation 2.) Maintenance Show: If the invariant is satisfied before the j th iteration then it is also satisfied before the j + 1st. Here: Before the j th iteration it holds INV, i.e. f = (j − 1)! Then f is multiplied with j ⇒ f = j! Then j is incremented by 1 ⇒f = (j − 1)! ⇒ INV 8-2 Another example: factorial calculation Factorial(int k ) loop invariant: if k < 0 then error(... ) f = (j − 1)! f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 1.) Initialisation 2.) Maintenance 3.) Termination 8-2 Another example: factorial calculation Factorial(int k ) loop invariant: if k < 0 then error(... ) f = (j − 1)! f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 1.) Initialisation 2.) Maintenance 3.) Termination Show: Together the invariant and the violation of the loop condition imply correctness. Here: 8-2 Another example: factorial calculation Factorial(int k ) loop invariant: if k < 0 then error(... ) f = (j − 1)! f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 1.) Initialisation 2.) Maintenance 3.) Termination Show: Together the invariant and the violation of the loop condition imply correctness. Here: Violated loop condition: j > k 8-2 Another example: factorial calculation Factorial(int k ) loop invariant: if k < 0 then error(... ) f = (j − 1)! f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 1.) Initialisation 2.) Maintenance 3.) Termination Show: Together the invariant and the violation of the loop condition imply correctness. Here: Violated loop condition: j > k , thus j = k + 1. 8-2 Another example: factorial calculation Factorial(int k ) loop invariant: if k < 0 then error(... ) f = (j − 1)! f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 1.) Initialisation 2.) Maintenance 3.) Termination Show: Together the invariant and the violation of the loop condition imply correctness. Here: Violated loop condition: j > k , thus j = k + 1. Insertion of j = k + 1“ in INV gives ” 8-3 Another example: factorial calculation Factorial(int k ) loop invariant: if k < 0 then error(... ) f = (j − 1)! f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 1.) Initialisation 2.) Maintenance 3.) Termination Show: Together the invariant and the violation of the loop condition imply correctness. Here: Violated loop condition: j > k , thus j = k + 1. Insertion of j = k + 1“ in INV gives f = k ! ” 8-3 Another example: factorial calculation Factorial(int k ) loop invariant: if k < 0 then error(... ) f = (j − 1)! f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 1.) Initialisation 2.) Maintenance 3.) Termination Show: Together the invariant and the violation of the loop condition imply correctness. Here: Violated loop condition: j > k , thus j = k + 1. Insertion of j = k + 1“ in INV gives f = k ! ” 8-3 Another example: factorial calculation Factorial(int k ) loop invariant: if k < 0 then error(... ) f = (j − 1)! f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 1.) Initialisation 2.) Maintenance 3.) Termination 8-3 Another example: factorial calculation Factorial(int k ) loop invariant: if k < 0 then error(... ) f = (j − 1)! f =1 j =2 while j ≤ k do f =f ·j j =j +1 return f 1.) Initialisation 2.) Maintenance 3.) Termination Algorithm Factorial(int) terminates and gives the correct result. 9-1 Self test Program InsertionSort in Python! 9-2 Self test Program InsertionSort in Python! count the number of comparisons∗ (of data elements) for different inputs. 9-3 Self test Program InsertionSort in Python! count the number Read Chapter 1 and Appendix A of comparisons∗ (of data from the book by Cormen et al. elements) for different and do as many of the practice inputs. exercises as possible! 9-4 Self test Program InsertionSort in Python! count the number Read Chapter 1 and Appendix A of comparisons∗ (of data from the book by Cormen et al. elements) for different and do as many of the practice inputs. exercises as possible! Bring your question into the tutorials! 9-5 Self test Program InsertionSort in Python! count the number Read Chapter 1 and Appendix A of comparisons∗ (of data from the book by Cormen et al. elements) for different and do as many of the practice inputs. exercises as possible! Bring your question into the tutorials! Keep up with the course from the very beginning! 9-6 Self test Program InsertionSort in Python! count the number Read Chapter 1 and Appendix A of comparisons∗ (of data from the book by Cormen et al. elements) for different and do as many of the practice inputs. exercises as possible! Bring your question into the tutorials! Keep up with the course from the very beginning! Register for the lecture and the tutorials in both TUNE and the e-learning portal.
