Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

I can’t believe that I can prove that it can sort

blog.adacore.com

Post reply on HN
Print view View original

1–10 of 124 posts

Re: I can’t believe that I can prove that it can sort

#2

Post by MattPalmer1086 »

Interesting. It is a bit counter intuitive at first but not too hard to see how it works.

After the first main loop, the first item will be the biggest item in the list.

The inner loop, as it always starts from 1 again will gradually replace the bigger items with smaller items, and so on.

Re: I can’t believe that I can prove that it can sort

#3

Post by roenxi »

If 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 glance.

To sort: 4-3-6-9-1, next round pivot for the i loop in [].

    [4]-3-6-9-1
    9-[3]-4-6-1
    3-9-[4]-6-1
    3-4-9-[6]-1
    3-4-6-9-[1]

    1-2-3-6-9 & sorted
I can see that it sorts everything to the left of a pivot, then because it does that n times it comes to a sorted list. A reasonable proof will be more complicated than I thought.

Re: I can’t believe that I can prove that it can sort

#4

Post by blueflow »

roenxi wrote: post #3

If 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.

Re: I can’t believe that I can prove that it can sort

#7

Post by iib »

smusamashah wrote: post #5

Here is how it looks. https://xosh.org/VisualizingSorts/sorting.html#IYZwngdgxgBAZ... If you compare it with both Insertion and Bubble sort. You can see it looks more like insertion sort than bubble sort.

I guess it can be thought of as an unoptimized insertion or bubble sort.

I think it is very possible to write this algorithm by mistake in intro compsci classes when you try to code a bubble sort by heart. I would think TAs may have many such instances in their students' homework.

Re: I can’t believe that I can prove that it can sort

#9

Post by eatonphil »

This is a fantastic post! It's great to have a concrete example of proving a not-trivial algorithm. And somehow this Ada code feels more approachable to me than HOL4 and other functional proof assistants I've looked at.

While it's been on my list for a while, I'm more curious to try out Ada now.

Post reply on HN