Nearly All Binary Searches and Mergesorts are Broken

A paper from POPL that we are reading in John's Research group refers to this blog post: Official Google Research Blog: Extra, Extra - Read All About It: Nearly All Binary Searches and Mergesorts are Broken. Scary and funny at the same time.

The problem occurs with int mid =(low + high) / 2; and statements like it. If low and high are integers, then there is not a problem. Since they are int typed instead, there is a possibility for overflow. An easy solution is to add in a subtraction or do some fancy shifting (see the original Google blog).

John mentions this type of thing a lot. It seems that a lot of formal methods people make assumptions about an int acting like an integer. Software engineers, on the other hand, are painfully aware that the problems normally come because int types do NOT act like integers. This is why there are some many complicated transfer functions in cXprop. The paper we are reading is Types, Bytes and Separation Logic by Harvey Tuch, Gerwin Klein, and Michael Norrish.