Fix introduction

appendix/bibliography/bibliography.bib

@@ -71,7 +71,7 @@ @article{aldrich2002alias
   publisher={ACM New York, NY, USA}
 }
 
-@INPROCEEDINGS{separationLogic1,
+@INPROCEEDINGS{separationLogic3,
   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}, 
@@ -91,7 +91,7 @@ @inproceedings{separationLogic2
   organization={Springer}
 }
 
-@article{separationLogic3,
+@article{separationLogic1,
 author = {Ishtiaq, Samin S. and O'Hearn, Peter W.},
 title = {BI as an assertion language for mutable data structures},
 year = {2001},

chapters/1-Introduction.typ

@@ -1,62 +1,32 @@
+#import "../config/utils.typ": code-compare
+#import "../vars/kt-to-vpr-examples.typ": intro-kt, intro-vpr
 #pagebreak(to:"odd")
 
 = 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 a topic that has been studied for decades  @Aliasing-OOP @beyondGenevaConvention @GenevaConvention 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.
 
 == Contributions
 
-This work aims to show how controlling aliasing through an annotation system can allow to refine formal verifcation performed by an already existing plugin @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 containing 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 containing 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>
-
-Differently from other programming languages, Kotlin lacks built-in mechanisms to control or prevent aliasing.
-This work addresses this issue by proposing the introduction of an annotation system specifically designed to manage and control aliasing in Kotlin. By incorporating this annotation system, developers can enforce stricter aliasing rules, improving the reliability of their code. This also enables to perform better formal verification, allowing to prove more interesting properties.
-
-== Overview
+This work demonstrates how controlling aliasing through an annotation system can enhance the formal verification process performed by an existing plugin @FormVerPlugin for the Kotlin language @KotlinSpec @Kotlin. The plugin verifies Kotlin using Viper @ViperWebSite @Viper, an intermediate verification language developed by ETH Zurich. Viper is designed to verify programs by enabling the specification of functions with preconditions and postconditions, which are then checked for correctness. This verification is performed using one of two back-ends: symbolic execution or verification condition generation, both of which rely on an SMT solver to validate the specified conditions.
+
+In order to verify to Kotlin with Viper, it is necessary to translate the former language into the latter. However, this translation presents challenges due to fundamental differences between the two languages. Specifically, Viper's memory model is based on separation logic @separationLogic1 @separationLogic2 @separationLogic3, which disallows shared mutable references. In contrast, Kotlin does not restrict aliasing, meaning that references in Kotlin can be both shared and mutable, posing a significant challenge when trying to encode Kotlin code into Viper.
+
+This issue is clearly illustrated in the Kotlin code example provided in @intro-comp. In that example, the language allows the same reference to be passed multiple times when calling function `f`, thereby creating aliasing. @intro-comp also shows a wrong approach for encoding that Kotlin code into Viper. Despite the Viper code closely resembling the original Kotlin code, it fails verification when `f(x, x)` is called. This failure occurs because `f` requires write access to the field `n` of its arguments, but as previously mentioned, Viper’s separation logic disallows references from being both shared and mutable simultaneously.
+
+#code-compare("Kotlin code with aliasing and its problematic encoding into Viper", .8fr, intro-kt, intro-vpr)<intro-comp>
+
+As mentioned before, Kotlin does not have built-in mechanisms to manage or prevent aliasing, which can lead to unintended side effects and make it harder to ensure code correctness. To address this issue, this work proposes and formalizes an annotation system specifically designed to manage and control aliasing within Kotlin.
+
+The proposed annotation system introduces a way for developers to specify and enforce stricter aliasing rules by tagging references with appropriate annotations. 
+This helps to clearly distinguish between references that might be shared and those that are unique. Additionally, the system differentiates between functions that create new aliases for their parameters and those that do not.
+This level of control is important for preventing common programming errors related to mutable shared state, such as race conditions or unintended side effects.
+
+The introduction of this annotation system not only improves the reliability of Kotlin programs by reducing the risk of aliasing-related bugs but also enhances the formal verification process using Viper. This work demonstrates how to effectively encode Kotlin programs into Viper by aligning Kotlin’s memory model with Viper’s memory model through the proposed annotation system.
+
+== Structure of the thesis
 
 The rest of the thesis is organized as follows:
 

vars/kt-to-vpr-examples.typ

@@ -1,3 +1,35 @@
+#let intro-kt = ```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)
+}
+```
+
+#let intro-vpr = ```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
+}
+```
+
 #let classes-kt = ```kt
 open class A(
     val x: Int,