Charl de Leur - Permission-based separation logic for Scala

author:Charl de Leur
title:Permission-based separation logic for Scala
keywords:
topics:Algorithms and Data Structures, Logics and semantics
committee:prof.dr. M. Huisman
Kuper (CAES)
dr. S.C.C. Blom
graduation date:27 August 2015


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.

References

  1. The Scala programming language (Digital version available here)
  2. Christian Haack, Marieke Huisman, and Clément Hurlin. Permission-based separation logic for Java. Manuscript, 2010. (Digital version available here)
  3. The VerCors project (Digital version available here)