add annotation system intro

appendix/bibliography/bibliography.bib

@@ -139,6 +139,26 @@ @book{Aliasing-OOP
 address = {Berlin, Heidelberg}
 }
 
+@article{Featherweight-Java,
+author = {Igarashi, Atsushi and Pierce, Benjamin C. and Wadler, Philip},
+title = {Featherweight Java: a minimal core calculus for Java and GJ},
+year = {2001},
+issue_date = {May 2001},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+volume = {23},
+number = {3},
+issn = {0164-0925},
+url = {https://doi.org/10.1145/503502.503505},
+doi = {10.1145/503502.503505},
+abstract = {Several recent studies have introduced lightweight versions of Java: reduced languages in which complex features like threads and reflection are dropped to enable rigorous arguments about key properties such as type safety. We carry this process a step further, omitting almost all features of the full language (including interfaces and even assignment) to obtain a small calculus, Featherweight Java, for which rigorous proofs are not only possible but easy. Featherweight Java bears a similar relation to Java as the lambda-calculus does to languages such as ML and Haskell. It offers a similar computational "feel," providing classes, methods, fields, inheritance, and dynamic typecasts with a semantics closely following Java's. A proof of type safety for Featherweight Java thus illustrates many of the interesting features of a safety proof for the full language, while remaining pleasingly compact. The minimal syntax, typing rules, and operational semantics of Featherweight Java make it a handy tool for studying the consequences of extensions and variations. As an illustration of its utility in this regard, we extend Featherweight Java with generic classes in the style of GJ (Bracha, Odersky, Stoutamire, and Wadler) and give a detailed proof of type safety. The extended system formalizes for the first time some of the key features of GJ.},
+journal = {ACM Trans. Program. Lang. Syst.},
+month = {may},
+pages = {396–450},
+numpages = {55},
+keywords = {Compilation, Java, generic classes, language design, language semantics}
+}
+
 TO BE ADDED PROBABLY
 - reachability types
 - capabilities for uniqueness and borrowing 

chapters/4-Annotation-System.typ

@@ -1,20 +1,70 @@
+#import "../config/utils.typ": *
+
 #pagebreak(to:"odd")
 = Annotation System
 
-== Aliasing control in Kotlin
+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.
+
+One distinguishing trait of this system is that it is designed exclusively for Kotlin, while the majority of previous works are made for Java and other languages.
+It is also specifically made for being as lightweight as possible and gradually integrable with already existing code.
+// TODO: borrowed unique / borrowed shared distinction here?
+
+A unique design goal of this system is to improve the verification process with Viper by establishing a link between separation logic and the absence of aliasing control in Kotlin.
+
+== Grammar
+
+@Featherweight-Java
+
+#frame-box(
+  $
+    CL &::= class C(overline(f\: alpha_f)) \
+    af &::= unique | shared \
+    beta &::= dot | borrowed \
+    M &::= m(overline(af beta space x)): af {begin_m; overline(s); ret_m e} \
+    p &::= x | p.f \
+    e &::= null | p | m(overline(p)) \
+    s &::= var x | p = e |  fi p_1 == p_2 then overline(s_1) els overline(s_2) | m(overline(p))
+    // \ &| loop p_1 == p_2 do overline(s)
+  $
+)
+
+- Only *fields*, *method parameters*, and *return values* have to be annotated.
+- A reference annotated as `unique` may either be `null` or point to an object, and it is the sole *accessible* reference pointing to that object.
+- A reference marked as `shared` can point to an object without being the exclusive reference to that object.
+- `T` is an annotation that can only be inferred and means that the reference is *not accessible*.
+- $borrowed$ (borrowed) indicates that the function receiving the reference won't create extra aliases to it, and on return, its fields will maintain at least the permissions stated in the class declaration. 
+- Annotations on fields indicate only the default permissions, in order to understand the real permissions of a fields it is necessary to look at the context. This concept is formalized by rules in /*@cap:paths*/ and shown in /*@field-annotations.*/
+- Primitive fields are not considered
+- `this` can be seen as a parameter
+- constructors can be seen as functions returning a `unique` value
+
+== Context
+
+#frame-box(
+  $
+    alpha &::= unique | shared | top \
+    beta &::= dot | borrowed \
+    Delta &::= dot | p : alpha beta, Delta
+  $
+)
+
+// TODO: put this in a separate chapter
+
+// == Aliasing control in Kotlin
 
-=== Verify  contracts
+// === Verify  contracts
 
 
-// example of contracts usage
+// // example of contracts usage
 
-// example of improvement in verification of contracts
+// // example of improvement in verification of contracts
 
-// quote something??
+// // quote something??
 
-=== Static analysis (IntelliJ)
-=== Smart cast
-=== Function optimiztion (modify lists implace)
-=== Garbage collection in Kotlin native
+// === Static analysis (IntelliJ)
+// === Smart cast
+// === Function optimiztion (modify lists implace)
+// === Garbage collection in Kotlin native
 
-== The system
+// == The system

config/utils.typ

@@ -78,9 +78,12 @@
 }
 
 #let frame-box = it => {
-  box(
-    inset: 8pt,
-    stroke: black,
-    it
+  align(
+    center,
+    box(
+      inset: 8pt,
+      stroke: black,
+      it
+    )
   )
 }