KeY-Hoare

Abstract

In contrast to the other book chapters that focus on verification of real-world Java program, here we introduce a program logic and a tool based on KeY that has been designed solely for teaching purposes (see the discussion in Section 1.3.3). It is targeted towards B.Sc. students who get in contact with formal program verification for the first time. Hence, we focus on program verification itself, while treating first-order reasoning as a black box. We aimed to keep this chapter self-contained so that it can be given to students as reading material without requiring them to read other chapters in this book. Even though most of the concepts discussed here are identical to or simplified versions of those used by the KeY system for Java, there are subtle differences such as the representation of arrays, which we point out when appropriate.