Shankar, N. (2010). Fixpoints and Search in PVS. In: Müller, P. (eds) Advanced Lectures on Software Engineering. LASER LASER 2007 2008. Lecture Notes in Computer Science, vol 6029. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13010-6_5
Abstract
The Knaster–Tarski theorem asserts the existence of least and greatest fixpoints for any monotonic function on a complete lattice. More strongly, it asserts the existence of a complete lattice of such fixpoints. This fundamental theorem has a fairly straightforward proof. We use a mechanically checked proof of the Knaster–Tarski theorem to illustrate several features of the Prototype Verification System (PVS). We specialize the theorem to the power set lattice, and apply the latter to the verification of a general forward search algorithm and a generalization of Dijkstra’s shortest path algorithm. We use these examples to argue that the verification of even simple, widely used algorithms can depend on a fair amount of background theory, human insight, and sophisticated mechanical support.
Keywords: Monotone Operator, Complete Lattice, Proof Obligation, Boolean Lattice, Typing Judgement