Verified Subtyping with Traits and Mixins
This addresses a verification challenge for Scala developers, offering a domain-specific solution to ensure type safety in trait-based compositions.
The paper tackles the problem of subtyping verification for objects composed with traits and mixins in Scala, presenting a method based on separation logic entailment and verifying that 67% of mixins in the Scala standard library conform to subtyping.
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.