[jhck]

You're right that the searching and sorting methods discussed are elementary, but note that the article is about how to prove the correctness of the methods (validity and termination); so it's not just the usual fare about binary search and insertion sort - the article's treatment of those methods actually builds on the transition system theory developed at the beginning. That said, this note is indeed used for CS 101 at Aarhus University - more specifically, it's used in the "Algorithms and Data Structures" course that first year CS students go through.

[dataflow]

Interesting. It's a really strange mix to me. They seem to start talking about safety and liveness properties, but only mention them a grand total of 4 times, and avoid mentioning anything related to them after page 17... in an 81-page book whose subject is ostensibly "Transition Systems", in big letters, which are neither algorithms nor data structures, but model of computation. Surely, if the goal is to talk about transition systems, there would be a LOT more that would be said about safety and liveness properties, and the logic surrounding them? They're generally introduced in graduate or advanced undergraduate courses teaching temporal logic. It's kind of bizarre to me to mention them so briefly and then move on so quickly (what would be the point of doing that in an introductory CS course?), but maybe it'll make sense if I actually read the book? Definitely seems like an unconventional approach on its face.

[qsort]

Sure, but I agree with parent's comment that it's a... weird turn?

When one introduces transition systems, I usually expect "yeah, now he's going to define a labeled transition system, then introduce modal logic, maybe temporal logic, definitely bisimulations, maybe Van Benthem".

Obviously one can do proofs of elementary algorithms with that formalism, it's just a bit unusual, that's all.

[rain1]

your literally named qsort why are you complaining

[NDizzle]

When it rains, it pours?!