A Computer-Assisted Proof of the Bellman-Ford Lemma
Peter H. Schmitt · Repository KITopen (Karlsruhe Institute of Technology) · 2011
These notes serve (at least) two purposes. First, they document a proof done with the KeY system of a purely mathematical statement, Lemma 1 below, within the context of Dijkstra’s Shortest Path Algorithm. This is an unusual application of the KeY system that is designed to verify Java programs. The verification of a Java implementation of Dijkstra’s algorithm itself is the topic of the Diploma thesis [10]. Secondly, we use this simple proof exercise to review the widely practiced method to handle partial functions via underspecification that is also used in the KeY system. Little can be found in the literature on the theoretical foundations of this approach. This report proposes a first step towards a theory of underspecification. Particular emphasis is devoted to the axiomatisation of abstract data types with partial functions. As a side issue we also include some comments on conservative extensions.