Verified Subtyping with Traits and Mixins

TL;DR

This paper introduces a method for verifying subtyping relations in object-oriented programs with traits and mixins using separation logic, implemented in Scala, and applied to the Scala standard library.

Contribution

It presents a novel approach to check subtyping with traits and mixins, addressing limitations in existing languages like Scala.

Findings

Verified 67% of Scala mixins conform to subtyping.

Implemented a domain-specific language in Scala for subtyping verification.

Applied the method to real-world Scala standard library code.

Abstract

Traits allow decomposing programs into smaller parts and mixins are a form of composition that resemble multiple inheritance. Unfortunately, in the presence of traits, programming languages like Scala give up on subtyping relation between objects. In this paper, we present a method to check subtyping between objects based on entailment in separation logic. We implement our method as a domain specific language in Scala and apply it on the Scala standard library. We have verified that 67% of mixins used in the Scala standard library do indeed conform to subtyping between the traits that are used to build them.