University of Twente Student Theses


Permission-based separation logic for Scala

Leur, C. de (2015) Permission-based separation logic for Scala.

[img] PDF
Abstract:Scala is a versatile multi-paradigm general purpose programming language on the Java Virtual Machine, which offers full compatibility with existing Java libraries and code, while providing a multitude of advanced features compared to Java itself. Permission-based separation logic has proven to be a powerful formalism in reasoning about memory and concurrency in object-oriented programs - specifically in Java, but there are still challenges in reasoning about more advanced languages such as Scala. Of the features Scala provides beyond Java, this thesis focusses on first class functions and lexical closures. A formal model subset of Scala is defined, around these features. Using this foundation we present an extension to permission-based separation logic to specify and reason about functions and closures. Furtermore we provide a demonstration and an argument for its use by performing a case study on the Scala actors library.
Item Type:Essay (Master)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science MSc (60300)
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page