# Algorithm Analysis and Design *(Week 2)*
Untuk membuktikan apakah sebuah algoritma benar, dapat menggunakan Counter Example (Indirect Proof), Induksi Matematika (Direct Proof), dan Loop Invariant

## Loop Invariant
- Small Definition: Semacam predikat yang selalu *true* untuk setiap loop. Merupakan tool untuk membuktikan bahwa sebuah algoritma itu **correct**

- Poin dimana loop invariant harus *true*:
1. **Initialization:** Invariant harus *true* sebelum iterasi pertama mulai.

**"Apakah *true* sebelum iterasi pertama dijalankan?"**
2. **Maintenance:** jika tepat sebelum iterasi *true*, maka sebelum iterasi berikutnya harus *true*

**"Asumsi *true* sebelum iterasi k-th. apakah *loop body* tetap *true* sebelum iterasi (k+1)-th?"**
3. **Termination:** Pada saat loop di *terminate*, Invarian memperlihatkan property khusus bahwa algoritma **correct**.

**"Asumsikan loop *terminate*. Apakah invarian memperlihatkan bahwa algoritma benar?"**

( although it can temporarily be false during the body of the loop )

*kita dapat membuat loop tanpa mengetahui loop invariant, namun dengan loop invariant maka akan memberitahu apakah algoritma tersebut benar atau tidak*

**Loop invariant tidak membuktikan bahwa loop terminate atau tidak**
- Formal Loop Invariant for Insertion sort Algorithm:
*"The subarray A[1...j-1] consists of elements originally in A[1...j-1] but in sorted order"*

> maybe this is not important but pay attention on **WHILE** loop.

### Tips untuk Bekerja dengan Loop Invariant
1. Gunakan Intuisimu bagaimana code tersebut berjalan
2. Dalam sebuah list, invariant biasanya menjelaskan sesuatu tentang "Bagian list yang telah di proses sejauh ini". Invarian untuk int biasanya relasi matematika atau *size bound*
3. Invarian tidak memiliki konsep waktu
4. Invarian tetap benar jika saat konsisi loop *false*
5. Dalam membuktikan, hanya gunakan invarian, loop condition (**true**), prekondisi, dan matematika. Dan Hal lain yang seharusnya menjadi bagian *loop invariant*

Source: [https://www.youtube.com/watch?v=AUs9mvIHoLg](https://www.youtube.com/watch?v=AUs9mvIHoLg)

### Binary Search

1 bsearch(type A[], type a) {
2 start = 1, end = length(A)
3
4   while ( start <= end ) {
5       mid = floor(start + end / 2)
6
7       if ( A[mid] == a ) return mid
8       if ( A[mid] > a ) end = mid - 1
9       if ( A[mid] < a ) start = mid + 1
10
11  }
12  return -1
13} 

Loop Invariant Sebagai Berikut:

a ∈ A[start..end]     (Ini penting sangat untuk memastikan kita approach ke jawaban)
end'-start' < end-start   (Ini penting sangat untuk memastikan batasnya mengecil)

- [Proving Binary Search using Loop Invariant](https://www.cs.cornell.edu/courses/cs2112/2015fa/lectures/lec_loopinv/)
Disini saya mencoba memahami cara membuktikan correctness algoritma binary search dengan loop invariant diatas. (hyperlink sumber diatas)
1. **Initialization:** A is sorted in Ascending order *true* dikarenakan syarat untuk method *Binary Search* adalah array yang Sorted. Sehingga juga `end'-start' < end-start` *true*. dan `a ∈ A[start..end]` karena merupakan prekondisi.
2. **Maintenance:**
- Pada saat `A[mid]>a` maka `end = mid - 1` dan Pada saat `A[mid]<a` maka `start = mid + 1`. kedua hal ini tidak mengubah isi dari Array sehingga A tetap Sorted
- Jika a terdapat pada 'A[start...end]' akan selalu memenuhi `end'-start' < end-start`.
3. **Termination:**
- Value dari end akan selalu non-negative serta jika start>end maka method akan terminate (jika a tidak di dalam A). Jika a di dalam A maka *eventually* `A[mid] == a` sehingga method akan terminate. A tetap sorted, a didalam A, dan `end'-start' < end-start`

## Running time for Binary Search

| Binary Search (type A[], type a) | Cost | Times |
|-------------------------------------|------|----------|
| start = 1, end = length(A) | c1 | 1 |
| while ( start <= end ) { | c2 | \\(\lfloor (\log{n}) \rfloor\\) |
| mid = floor(start + end / 2) | c3 | \\(\lfloor (\log{n}) \rfloor\\)|
| if ( A[mid] == a ) return mid | c4 | \\(\lfloor (\log{n}) \rfloor\\) |
| if ( A[mid] > a ) end = mid - 1 | c5 | \\(\lfloor (\log{n}) \rfloor\\) |
| if ( A[mid] < a ) start = mid + 1 } | c6 | \\(\lfloor (\log{n}) \rfloor\\) |
| return -1 | c7 | 1 |
| } | 0 | |

> Please jika ada kesalahan (Especially tentang running time) tolong kasi tau hehe~