Add introduction draft

appendix/bibliography/bibliography.bib

@@ -17,6 +17,16 @@ @article{GenevaConvention
 numpages = {6}
 }
 
+@article{beyondGenevaConvention,
+  title={Beyond the geneva convention on the treatment of object aliasing},
+  author={Clarke, Dave and Noble, James and Wrigstad, Tobias},
+  journal={Aliasing in Object-Oriented Programming. Types, Analysis and Verification},
+  pages={1--6},
+  year={2013},
+  publisher={Springer}
+}
+
+
 @article{zimmerman2023latte,
   title={Latte: Lightweight Aliasing Tracking for Java},
   author={Zimmerman, Conrad and Gamboa, Catarina and Fonseca, Alcides and Aldrich, Jonathan},
@@ -61,7 +71,9 @@ @article{aldrich2002alias
   publisher={ACM New York, NY, USA}
 }
 
-@INPROCEEDINGS{1029817,
+// TODO: decide what to keep for separation logic
+
+@INPROCEEDINGS{separationLogic1,
   author={Reynolds, J.C.},
   booktitle={Proceedings 17th Annual IEEE Symposium on Logic in Computer Science}, 
   title={Separation logic: a logic for shared mutable data structures}, 
@@ -72,8 +84,35 @@ @INPROCEEDINGS{1029817
   keywords={Data structures;Computer science;Programmable logic arrays;Reflection;Logic programming;Computer languages;Logic arrays;Arithmetic;Artificial intelligence;Bibliographies},
   doi={10.1109/LICS.2002.1029817}}
 
+@inproceedings{separationLogic2,
+  title={Local reasoning about programs that alter data structures},
+  author={O’Hearn, Peter and Reynolds, John and Yang, Hongseok},
+  booktitle={Computer Science Logic: 15th International Workshop, CSL 2001 10th Annual Conference of the EACSL Paris, France, September 10--13, 2001, Proceedings 15},
+  pages={1--19},
+  year={2001},
+  organization={Springer}
+}
 
-@inproceedings{MuellerSchwerhoffSummers16,
+@article{separationLogic3,
+author = {Ishtiaq, Samin S. and O'Hearn, Peter W.},
+title = {BI as an assertion language for mutable data structures},
+year = {2001},
+issue_date = {March 2001},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+volume = {36},
+number = {3},
+issn = {0362-1340},
+url = {https://doi.org/10.1145/373243.375719},
+doi = {10.1145/373243.375719},
+abstract = {Reynolds has developed a logic for reasoning about mutable data structures in which the pre- and postconditions are written in an intuitionistic logic enriched with a spatial form of conjunction. We investigate the approach from the point of view of the logic BI of bunched implications of O'Hearnand Pym. We begin by giving a model in which the law of the excluded middleholds, thus showing that the approach is compatible with classical logic. The relationship between the intuitionistic and classical versions of the system is established by a translation, analogous to a translation from intuitionistic logic into the modal logic S4. We also consider the question of completeness of the axioms. BI's spatial implication is used to express weakest preconditions for object-component assignments, and an axiom for allocating a cons cell is shown to be complete under an interpretation of triplesthat allows a command to be applied to states with dangling pointers. We make this latter a feature, by incorporating an operation, and axiom, for disposing of memory. Finally, we describe a local character enjoyed by specifications in the logic, and show how this enables a class of frame axioms, which say what parts of the heap don't change, to be inferred automatically.},
+journal = {SIGPLAN Not.},
+month = {jan},
+pages = {14–26},
+numpages = {13}
+}
+
+@inproceedings{Viper,
   author      = {P. M{\"u}ller and M. Schwerhoff and A. J. Summers},
   title       = {Viper: A Verification Infrastructure for Permission-Based Reasoning},
   booktitle   = {Verification, Model Checking, and Abstract Interpretation (VMCAI)},
@@ -130,6 +169,19 @@ @online{Kotlin
   url          = {https://kotlinlang.org/},
 }
 
+@article{KotlinSpec,
+  title={Kotlin language specification},
+  author={Akhin, Marat and Belyaev, Mikhail},
+  journal={Kotlin Language Specification},
+  year={2021}
+}
+
+@online{ViperWebSite,
+  author = {Department of Computer Science, ETH Zürich},
+  title = {Viper Language},
+  url = {https://www.pm.inf.ethz.ch/research/viper.html},
+}
+
 @misc{FormVerPlugin,
   title = {Formal Verification Plugin for Kotlin},
   year = {2024},

chapters/1-Introduction.typ

@@ -1,5 +1,74 @@
 #pagebreak(to:"odd")
 
-*TODO: For all chapters/subchapters, consistency in the use of capital letters in titles.*
+= Introduction
 
-= Introduction
+Aliasing is a topic that has been studied for decades  @Aliasing-OOP @GenevaConvention @beyondGenevaConvention in Computer Science and it refers to the situation where two or more references point to the same object.
+Aliasing is an important characteristic of object-oriented programming languages allowing the programmers to develope complex designs involving sharing. However, reasoning about programs written with languages that allow aliasing without any kind of control is a hard task for programmers, compilers and formal verifcation tools. In fact, as reported in the Geneva Convention @GenevaConvention, without having guarantees about aliasing it can be difficult to prove the correctness of a simple Hoare formula like the following. $ {x = "true"} space y := "false" {x = "true"} $ 
+Indeed, when $x$ and $y$ are aliased, the formula is not valid, and most of the time proving that aliasing cannot occur is not straightforward.
+
+#v(1em)
+// TODO: decide whether to keep @separationLogic3
+
+This work aims to show how controlling aliasing through an annotation system can allow to refine formal verifcation @FormVerPlugin for the Kotlin language @Kotlin @KotlinSpec.
+In particular, formal verification is performed using Viper @ViperWebSite @Viper, a language developed by ETH Zurich.
+Viper is an intermediate verification language that allows to write functions with preconditions and postconditions. The correctness of these conditions is verified using one of the two verification back-ends (one based on symbolic execution and one based on verification condition generation) and an SMT solver.
+In order to verify Kotlin code with Viper it is just necessary to translate the former language into the latter.
+However, Viper's memory model is based on separation logic @separationLogic1 @separationLogic2 @separationLogic3 disallowing references that are both shared and mutable.
+This restriction becomes problematic when encoding Kotlin code into Viper since Kotlin does not provide such guarantees.
+
+To understand better the problem, it is possible to look at the Kotlin code in @example-kt-1 where passing the same reference twice when calling function `f`, and thus creating aliasing, is completely allowed by the language. @example-vpr-1 shows a wrong way to encoding the example presented in @example-kt-1. The Viper example, despite being really similar to the Kotlin one, fails verification when calling `f(x, x)`. This happens because `f` requires write access to the field `n` of its arguments and, as mentioned before, Viper disallows references to be shared and mutable at the same time.
+
+#figure(
+  caption: "Kotlin code containg aliasing",
+  ```kt
+  class A(var n: Int)
+
+  fun f(x: A, y: A) {
+      x.n = 1
+      y.n = 2
+  }
+
+  fun use_f(x: A) {
+      f(x, x)
+  }
+  ```
+)<example-kt-1>
+
+#figure(
+  caption: "Viper code containg aliasing",
+  ```java
+  field n: Int
+
+  method f(x: Ref, y: Ref)
+  requires acc(x.n) && acc(y.n)
+  {
+    x.n := 1
+    y.n := 2
+  }
+
+  method use_f(x: Ref)
+  requires acc(x.n)
+  {
+    f(x, x) // verifcation error
+  }
+  ```
+)<example-vpr-1>
+
+Kotlin does not provide primitives to control or avoid aliasing. This work shows that this problem can be overcome by introducing an annotation system for controlling aliasing.
+// TODO: elaborate this part a bit more 
+
+#v(1em)
+
+The rest of the thesis is organized as follows:
+
+/ @cap:background : provides a description of the background information needed to understand the concepts presented by this work. In particular, this chapter presents the Kotlin programming language and its feature of interest for the thesis. After that, an overview to the "Aliasing" topic in Computer Science is provided and finally it is presented an introduction to the Viper language and set of verifcation tools.
+
+/ @cap:related-work : analyzes works that has been fundamental for the development of this thesis. The chapter is divided in two parts, the former describing existing works about aliasing and systems for controlling it; the latter gives an overview of the already existing tools that perform formal verification using Viper.
+
+/ @cap:annotation-system : presents a novel annotation system for controlling aliasing on a language that can represent a significant subset of the Kotlin language. After introducing the language and several auxiliary rules and functions, the typing rules for the system are formalized.
+
+/ @cap:annotations-kt : discusses the application of the proposed annotation system in the Kotlin language. It shows several examples of Kotlin code extended with these annotations and explores how the annotations can be used for bringing improvements to the language.
+
+/ @cap:encoding : shows how the annotation system presented before can be used to obtain a better encoding of Kotlin into Viper, thus improving the quality of verification.
+
+/ @cap:conclusion : summarizes the contributions of this research and points out reasonable extensions to this work as well as potential new areas for future research.

chapters/2-Background.typ

@@ -1,5 +1,5 @@
 #pagebreak(to:"odd")
-= Background
+= Background<cap:background>
 
 // TODO: symbols for code that compiles vs code that doesn't?
 // TODO: cite language specification
@@ -210,7 +210,7 @@ Aliasing prevention alone is insufficient because aliasing is unavoidable in con
 == Viper and Separation Logic
 
 === Separation Logic
-In Computer Science, separation logic @1029817 is an extension of Hoare logic, a way of reasoning about programs.
+In Computer Science, separation logic @separationLogic1 @separationLogic2 @separationLogic3 is an extension of Hoare logic, a way of reasoning about programs.
 
 Separation logic facilitates reasoning about:
 - Programs that manipulate pointer data structures including information hiding in the presence of pointers.
@@ -229,7 +229,7 @@ $
 
 // TODO: use different words (this is just copy pasted)
 
-Viper @MuellerSchwerhoffSummers16 (Verification Infrastructure for Permission-based Reasoning) is a language and suite of tools, providing an architecture on which new verification tools and prototypes can be developed simply and quickly. Viper is being developed at ETH Zurich in close collaboration with the team of Alex Summers at UBC.
+Viper @Viper @ViperWebSite (Verification Infrastructure for Permission-based Reasoning) is a language and suite of tools, providing an architecture on which new verification tools and prototypes can be developed simply and quickly. Viper is being developed at ETH Zurich in close collaboration with the team of Alex Summers at UBC.
 
 Viper comprises a novel intermediate verification language, also named Viper, and automatic verifiers for the language, as well as example front-end tools. The Viper toolset can be used to implement verification techniques for front-end programming languages via translations into the Viper language.
 

chapters/3-Related-Work.typ

@@ -1,5 +1,5 @@
 #pagebreak(to:"odd")
-= Related Work
+= Related Work<cap:related-work>
 
 == Systems for Aliasing Control
 

chapters/4-Annotation-System.typ

@@ -13,7 +13,7 @@
 // TODO: decide whether to put unique, shared, borrowed in italic
 // TODO: decide whether to put nomi delle regole in italic
 
-= Annotation System
+= Annotation System<cap:annotation-system>
 
 This chapter describes an annotation system for controlling aliasing within a subset of the Kotlin language.
 The system takes inspiration from some previous works @boyland2001alias @zimmerman2023latte @aldrich2002alias  but it also introduces significant modifications.

chapters/5-Annotations-Kotlin.typ

@@ -1,5 +1,5 @@
 #pagebreak(to:"odd")
-= Annotations in Kotlin
+= Annotations in Kotlin<cap:annotations-kt>
 
 == Examples of Aliasing control in Kotlin
 

chapters/6-Encoding.typ

@@ -1,5 +1,5 @@
 #pagebreak(to:"odd")
-= Encoding in Viper
+= Encoding in Viper<cap:encoding>
 @FormVerPlugin
 
 == Classes Encoding

chapters/7-Conclusion.typ

@@ -1,5 +1,5 @@
 #pagebreak(to:"odd")
-= Conclusion
+= Conclusion<cap:conclusion>
 == Results
 == Future Work
 === Improving Annotations Inference