University:
Amherst College
Course:
COSC 311 | Algorithms
Academic year:

2022
Views:

157

Pages:

2
Author:

Farneamvi

Proving Correctness with Invariants Today in class we talked about how to prove that our insertion sort algorithm is correct using invariants. This document provides a formally written proof of the reasoning we discussed, including the inner while loop. Loop-1 1. Initialization. By the precondition, to_sort contains a multiset of ints. None of the code between the precondition and the first loop-1 iteration touches to_sort, so to_sort contains all of the original data at the start of the first iteration, satisfying invariant (1). Just before the start of the loop, we set i=1, so subarray to_sort[0...i-1] consists of just element 0 (i.e., a single element), so it must be sorted, satisfying invariant (2). 2. Maintenance. We want to show that if our invariant is true and the loop condition (i.e, i=to_sort[j], then (a) all data in subarray to_sort[j+2...i] is greater than val (by invariant 3), (b) all data in subarray to_sort[0...j] is smaller than val (by the fact that val>=to_sort[j]), and (c) the data in each of subarrays to_sort[0...j] and to_sort[j+2...i] is sorted (by invariant 2). Hence after inserting val into position j+1, the whole subarray to_sort[0...i] is sorted. 2

Description

Related Documents

Free up your schedule!

Take 5 seconds to unlock