> I did math at university, but everyone in the sciences took one year of CS and the first semester was Algorithms & Data Structures. The course itself was not that remarkable (Gerth Brodal taught it and did a good job) but there was an excellent pre-course prep week. 1/2
> Everyone was straight from high school and weren't expected to know set theory or discrete logic, so it was mainly a primer on stuff like that, which I didn't really need. But one part of the prep week was this amazing booklet, which changed how I thought: https://cs.au.dk/~gerth/dADS1-12/daimi-fn64.pdf
> That was my introduction to Floyd-Hoare logic but in a general setting that applies to both programs and non-deterministic state transition systems. Totally rewired how I thought about programming forever.
If you want more theory, I recently stumbled across some great lecture materials [1] for a course on coalgebra, which is a category-theoretic way of modeling state-based systems, as well as familiar computer science concepts like (co)data types and (co)induction.
Looking at the table of contents, it's kind of jarring to see a discussion of transition systems followed by elementary topics like binary search, sorting, etc. I would've expected the book to start with labeled and unlabeled transition systems and then get into various forms of temporal logic, etc. Who is the target audience here? A CS 101 student, or a CS graduate student?
These notes is indeed used in "CS 101".
The note is meant to fill a need not covered by the main materials.
In this case the concept of transition systems is used throughout
the course for proofs. In a different note graph algorithms are
presented - and the the red thread is that all proods use transitions
systems.
In short: you need to look at the full course to see where a lecture note fits in.
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.
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.
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.
It is an odd mix, but I like that. High level formalisms with familiar
D&S 101 examples. Reminiscent of reading Knuth. It leans heavily
toward formalisms enabling proofs, but maybe skips philosophy of state
worth mentioning - state may not be enumerable. It can be implicit. It
can get duplicated with contradictory representations.
> I did math at university, but everyone in the sciences took one year of CS and the first semester was Algorithms & Data Structures. The course itself was not that remarkable (Gerth Brodal taught it and did a good job) but there was an excellent pre-course prep week. 1/2
> Everyone was straight from high school and weren't expected to know set theory or discrete logic, so it was mainly a primer on stuff like that, which I didn't really need. But one part of the prep week was this amazing booklet, which changed how I thought: https://cs.au.dk/~gerth/dADS1-12/daimi-fn64.pdf
> That was my introduction to Floyd-Hoare logic but in a general setting that applies to both programs and non-deterministic state transition systems. Totally rewired how I thought about programming forever.