More Efficient Property Types with SMT- Decidable Assertions

Property type systems extend static type systems by allowing users to refine types with logical predicates. Kukicha is a novel two-step method to implement property types in object-oriented programming languages by combining efficient type rules with the power of deductive verification. However, the Kukicha type rules so far are only capable of verifying a small subset of property types. Support for dependent types in particular is very limited and requires the use of deductive verification, taking away from the simpler type rules’ convenience. We introduce a new component to the Kukicha method that can automatically verify a subset of property types that are out of scope for the type rules but also don’t require the overhead of deductive verification. We formalise our extension within the theoretical framework of Kukicha and prove that it is sound. We further implement our extension in the Property Checker, the Kukicha implementation for Java, by leveraging SMT solving tools. Finally, we examine the impact of our work using a small case study.