Verified Subtyping with Traits and Mixins
The concept of verified subtyping with traits and mixins in object-oriented design. Learn about Liskov Substitution Principle, behavior subtyping, and contributions of subtyping with traits and mixins in Scala. Understand the use of traits and mixins in creating fine-grained units of reusable code."
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Verified Subtyping with Traits and Mixins Asankhaya Sharma National University of Singapore
Object Oriented Design S Single Responsibility O Open Close L Liskov Substitution I Interface Segregation D Dependency Inversion First proposed by Robert C. Martin in comp.object newsgroup in March 1995 3/10/2025 FSFMA 2014 2
Liskov Substitution Principle Let q(x) be a property provable about objects x of type T. Then q(y) should be provable for objects y of type S where S is a subtype of T - Barbara Liskov and Jeannette Wing 3/10/2025 FSFMA 2014 3
Behavior Subtyping Useful to reason about design of class hierarchies Stronger notion than typical subtyping of functions defined in type theory Function subtyping is based on contravariance of argument types and covariance of the return type Behavioral subtyping is trivially undecidable If the property is this method always terminates 3/10/2025 FSFMA 2014 4
Contributions Subtyping with Traits and Mixins in Scala By checking entailments in separation logic Extend Scala with a domain specific language (SLEEK DSL) Allows Scala programmers to insert subtyping checks in their programs Case study on subtyping in Scala Standard Library Verified subtyping in 67% of Mixins 3/10/2025 FSFMA 2014 5
Traits and Mixins Traits Fine grained unit of reuse Similar to abstract classes but some methods can have implementations as well Mixin Composition (Mixin) A class which contains a combination of methods from other traits and classes Similar to multiple inheritance if the combination contains all methods of combined classes 3/10/2025 FSFMA 2014 6
Traits Example trait ICell { def get() : Int def set(x : Int) } trait BICell extends ICell { private var x : Int = 0 def get() { x } def set(x : Int) { this.x = x } } Similar to an Abstract Class Implementation of ICell 3/10/2025 FSFMA 2014 7
Traits Example (cont.) trait Double extends ICell { abstract override def set(x : Int) { super.set(2*x) } } trait Inc extends ICell { abstract override def set(x : Int) { super.set(x+1) } } 3/10/2025 FSFMA 2014 8
Mixins Example OddICell (odd values) class OddICell extends BICell with Inc with Double EvenICell (even values) class EvenICell extends BICell with Double with Inc OddICell Double Inc BICell Class Linearization EvenICell Inc Double BICell 3/10/2025 FSFMA 2014 9
Scala doesnt enforce Subtyping def m (c: BICell with Inc with Double) : Int { c.get } val oic = new OddICell val eic = new EvenICell m(oic) m(eic) by the type system Both calls are allowed Only object oic is subtype of c 3/10/2025 FSFMA 2014 10
Verified Subtyping A mixin can be represented as a separation logic predicate based on class linearization OddICell Double Inc BICell OddICell<this> == BICell<this,p> * Inc<p,q> * Double<q,null> EvenICell Inc Double BICell EvenICell<this> == BICell<this,p> * Double<p,q> * Inc<q,null> 3/10/2025 FSFMA 2014 11
From Subtyping to Entailment Subtyping can be reduced to checking entailment between the predicates m(oic) OddICell<oic> |- BICell<c,p> * Inc<p,q> * Double<q,null> Valid m(eic) EvenICell<eic> |- BICell<c,p> * Inc<p,q> * Double<q,null> Invalid 3/10/2025 FSFMA 2014 12
SLEEK DSL Implementation based on SLEEK An existing separation logic based entailment prover Supports user defined predicates and user specified lemmas With Shape, Size, and Bag properties 3/10/2025 FSFMA 2014 13
Implementation Overview sleek.lib SLEEK exe sleek.dsl sleek.inter Scala Scala Programs Interpreter 3/10/2025 FSFMA 2014 14
Scala with SLEEK DSL Insert checks in Scala programs to verify subtyping using SLEEK DSL def m (c: BICell with Inc with Double) : Int { c.get } val oic = new OddICell val eic = new EvenICell if (OddICell<oic> |- BICell<c,p> * Inc<p,q> * Double<q,null> ) m(oic) if (EvenICell<eic> |- BICell<c,p> * Inc<p,q> * Double<q,null>) m(eic) 3/10/2025 FSFMA 2014 15
Experiments Scala Standard Library Considered four class hierarchies Exceptions Maths Parser Combinators Collections 3/10/2025 FSFMA 2014 16
Results Class Hierarchy Mixins in the Hierarchy Mixins with Verified Subtyping Percentage Exceptions 11 11 100 Maths 5 4 80 Combinators 6 6 100 Collections 27 12 44 Total 49 33 67 Traits provide more flexibility, 33% of Mixins use Traits in a way that does not conform to subytping 3/10/2025 FSFMA 2014 17
Conclusions We use entailment proving in separation logic to check subtyping with Traits and Mixins A domain specific language based on SLEEK to check entailments from Scala programs Case study based on Scala Standard Library 3/10/2025 FSFMA 2014 18
Perspectives Lays the foundation for verifying OO Scala programs Specification reuse with traits and mixins Inheritance verification Static and Dynamic Specifications for traits and mixins Avoid re-verification Compositional and modular 3/10/2025 FSFMA 2014 19
Thank You ! Questions ? Scala with SLEEK DSL Web Tool, Source Code and Sample Programs http://loris- 7.ddns.comp.nus.edu.sg/~project/SLEEKDSL/ Contact asankhaya@nus.edu.sg 3/10/2025 FSFMA 2014 20
