The geometry of conservative programs

The programs, we consider are written in a restricted form of the language introduced by Dijkstra (1968). A program is said to be conservative when each of its loops restores all the resources it consumes. We define the geometric model of such a program and prove that the collection of directed paths on it is a reasonable over-approximation of its set of execution traces. In particular, two directed paths that are close enough with respect to the uniform distance result in the same action on the memory states of the system. The same holds for weakly dihomotopic directed paths. As a by-product, we obtain a notion of independence, which is favourably compared to more common ones. The geometric models actually belong to a handy class of local pospaces whose elements are called isothetic regions. The local pospaces we use differ from the original ones, we carefully explain why the alternative notion should be preferred. The title intentionally echoes the article by Carson and Reynolds (1987).