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

121–124 of 124 posts

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

#121

Post by tonmoy »

School-Cotton wrote: post #68
tonmoy wrote: post #48

Earlier quoted context omitted.

Note that the equality sign is less than, but the algorithm sorts in a descending order.

Not true. Clojure code: (defn swap [items i j] (assoc items i (items j) j (items i))) (defn weirdsort [items] (let [ct (count items) indices (for [i (range ct) j (range ct)] [i j])] (reduce (fn [items [i j]] (let [ith (nth items i) jth (nth items j)] (if ( Then in the repl: my-namespace> (def items (shuffle (range 20))) #'my-namespace/items my-namespace> items [19 0 13 16 14 18 15 7 10 17 9 11 6 1 3 4 12 2 5 8] my-na…

Sorry I meant to write ascending. It is weird that it swaps when i < j, but the list ends up ascending

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

#122

Post by nephanth »

Article says it is better to actually read the paper instead of trying to figure it out.

I disagree on that. It is a good exercise to try to prove it by yourself and it was actually quite fun

Main mistakes author makes though

- trying to prove it works without first understanding why / how it works. Always simulate test-runs on paper / in your head before

- trying to prove on machine first. Always make sure you can do the proof on paper first. Then and only then should you battle with your verifier / solver to get it to understand your proof

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

#123

Post by petercooper »

carlsborg wrote: post #12

Vaguely remember seeing this in the first few chapters somewhere of Spirit of C by Mullish and Cooper.

Can confirm. It's on page 243, in the "Arrays" chapter, and is referred to as the "exchange sort." The actual code is:

    /* Sort the array
    for (i = 0; i  array[j]])
            {
                int temp = array[i];
                array[i] = array[j]:
                array[j] = temp;
            }
So that's from the late 80s.

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

#124

Post by Jtsummers »

petercooper wrote: post #123
carlsborg wrote: post #12

Vaguely remember seeing this in the first few chapters somewhere of Spirit of C by Mullish and Cooper.

Can confirm. It's on page 243, in the "Arrays" chapter, and is referred to as the "exchange sort." The actual code is: /* Sort the array for (i = 0; i array[j]]) { int temp = array[i]; array[i] = array[j]: array[j] = temp; } So that's from the late 80s.

That's not the same sort as in the article. Two key differences:

1. j in the article runs from 0 to array_size-1 (if done in C like this, in the article it's a 1-based array so 1 to array_size). This sort has j run from i+1 to array_size-1.

2. The swap condition is reversed. In the article's sort the swap happens when array[i] < array[j].

Post reply on HN