Modify structure

chapters/3-Related-Work.typ

@@ -84,7 +84,10 @@ Recently, several programming languages have started to introduce type systems t
 
 Rust @rustlang is a modern programming language that prioritizes both high performance and static safety. A crucial aspect of Rust is its ownership-based type system, which ensures complete memory safety by preventing issues like dangling pointers, data races, and unintended side effects from aliased references. This type system enforces strict rules, allowing memory to be either mutable or shared, but not both simultaneously, thereby avoiding common memory errors. Additionally, this design choice simplifies the process of formal verification.
 
-- *TODO: Swift*
+- *TODO: Swift* 
+// https://github.com/swiftlang/swift/blob/main/docs/OwnershipManifesto.md
+// https://www.swift.org/migration/documentation/swift-6-concurrency-migration-guide/dataracesafety/
+// https://docs.swift.org/swift-book/documentation/the-swift-programming-language/declarations#Parameter-Modifiers
 - *TODO: Ocaml???*
 
 == Tools for verification with Viper

chapters/5-Annotations-Kotlin.typ → chapters/4-Annotations-Kotlin.typ

@@ -1,13 +1,18 @@
 #pagebreak(to:"odd")
-= Annotations in Kotlin<cap:annotations-kt>
+= Uniqueness in Kotlin<cap:annotations-kt>
+
+== Overview
 
 == Examples of Aliasing control in Kotlin
 
 // put examples that are currently in chapter 4
 
+// -> maybe something simpler here
+
 == Stack example
 
 // since it's popular to have this example (latte, aliasJava)
+// maybe it's better to have this in the end of chapter 5
 
 == Improvents to the language
 

chapters/4-Annotation-System.typ → chapters/5-Annotation-System.typ

@@ -28,20 +28,19 @@ A unique design goal of this system is to improve the verification process with
 
 In order to define the rules of this annotation system, a grammar representing a substet of the Kotlin language is used.
 
-#figure(
-  caption: "Grammar defining a subset of the Kotlin language",
-  frame-box(
-    $
-      CL &::= class C(overline(f\: alpha_f)) \
-      M &::= m(overline(x\: af beta)): af {begin_m; overline(s); ret_m e} \
-      af &::= unique | shared \
-      beta &::= dot | borrowed \
-      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)
-    $
-))
+
+#frame-box(
+  $
+    CL &::= class C(overline(f\: alpha_f)) \
+    M &::= m(overline(x\: af beta)): af {begin_m; overline(s); ret_m e} \
+    af &::= unique | shared \
+    beta &::= dot | borrowed \
+    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)
+  $
+)
 
 === Classes and Methods
 - Primitive fields are not considered
@@ -107,12 +106,15 @@ fun m3(
 ```
 #align(
   center,
-  grid(
-    columns: (auto, auto),
-    column-gutter: 2em,
-    row-gutter: .5em,
-    [*Grammar*],[*Kotlin*],
-    grammar_annotations, kt_annotations
+  figure(
+    caption: "Comparision between the grammar and annotated Kotlin",
+    grid(
+      columns: (auto, auto),
+      column-gutter: 2em,
+      row-gutter: .5em,
+      [*Grammar*],[*Kotlin*],
+      grammar_annotations, kt_annotations
+    )
   )
 )
 
@@ -129,6 +131,8 @@ fun m3(
 
 == Context
 
+A context is a list of paths associated with their annotations $alpha$ and $beta$. While $beta$ is defined in the same way of the grammar, $alpha$ is slightly different. Other than _unique_ and _shared_, in a context, an annotation $alpha$ can also be $top$. As will be better explained in the following sections, the annotation $top$ can only be inferred, so it is not possible for the user to write it. A path annotated with $top$ within a context is not accessible, meaning that the path needs to be re-assigned before beign read. The formal meaning of the annotation $top$ will be clearer while formilizing the statement typing rules.
+
 #frame-box(
   $
     alpha &::= unique | shared | top \
@@ -137,10 +141,6 @@ fun m3(
   $
 )
 
-#v(1em)
-
-A context is a list of paths associated with their annotations $alpha$ and $beta$. While $beta$ is defined in the same way of the grammar, $alpha$ is slightly different. Other than _unique_ and _shared_, in a context, an annotation $alpha$ can also be $top$. As will be better explained in the following sections, the annotation $top$ can only be inferred, so it is not possible for the user to write it. A path annotated with $top$ within a context is not accessible, meaning that the path needs to be re-assigned before beign read. The formal meaning of the annotation $top$ will be clearer while formilizing the statement typing rules.
-
 === Well-Formed Context
 
 #display-rules(

preface/abstract.typ

@@ -1,6 +1,5 @@
 #import "../config/constants.typ": abstract
 #set page(numbering: "i")
-#counter(page).update(1)
 
 #v(10em)
 

structure.typ

@@ -14,8 +14,8 @@
 #include "./chapters/1-Introduction.typ"
 #include "./chapters/2-Background.typ"
 #include "./chapters/3-Related-Work.typ"
-#include "./chapters/4-Annotation-System.typ"
-#include "./chapters/5-Annotations-Kotlin.typ"
+#include "./chapters/4-Annotations-Kotlin.typ"
+#include "./chapters/5-Annotation-System.typ"
 #include "./chapters/6-Encoding.typ"
 #include "./chapters/7-Conclusion.typ"