Verified Subtyping with Traits and Mixins
Programming Languages
2014-07-16 v1 Logic in Computer Science
Software Engineering
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.
Cite
@article{arxiv.1407.3892,
title = {Verified Subtyping with Traits and Mixins},
author = {Asankhaya Sharma},
journal= {arXiv preprint arXiv:1407.3892},
year = {2014}
}
Comments
In Proceedings FSFMA 2014, arXiv:1407.1952