From f5a900a303033f9c1b449c9fbae35cc5137754a3 Mon Sep 17 00:00:00 2001 From: Francesco Protopapa Date: Wed, 11 Sep 2024 13:27:34 +0200 Subject: [PATCH] Adjustments --- appendix/full-rules-set.typ | 16 +++++------ chapters/1-Introduction.typ | 12 ++++---- chapters/2-Background.typ | 8 +++--- chapters/3-Related-Work.typ | 8 +++--- chapters/4-Annotations-Kotlin.typ | 5 ++-- chapters/5-Annotation-System.typ | 48 +++++++++++++++---------------- config/utils.typ | 2 +- preface/copyright.typ | 2 +- vars/kt-to-vpr-examples.typ | 4 +-- vars/rules/base.typ | 18 ++++++------ 10 files changed, 62 insertions(+), 61 deletions(-) diff --git a/appendix/full-rules-set.typ b/appendix/full-rules-set.typ index 221f11e..bbab762 100644 --- a/appendix/full-rules-set.typ +++ b/appendix/full-rules-set.typ @@ -27,7 +27,7 @@ All the following rules are to be considered for a given program $P$, where fiel Ctx-Base, Ctx-Rec, ) -== Sub-Paths and Sup-Paths +== Sub-Paths and Super-Paths === Definition @@ -46,9 +46,9 @@ All the following rules are to be considered for a given program $P$, where fiel === Deep Remove #display-rules( - Remove-SupPathsEq-Empty, "", - Remove-SupPathsEq-Discard, "", - Remove-SupPathsEq-Keep, "", + Remove-SuperPathsEq-Empty, "", + Remove-SuperPathsEq-Discard, "", + Remove-SuperPathsEq-Keep, "", ) === Replace @@ -57,12 +57,12 @@ All the following rules are to be considered for a given program $P$, where fiel Replace, "", ) -=== Get Sup-Paths +=== Get Super-Paths #display-rules( - Get-SupPaths-Empty, "", - Get-SupPaths-Discard, "", - Get-SupPaths-Keep, "", + Get-SuperPaths-Empty, "", + Get-SuperPaths-Discard, "", + Get-SuperPaths-Keep, "", ) == Relations between Annotations diff --git a/chapters/1-Introduction.typ b/chapters/1-Introduction.typ index 18ebb92..5db8c67 100644 --- a/chapters/1-Introduction.typ +++ b/chapters/1-Introduction.typ @@ -4,7 +4,7 @@ = Introduction -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 a topic that has been studied for decades in computer science @Aliasing-OOP @beyondGenevaConvention @GenevaConvention 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 verification tools. In fact, as reported in _the Geneva Convention on the Treatment of Object Aliasing_ @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. @@ -15,7 +15,7 @@ This verification is possible because separation logic allows to express that $x This work demonstrates how controlling aliasing through an annotation system can enhance the formal verification process performed by SnaKt @FormVerPlugin, an existing plugin for the Kotlin language @KotlinSpec @Kotlin. SnaKt 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 @MuellerSchwerhoffSummers16b or verification condition generation @HeuleKassiosMuellerSummers13, 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, 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. +In order to verify to Kotlin with Viper, it is necessary to translate the former language into the latter. However, this translation presents several challenges due to fundamental differences between the two languages. Specifically, Viper's memory model is based on separation logic, 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. Additionally, @intro-comp presents a naive 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. @@ -42,12 +42,12 @@ 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. Following this, the chapter provides an overview of the "Aliasing" topic in Computer Science and presents an introduction to the Viper language and its set of verification 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:related-work : analyzes works that have 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 giving 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 : introduces a uniqueness system for the Kotlin language. It shows several examples of Kotlin code extended with uniqueness annotations and explores how the annotations can be used for bringing improvements to the language. -/ @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:annotation-system : formalizes the annotation system introduced before 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: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: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 performed by SnaKt. / @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. diff --git a/chapters/2-Background.typ b/chapters/2-Background.typ index 5df5db4..ff3d081 100644 --- a/chapters/2-Background.typ +++ b/chapters/2-Background.typ @@ -39,7 +39,7 @@ In Kotlin, when the compiler can determine that a variable's type is more specif === Null Safety -Kotlin's type system has been designed with the goal of eliminating the danger of null references. In many programming languages, including Java, accessing a member of a null reference results in a null reference exception. This is more difficult to happen in Kotlin since the type system distinguishes between references that can hold `null` and those that cannot, the former are called nullable references while the latter are called non-nullable reference. @kt-null-safety shows how nullable references are declared by appending a question mark to the type name and it shows that trying to assign `null` to a non-nullable reference leads to a compilation error. +Kotlin's type system has been designed with the goal of eliminating the danger of null references. In many programming languages, including Java, accessing a member of a null reference results in a null reference exception. Kotlin avoids most of these situations because the type system distinguishes between references that can hold `null` and those that cannot, the former are called nullable references while the latter are called non-nullable references. @kt-null-safety shows how nullable references are declared by appending a question mark to the type name and it shows that trying to assign `null` to a non-nullable reference leads to a compilation error. #figure( caption: "Kotlin null safety example", @@ -86,7 +86,7 @@ A backing field is generated under two conditions: if the property relies on the set(value) { // setter if (value > 0) field = value // accessing backing field else throw IllegalArgumentException( - "Square size must be greater than 0" + "Square width must be greater than 0" ) } val area @@ -99,7 +99,7 @@ A backing field is generated under two conditions: if the property relies on the Kotlin contracts @KotlinContracts are an experimental feature introduced in Kotlin 1.3 designed to provide additional guarantees about code behavior, helping the compiler in performing more precise analysis and optimizations. Contracts are defined using a special contract block within a function, describing the relationship between input parameters and the function's effects. This can include conditions such as whether a lambda is invoked or if a function returns under certain conditions. By specifying these relationships, contracts provide guarantees to the caller of a function, offering the compiler additional information that enable more advanced code analysis. -It is important to point out that currently contracts correctness is not statically verified. The compiler trusts contracts unconditionally meaning that the programmer is responsible for writing correct and sound contracts. +It is important to point out that currently contracts are only partially verified by the compiler. In certain cases, the compiler trusts the contracts without verification, placing the responsibility on the programmer to ensure that the contracts are correct. In @contract-1 it is possible to see how contracts allow the initialization of immutable variables within the body of a lambda, doing this is not possible without using a contract (@contract-2). @@ -404,7 +404,7 @@ As well as being declared in preconditions and postconditions, field permissions Sometimes, exclusive permissions can be too restrictive. Viper also allows to have fractional permissions for heap locations that can be shared but only read. Fractional permissions are declared with a permission amount between 0 and 1 or with the `wildcard` keyword. The value represented by a `wildcard` is not constant, instead it is reselected each time an expression involving a `wildcard` is identified. -The `wildcard` permission amount provides a convenient way to implement duplicable read-only resources, which is often suitable for the representation of immutable data. The example in @vpr-fractional shows how fractional permissions can be combined to gain full permissions (Line 6-7). In the same example it is also possible to see that Viper does not allow to have a permission amount greater than 1, in fact, since `wildcard` is an amount grater than 0, a situation in which `x == y == z` is not possible and so the assertion on Line 11 can be verified. +The `wildcard` permission amount provides a convenient way to implement duplicable read-only resources, which is often suitable for the representation of immutable data. The example in @vpr-fractional shows how fractional permissions can be combined to gain full permissions (Line 6-7). In the same example it is also possible to see that Viper does not allow to have a permission amount greater than 1, in fact, since `wildcard` is an amount greater than 0, a situation in which `x == y == z` is not possible and so the assertion on Line 11 can be verified. #figure( caption: "Viper fractional permissions example", diff --git a/chapters/3-Related-Work.typ b/chapters/3-Related-Work.typ index c482b58..1ce85b1 100644 --- a/chapters/3-Related-Work.typ +++ b/chapters/3-Related-Work.typ @@ -51,8 +51,8 @@ AliasJava is characterized by a strong uniqueness invariant asserting that "at a This invariant is maintained by the fact that unique references can only be read in a destructive manner, meaning that immediately being read, the value `null` is assigned to the reference. Boyland @boyland2001alias proposes a system for controlling aliasing in Java that does not require to use destructive reads. -The system utilizes a set of annotations to distinguish between different types of references. Specifically, procedure parameters and return values can be annotated as unique, indicating that they are not aliased elsewhere. Conversely, parameters and return values that are not unique are classified as shared. Within this system, a shared parameter may also be declared as borrowed, meaning that the function will not create further aliases for that parameter. Finally, fields can be marked as unique; if not, they are treated as shared. -The main contribution of this work is the introduction of the "alias burying" rule: "When a unique field of an object is read, all aliases of the field are made undefined". This means that aliases of a unique field are allowed if they are assigned before being used again. The "alias burying" rule is important because it allows to avoid having destructive reads for unique references. +The system utilizes a set of annotations to distinguish between different types of references. Specifically, procedure parameters and return values can be annotated as unique, indicating that they are not aliased elsewhere. Conversely, parameters and return values that are not unique are classified as shared. Within the system, a shared parameter may also be declared as borrowed, meaning that the function will not create further aliases for that parameter. Finally, fields can be marked as unique; if not, they are treated as shared. +The main contribution of Boyland's work is the introduction of the "alias burying" rule: "When a unique field of an object is read, all aliases of the field are made undefined". This means that aliases of a unique field are allowed if they are assigned before being used again. The "alias burying" rule is important because it allows to avoid having destructive reads for unique references. On the other hand, having a shared reference does not provide any guarantee on the uniqueness of that reference. Finally the object referred to by a borrowed parameter may not be returned from a procedure, assigned to a field or passed as a non-borrowed parameter. @@ -88,7 +88,7 @@ By default, Prusti ensures that a Rust program will not encounter an unrecoverab In addition to use Prusti to ensure that programs are free from runtime panics, developers can gradually add annotations to their code, thereby achieving increasingly robust correctness guarantees and improving the overall reliability and safety of their software. -In terms of Viper encoding, Rust structs are represented as potentially nested and recursive predicates representing unique access to a type instance. Furthermore, moves and straightforward usages of Rust's shared and mutable borrows are akin to ownership transfers within the permission semantics of separation logic assertions. Reborrowing is directly modeled using magic wands: when a reborrowed reference is returned to the caller, it includes a magic wand denoting the ownership of all locations from which borrowing occurred, except those currently in the proof. +In terms of Viper encoding, Rust structs are represented as potentially nested and recursive predicates representing unique access to a type instance. Furthermore, moves and straightforward usages of Rust's shared and mutable borrows are akin to ownership transfers within the permission semantics of separation logic assertions. Reborrowing is directly modeled using magic wands, Viper's counterpart to the separating implication in separation logic. When a reborrowed reference is returned to the caller, it includes a magic wand denoting the ownership of all locations from which borrowing occurred, except those currently in the proof. === Gobra @@ -96,7 +96,7 @@ Go is a programming language that combines typical characteristics of imperative Gobra @gobra is a tool designed for Go that allows modular verification of programs. It can ensure memory safety, crash resistance, absence of data races, and compliance with user-defined specifications. -Compared to Prusti, Gobra generally requires more user-provided annotations. Benchmarks indicate that the annotation overhead varies from 0.3 to 3.1 lines of annotations per line of code. +Compared to Prusti, Gobra generally requires more user-provided annotations. Benchmarks by Wolf et al. @gobra indicate that the annotation overhead varies from 0.3 to 3.1 lines of annotations per line of code. === Nagini diff --git a/chapters/4-Annotations-Kotlin.typ b/chapters/4-Annotations-Kotlin.typ index c6c493b..a4f0bc0 100644 --- a/chapters/4-Annotations-Kotlin.typ +++ b/chapters/4-Annotations-Kotlin.typ @@ -107,6 +107,7 @@ The uniqueness system handles assignments similarly to Alias Burying @boyland200 } fun correctAssignment(@Unique a: A) { + borrowUnique(a.t) // ok, 'a.t' remains accessible val temp = a.t // 'temp' becomes unique, but 'a.t' becomes inaccessible borrowUnique(temp) // ok a.t = null // 'a.t' is unique again @@ -121,7 +122,7 @@ The uniqueness annotations that have been introduced can bring several benefits === Formal Verification -The main goal of introducing the concept of uniqueness in Kotlin is to enable the verification of interesting functional properties. For instance, formalists might be interested in proving the absence of `IndexOutOfBoundsException` in a function. However, the lack of aliasing guarantees within a concurrent context in Kotlin can complicate such proofs @KotlinDocsConcurrency, even for relatively simple functions like the one shown in @out-of-bound. In this example, the following scenario could potentially lead to an `IndexOutOfBoundsException`: +The main goal of introducing the concept of uniqueness in Kotlin is to enable the verification of interesting functional properties. For example, it might be interesting to prove the absence of `IndexOutOfBoundsException` in a function. However, the lack of aliasing guarantees within a concurrent context in Kotlin can complicate such proofs @KotlinDocsConcurrency, even for relatively simple functions like the one shown in @out-of-bound. In this example, the following scenario could potentially lead to an `IndexOutOfBoundsException`: - The function executes `xs.add(x)`, adding an element to the list `xs`. - Concurrently, another function with access to an alias of `xs` invokes the `clear` method, emptying the list. - Subsequently, `xs[0]` is called on the now-empty list, raising an `IndexOutOfBoundsException`. @@ -144,7 +145,7 @@ This characteristic aligns well with Viper's notion of write access. In Viper, w As introduced in @cap:smart-cast, smart casts are an important feature in Kotlin that allow developers to avoid using explicit cast operators under certain conditions. However, the compiler can only perform a smart cast if it can guarantee that the cast will always be safe @KotlinSpec. This guarantee relies on the concept of stability: a variable is considered stable if it cannot change after being checked, allowing the compiler to safely assume its type throughout a block of code. -Since Kotlin is a concurrent language, the compiler cannot perform smart casts when dealing with mutable properties. The reason is that after checking the type of a mutable property, another function running concurrently may access the same reference and change its value. @smart-cast-error, shows that after checking that `a.valProperty` is not `null`, the compiler can smart cast it from `Int?` to `Int`. However, the same operation is not possible for `a.varProperty` because, immediately after checking that it is not `null`, another function running concurrently might set it to `null`. +Since Kotlin allows for concurrent execution, the compiler cannot perform smart casts when dealing with mutable properties. The reason is that after checking the type of a mutable property, another function running concurrently may access the same reference and change its value. @smart-cast-error, shows that after checking that `a.valProperty` is not `null`, the compiler can smart cast it from `Int?` to `Int`. However, the same operation is not possible for `a.varProperty` because, immediately after checking that it is not `null`, another function running concurrently might set it to `null`. Guarantees on the uniqueness of references can enable the compiler to perform more exhaustive analysis for smart casts. When a reference is unique, the uniqueness system ensures that there are no accessible aliases to that reference, meaning it is impossible for a concurrently running function to modify its value. @smart-cast-unique shows the same example as before, but with the function parameter being unique. Since `a` is unique, it is completely safe to smart cast `a.varProperty` from `Int?` to `Int` after verifying that it is not null. #figure( diff --git a/chapters/5-Annotation-System.typ b/chapters/5-Annotation-System.typ index 22d2114..93706ad 100644 --- a/chapters/5-Annotation-System.typ +++ b/chapters/5-Annotation-System.typ @@ -13,7 +13,7 @@ This chapter formalizes the uniqueness system that was introduced in @cap:annota While inspired by prior works @aldrich2002alias @boyland2001alias @zimmerman2023latte, it introduces several significant improvements. This system is designed for being as lightweight as possible and gradually integrable with already existing Kotlin code. -The main goal of the system is to improve the verification process with Viper by establishing a link between separation logic and the absence of aliasing control in Kotlin. +The main goal of the system is to improve SnaKt's verification process by adding aliasing control to Kotlin, thereby establishing a connection to separation logic in Viper. == Grammar @@ -81,7 +81,7 @@ A context is a list of distinct paths associated with their annotations $alpha$ #v(1em) Apart from $top$, the rest of the annotations are similar to the annotations in the previous section. -A reference annotated as unique may either be `null` or point to an object, with no other accessible references to that object. In contrast, a reference marked as shared can point to an object without being the only reference to it. The annotation borrowed indicates that the method receiving the reference will not create additional aliases to it, and upon returning, the fields of the object will have at least the permissions specified in the class declaration. Finally, annotations on fields only indicate the default permissions; to determine the actual permissions of a field, the context must be considered, a concept that will be formalized in the upcoming sections. +A reference annotated as unique may either be `null` or point to an object, with no other accessible references to that object. In contrast, a reference marked as shared can point to an object without being the only reference to it. The annotation $borrowed$ (borrowed) indicates that the method receiving the reference will not create additional aliases to it, and upon returning, the fields of the object will have at least the permissions specified in the class declaration. Finally, annotations on fields only indicate the default permissions; to determine the actual permissions of a field, the context must be considered, a concept that will be formalized in the upcoming sections. == Well-Formed Context @@ -107,7 +107,7 @@ This first set of rules defines how a well-formed context is structured. The jud The judgment "$Delta_1 ctx$" is derivable meaning that $Delta_1$ is a well-formed context. However, the judgments "$Delta_2 ctx$" and "$Delta_3 ctx$" are not derivable meaning that $Delta_2$ and $Delta_3$ are not well-formed contexts. Indeed, they are not well-formed because $x$ appears twice in $Delta_2$ and $x.f$ appears twice in $Delta_3$. ] -== Sub-Paths and Sup-Paths +== Sub-Paths and Super-Paths === Definition @@ -116,13 +116,13 @@ This first set of rules defines how a well-formed context is structured. The jud SubPath-Eq-1, SubPath-Eq-2, ) -This set of rules is used to formally define sub-paths and sup-paths. +This set of rules is used to formally define sub-paths and super-paths. #example[ Given two paths $x.y$ and $x.y.z$, the following judgment is derivable: $ x.y subset.sq x.y.z $ We say that: - $x.y$ is a sub-path of $x.y.z$ - - $x.y.z$ is a sup-path of $x.y$ + - $x.y.z$ is a super-path of $x.y$ ] === Remove @@ -146,12 +146,12 @@ Basically, the function will return the context without the specified path if th === Deep Remove #display-rules( - Remove-SupPathsEq-Empty, "", - Remove-SupPathsEq-Discard, "", - Remove-SupPathsEq-Keep, "", + Remove-SuperPathsEq-Empty, "", + Remove-SuperPathsEq-Discard, "", + Remove-SuperPathsEq-Keep, "", ) -Deep-Remove rules define a function similar to Remove ($without$) that in addiction to removing the given path from the context, also removes all the sup-paths of that path. +Deep-Remove rules define a function similar to Remove ($without$) that in addiction to removing the given path from the context, also removes all the super-paths of that path. $ \_minus.circle\_: Delta -> p -> Delta $ @@ -166,7 +166,7 @@ $ \_minus.circle\_: Delta -> p -> Delta $ Replace, "", ) -This rule gives the definition of a function that will be fundamental for typing statements. The function takes a context, a path $p$ and a set of annotations $alpha beta$ and returns a context in which all the sup-paths of $p$ have been removed and the annotation of $p$ becomes $alpha beta$. +This rule gives the definition of a function that will be fundamental for typing statements. The function takes a context, a path $p$ and a set of annotations $alpha beta$ and returns a context in which all the super-paths of $p$ have been removed and the annotation of $p$ becomes $alpha beta$. $ \_[\_|->\_] : Delta -> p -> alpha beta -> Delta $ @@ -175,21 +175,21 @@ $ \_[\_|->\_] : Delta -> p -> alpha beta -> Delta $ Replace has the following result: $ Delta[x.y |-> top] = x: unique, space x.y: top $ ] -=== Get Sup-Paths +=== Get Super-Paths #display-rules( - Get-SupPaths-Empty, "", - Get-SupPaths-Discard, "", - Get-SupPaths-Keep, "", + Get-SuperPaths-Empty, "", + Get-SuperPaths-Discard, "", + Get-SuperPaths-Keep, "", ) -Finally, Get-Sup-Paths rules are used to define a function that returns all the sup-paths of a give path within a context. Also this function will be used for statements typing rules. +Finally, Get-Super-Paths rules are used to define a function that returns all the super-paths of a give path within a context. Also this function will be used for statements typing rules. $ \_ tr sp(\_) : Delta -> p -> overline(p : alpha beta) $ #example[ Given a context: $ Delta = x: unique, space x.y: unique, space x.y.z: unique $ - Getting sup-paths has the following result: $ sp(x.y) = x.y.z: unique $ + Getting super-paths has the following result: $ sp(x.y) = x.y.z: unique $ ] == Relations between Annotations @@ -313,9 +313,9 @@ Furthermore, in the rule Get-Path, the premise $Delta inangle(p.f) = alpha'$ doe Std-Rec-2, "", ) -If the judgment $Delta tr std(p, alpha beta)$ is derivable, inside the context $Delta$, all the sup-paths of $p$ carry the right annotations when $p$ is passed to a method expecting an argument annotated with $alpha beta$. This type of judgment is necessary verify the correctness of the annotations in a method-modular fashion. +If the judgment $Delta tr std(p, alpha beta)$ is derivable, inside the context $Delta$, all the super-paths of $p$ carry the right annotations when $p$ is passed to a method expecting an argument annotated with $alpha beta$. This type of judgment is necessary verify the correctness of the annotations in a method-modular fashion. -Since a called method does not have information about $Delta$ when verified, all the sup-paths of $p$ must have an annotation in $Delta$ that is lower or equal ($rel$) to the annotation that they have in a context containing just their root annotated with $alpha beta$. +Since a called method does not have information about $Delta$ when verified, all the super-paths of $p$ must have an annotation in $Delta$ that is lower or equal ($rel$) to the annotation that they have in a context containing just their root annotated with $alpha beta$. #example[ Given the following program: @@ -487,7 +487,7 @@ Typing a method call follows the logic presented in the rules of @cap:passing ($ - $p_j$ is shared. - The method that has been called expects shared (possibly borrowed) arguments in positions $i$ and $j$. - The resulting context is constructed in the following way: - - Paths passed to the method and their sup-paths are removed from the initial context. + - Paths passed to the method and their super-paths are removed from the initial context. - A list of annotated paths (in which a the same path may appear twice) in constructed by mapping passed paths according to the "passing" ($~>$) rules. - The obtained list is normalized and added to the context. @@ -525,7 +525,7 @@ Finally @call-sup-ok-2 shows that it is possible to call `h` by passing `x` and ) #figure( - caption: "Typing example for correct method call with sup-references", + caption: "Typing example for correct method call with super-paths", ``` class A(f: shared) @@ -543,7 +543,7 @@ Finally @call-sup-ok-2 shows that it is possible to call `h` by passing `x` and ) #figure( - caption: "Typing example for incorrect method call with sup-references", + caption: "Typing example for incorrect method call with super-paths", ``` class B(f: unique) @@ -560,7 +560,7 @@ Finally @call-sup-ok-2 shows that it is possible to call `h` by passing `x` and ) #figure( - caption: "Typing example for correct method call with sup-references", + caption: "Typing example for correct method call with super-paths", ``` class B(f: unique) @@ -584,7 +584,7 @@ All rules for typing assignments have a path $p$ on the left-hand side and vary #display-rules(Assign-Null, "") -The definition of unique tells us that a reference is unique when it is `null` or is the sole accessible reference pointing to the object that is pointing. Given that, we can safely consider unique a path $p$ after assigning `null` to it. Moreover, all sup-paths of $p$ are removed from the context after the assignment. +The definition of unique tells us that a reference is unique when it is `null` or is the sole accessible reference pointing to the object that is pointing. Given that, we can safely consider unique a path $p$ after assigning `null` to it. Moreover, all super-paths of $p$ are removed from the context after the assignment. #figure( caption: "Typing example for assigning null", @@ -738,7 +738,7 @@ consume_unique(c: unique): shared consume_shared(a: shared): shared -fun f(@Unique a: A, @Borrowed c: C) { +fun f(a: unique, c: shared ♭) { begin_f; ⊣ Δ = a: unique, t: shared ♭ if (a.c == c) { diff --git a/config/utils.typ b/config/utils.typ index ae7c81c..a995b7d 100644 --- a/config/utils.typ +++ b/config/utils.typ @@ -24,7 +24,7 @@ #let mtype = "m-type" #let ctx = "ctx" #let norm = "normalize" -#let sp = "supPaths" +#let sp = "superPaths" #let std = "std" #let loop = "while" #let do = "do" diff --git a/preface/copyright.typ b/preface/copyright.typ index 019c292..352028a 100644 --- a/preface/copyright.typ +++ b/preface/copyright.typ @@ -3,5 +3,5 @@ #set page(numbering: none) #align(left + bottom, [ - #text(myName): #text(style: "italic", myTitle.replace("\n","")), #text(myDegree), #sym.copyright #text(myTime) + #text(myName): #text(style: "italic", myTitle.replace("\n"," ")), #text(myDegree), #sym.copyright #text(myTime) ]) \ No newline at end of file diff --git a/vars/kt-to-vpr-examples.typ b/vars/kt-to-vpr-examples.typ index 710c9c2..4de11aa 100644 --- a/vars/kt-to-vpr-examples.typ +++ b/vars/kt-to-vpr-examples.typ @@ -375,9 +375,9 @@ m2(this: unique) : shared { m3( x1: unique, - x2: unique borrowed, + x2: unique ♭, x3: shared, - x4: shared borrowed + x4: shared ♭ ) { ... } diff --git a/vars/rules/base.typ b/vars/rules/base.typ index 814c09a..2f91eeb 100644 --- a/vars/rules/base.typ +++ b/vars/rules/base.typ @@ -119,18 +119,18 @@ rule(label: "Sub-Path-Eq-2", $p subset.sq.eq p'$), ) -#let Remove-SupPathsEq-Empty = prooftree( +#let Remove-SuperPathsEq-Empty = prooftree( axiom(""), rule(label: "Deep-Remove-Empty", $dot minus.circle p = dot$), ) -#let Remove-SupPathsEq-Discard = prooftree( +#let Remove-SuperPathsEq-Discard = prooftree( axiom($p subset.sq.eq p'$), axiom($Delta minus.circle p = Delta'$), rule(n:2, label: "Deep-Remove-Discard", $(p': alpha beta, Delta) minus.circle p = Delta'$), ) -#let Remove-SupPathsEq-Keep = prooftree( +#let Remove-SuperPathsEq-Keep = prooftree( axiom($p subset.not.sq.eq p'$), axiom($Delta minus.circle p = Delta'$), rule(n:2, label: "Deep-Remove-Keep", $(p': alpha beta, Delta) minus.circle p = (p': alpha beta, Delta')$), @@ -141,21 +141,21 @@ rule(label: "Replace", $Delta[p |-> alpha beta] = Delta', p: alpha beta$), ) -#let Get-SupPaths-Empty = prooftree( +#let Get-SuperPaths-Empty = prooftree( axiom(""), - rule(label: "Get-Sup-Paths-Empty", $dot tr sp(p) = dot$), + rule(label: "Get-Super-Paths-Empty", $dot tr sp(p) = dot$), ) -#let Get-SupPaths-Discard = prooftree( +#let Get-SuperPaths-Discard = prooftree( axiom($not (p subset.sq p')$), axiom($Delta tr sp(p) = p_0 : alpha_0 beta_0, ..., p_n : alpha_n beta_n$), - rule(n: 2, label: "Get-Sup-Paths-Discard", $p': alpha beta, Delta tr sp(p) = p_0 : alpha_0 beta_0, ..., p_n : alpha_n beta_n$), + rule(n: 2, label: "Get-Super-Paths-Discard", $p': alpha beta, Delta tr sp(p) = p_0 : alpha_0 beta_0, ..., p_n : alpha_n beta_n$), ) -#let Get-SupPaths-Keep = prooftree( +#let Get-SuperPaths-Keep = prooftree( axiom($p subset.sq p'$), axiom($Delta tr sp(p) = p_0 : alpha_0 beta_0, ..., p_n : alpha_n beta_n$), - rule(n: 2, label: "Get-Sup-Paths-Keep", $p': alpha beta, Delta tr sp(p) = p': alpha beta, p_0 : alpha_0 beta_0, ..., p_n : alpha_n beta_n$), + rule(n: 2, label: "Get-Super-Paths-Keep", $p': alpha beta, Delta tr sp(p) = p': alpha beta, p_0 : alpha_0 beta_0, ..., p_n : alpha_n beta_n$), ) // ************ Get ************