Translating Scala to SIL
Bernhard F. Brodowsky · Repository for Publications and Research Data (ETH Zurich) · 2013
In this thesis, we describe a tool which is implemented as a Scala compiler plugin that translates a Scala program to a SIL program which is then passed to a verifier.We reused experience gained with Chalice [10] and reapplied it to Scala [12] to support features like classes, methods, pure functions, the whole Implicit Dynamic Frames [17] support and the type system.We also solved several problems that were not present in Chalice including the translation of non-pure Scala expressions to pure SIL expressions.Additionally, we found a new solution for the translation of Scala lazy vals which allows the verification of Scala programs which include lazy vals with some additional restrictions.i Contents 5.1.4The Cake Pattern . . . .