Predicate subtyping in VerCors

VerCors is a program verifier that can verify specifications for programs written in Java, C and PVL (VerCors own language with built-in support for VerCors specifications). These specifications are expressed through pre-conditions and post-conditions similar to JML (Java Modeling Language) annotations. Many Java and C programs use bounded integers, rather than mathematical integers. Meanwhile, VerCors can only reason about all integer-based types as mathematical integers. As such, VerCors cannot verify a program for the absence of integer overflows. Bounded integers can be seen as subtypes of integers. Predicate subtyping is a subtyping system in which a subtype gets constructed with a type and predicates on a term of said type. The terms of the constructed subtype are all terms of the original type for which all predicates hold. We have added predicate-based subtyping to VerCors as a more general solution to supporting bounded integers. In this thesis we will first show how to manually translate examples of the proposed subtyping system into the corresponding specification in a program. We will also establish supporting mathematical theory describing the relations between predicate subtypes.