University of Twente Student Theses
Permission-based separation logic for Scala
Leur, C. de (2015) Permission-based separation logic for Scala.
|
PDF
1MB |
| 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: | https://purl.utwente.nl/essays/68029 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page