Combsort is far more elegant and faster
algorithm. I've wrote a type-generic combsort
a while ago here:
https://github.com/FrozenVoid/combsort.h
(Combsort as well as mentioned algorithm also consists of two loops and a swap)
I can’t believe that I can prove that it can sort
11–20 of 124 posts
Re: I can’t believe that I can prove that it can sort
#12Vaguely remember seeing this in the first few chapters somewhere of Spirit of C by Mullish and Cooper.
Re: I can’t believe that I can prove that it can sort
#13I actually used this algorithm a decade ago to implement a log-based, transactional database system for an embedded system with very low amount of memory and requirement that all memory be statically allocated.
To the frustration of the rest of the development team who first called me an idiot (I was new) then they could not make quicksort run as fast on inputs that were capped at something like 500 items. Apparently, algorithmic complexity isn't everything.
Re: I can’t believe that I can prove that it can sort
#14If it looks "obviously wrong" the quick proof that it works ... the j loop will move the largest unsorted element in the array into a sorted position. Since the i loop executes the j loop n times, the array must be sorted (since the n largest elements will be in the correct order). EDIT ^W^W^W Nope, I'm wrong. I did a worked example on paper. I think the devious thing here is the algorithm looks simple at a lazy glan…
This somewhat looks like bubble-sort minus the early exit.
It is just quirky insert-sort. In each outer cycle, it inserts value originally from the A[i] position to already sorted sequence A[1]..A[i-1], while using A[i] as a temporary variable to shift higher part of the sorted sequence one position up.
Re: I can’t believe that I can prove that it can sort
#15[deleted]
Re: I can’t believe that I can prove that it can sort
#16I actually used this algorithm a decade ago to implement a log-based, transactional database system for an embedded system with very low amount of memory and requirement that all memory be statically allocated. To the frustration of the rest of the development team who first called me an idiot (I was new) then they could not make quicksort run as fast on inputs that were capped at something like 500 items. Apparently…
If I understand correctly, you would just run the n+1 th outer loop to insert the new item each time?
Re: I can’t believe that I can prove that it can sort
#17So, Lionel knew how to implement a 3D Renderer, but had no clue about O(n) complexity neither other sorting algorithms?
I am buffled
Re: I can’t believe that I can prove that it can sort
#18I actually used this algorithm a decade ago to implement a log-based, transactional database system for an embedded system with very low amount of memory and requirement that all memory be statically allocated. To the frustration of the rest of the development team who first called me an idiot (I was new) then they could not make quicksort run as fast on inputs that were capped at something like 500 items. Apparently…
If I understand correctly, you would just run the n+1 th outer loop to insert the new item each time?
[deleted]
Re: I can’t believe that I can prove that it can sort
#19The comments so far have tended to focus on the proof itself, but for me the coolest part of the blog post were the formal methods.
Does anyone here also use SPARK for this sort of thing? Are there other formal methods tools you'd use if you had to prove something like this?
Re: I can’t believe that I can prove that it can sort
#20After each outer loop iteration, A[:i] (the array up to i) is in ascending order with the max of A at A[i].
This is true the first iteration since max(A) is eventually swapped to A[1]. This is true in subsequent iterations since during the ith iteration, it inserts the next element, initially at A[i], into A[:i-1] and shift everything up with swaps with A[i] so A[:i] is sorted, with the max of A moved to A[i]. After that no more swaps happen in the ith iteration since A[i] contains the max of A.