diff --git a/appendix/full-rules-set.typ b/appendix/full-rules-set.typ index a85e9e7..74d114f 100644 --- a/appendix/full-rules-set.typ +++ b/appendix/full-rules-set.typ @@ -18,20 +18,20 @@ All the following rules are to be considered for a given program $P$, where fiel F-Type, "" ) -== Context - -=== Well-Formed Contexts +== Well-Formed Contexts #display-rules( Not-In-Base, Not-In-Rec, Ctx-Base, Ctx-Rec, ) -=== Lookup +== Sub-Paths and Sup-Paths + +=== Definition #display-rules( - Lookup-Base, Lookup-Rec, - Lookup-Default, "", + SubPath-Base, SubPath-Rec, + SubPath-Eq-1, SubPath-Eq-2, ) === Remove @@ -41,15 +41,6 @@ All the following rules are to be considered for a given program $P$, where fiel Remove-Rec, "", ) -== Sub-Paths and Sup-Paths - -=== Definition - -#display-rules( - SubPath-Base, SubPath-Rec, - SubPath-Eq-1, SubPath-Eq-2, -) - === Deep Remove #display-rules( @@ -98,6 +89,13 @@ All the following rules are to be considered for a given program $P$, where fiel Root-Base, Root-Rec, ) +=== Lookup + +#display-rules( + Lookup-Base, Lookup-Rec, + Lookup-Default, "", +) + === Get #display-rules( @@ -146,13 +144,13 @@ All the following rules are to be considered for a given program $P$, where fiel #display-rules( Begin, "", - Decl, Assign-Null, - Seq-New, "", + Seq-New, Decl, + Call, "", + Assign-Null, "", + Assign-Call, "", Assign-Unique, "", Assign-Shared, "", Assign-Borrowed-Field, "", - Assign-Call, "", - Call, "", If, "", Return-p, "", ) diff --git a/chapters/5-Annotation-System.typ b/chapters/5-Annotation-System.typ index e0d5a7e..19b8c78 100644 --- a/chapters/5-Annotation-System.typ +++ b/chapters/5-Annotation-System.typ @@ -82,7 +82,7 @@ A context is a list of distinct paths associated with their annotations $alpha$ 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. -=== Well-Formed Context +== Well-Formed Context #display-rules( Not-In-Base, Not-In-Rec, @@ -106,33 +106,6 @@ 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$. ] -=== Lookup - -#display-rules( - Lookup-Base, Lookup-Rec, - Lookup-Default, "", -) - -Lookup rules define a (partial) function that, given a well-formed context, returns the annotations associated with a given path - -When the path is explicitly contained within the context, the function returns the corresponding annotation. If a field access ($p.f$) is not explicitly present in the context, the function returns the annotations specified in the class declaration. This concept, formalized by Lookup-Default, is crucial as it ensures that contexts remain finite, even when handling recursive classes. However, if a variable ($x$) is not present in the context, its lookup cannot be derived. - -It is important to note that the lookup function returns the annotations associated with a path based on the context or the class declaration, rather than determining the actual ownership status of that path. - -$ \_inangle(\_): Delta -> p -> alpha beta $ - -#example[ - Given a context: $ Delta = x : shared, space x.f : unique $ - The result of the lookup for $x.f$ is the following: $ Delta inangle(x.f) = unique $ However, since $x$ is shared, there can be multiple references accessing $x$. This implies there can be multiple references accessing $x.f$, meaning that $x.f$ is also shared. - This behavior is intended and a function able to provide the actual ownership of a reference will be defined in the next sections. -] - -#example[ - Given class $C$, context $Delta$ and variable $x$ such that: $ class C(f: shared) in P \ Delta = x : unique \ type(x.f) = shared $ - The result of the lookup for $x.f$ is the following: $ Delta inangle(x.f) = shared $ - Since $x.f in.not Delta$, the lookup returns the default annotation, which is the one declared in the class signature. -] - == Sub-Paths and Sup-Paths === Definition @@ -262,6 +235,33 @@ $ root : p -> p $ $ root(x.y.z) = x \ root(y.z) = y \ root(z) = z $ ] +=== Lookup + +#display-rules( + Lookup-Base, Lookup-Rec, + Lookup-Default, "", +) + +Lookup rules define a (partial) function that, given a well-formed context, returns the annotations associated with a given path + +When the path is explicitly contained within the context, the function returns the corresponding annotation. If a field access ($p.f$) is not explicitly present in the context, the function returns the annotations specified in the class declaration. This concept, formalized by Lookup-Default, is crucial as it ensures that contexts remain finite, even when handling recursive classes. However, if a variable ($x$) is not present in the context, its lookup cannot be derived. + +It is important to note that the lookup function returns the annotations associated with a path based on the context or the class declaration, rather than determining the actual ownership status of that path. + +$ \_inangle(\_): Delta -> p -> alpha beta $ + +#example[ + Given a context: $ Delta = x : shared, space x.f : unique $ + The result of the lookup for $x.f$ is the following: $ Delta inangle(x.f) = unique $ However, since $x$ is shared, there can be multiple references accessing $x$. This implies there can be multiple references accessing $x.f$, meaning that $x.f$ is also shared. + This behavior is intentional, and a function that determines the actual ownership of a path is defined in the subsequent section. +] + +#example[ + Given class $C$, context $Delta$ and variable $x$ such that: $ class C(f: shared) in P \ Delta = x : unique \ type(x.f) = shared $ + The result of the lookup for $x.f$ is the following: $ Delta inangle(x.f) = shared $ + Since $x.f in.not Delta$, the lookup returns the default annotation, which is the one declared in the class signature. +] + === Get #display-rules(