Permission-Based Verifcation of Subclassing and Traits
Andreas BÃ ⁄ hlmann · Repository for Publications and Research Data (ETH Zurich) · 2013
Despite the fact that object-oriented languages are well established in general, it is still a challenging task to support subtyping and inheritance in automated program verifiers, especially in the context of permission logics.The same applies even more to traits, which are a means for fine-grained code reuse promoted by programming languages such as Scala.Traits have only recently gained attention in the automated program verification community and are not yet supported in an automated program verifier.In this thesis we adapt the concept of abstract predicate families developed by Parkinson and Bierman in the context of separation logic to the context of implicit dynamic frames.Based on this, we develop an algorithm for the automated verification of Chalice programs.Chalice is a Microsoft Research language based on implicit dynamic frames that is object-based, supports fork-join concurrency, monitors, fractional permissions, abstract predicates, pure functions and has been extended, as part of this work, with support for subtyping and inheritance.We have implemented and tested the developed algorithm in the automated program verifier Syxc based on symbolic execution.In line with the long-term goal of Syxc to verify Scala programs, we extend our algorithm in order to verify traits.We show in particular how to verify traits in the presence of late-bound super calls, which are similar to dynamically dispatched calls.