From c843a867a2993bc13767b312373b094bbe53cbfd Mon Sep 17 00:00:00 2001 From: Jenny Xiang Date: Fri, 26 Apr 2024 12:05:25 -0700 Subject: [PATCH 1/2] Create some JavaExamples --- JavaExamples | 78 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 78 insertions(+) create mode 100644 JavaExamples diff --git a/JavaExamples b/JavaExamples new file mode 100644 index 0000000..c0259e3 --- /dev/null +++ b/JavaExamples @@ -0,0 +1,78 @@ +/// Java Examples + +// Mutating immut set, `s` is immut +void foo(Set s) { + Set new_s = s; + new_s.add("x"); // ERROR +} + +// Mutating immut set, `new_s` is immut +void foo(@Mutable Set s) { + Set new_s = new HashSet<>(s); + new_s.add("x"); // ERROR +} + +// Mutating mut set +void foo(Set s) { + @Mutable Set new_s = new HashSet<>(s); + new_s.add("x"); // OK +} + +// Type parameter mutability +void foo(Set> s, List l) { + assert s.get(l) != null; + List v = s.get(l); + l.add("x"); // ERROR + v.add("x"); // ERROR +} + +// Immut class and its members +class Person { + String name; + List family; + + Person(String n, List f) { + this.name = n; // OK + this.family = f; // OK + } + + void setName(String n) { + this.name = n; // ERROR + } + + @Mutable List getFamily() { + return family; // ERROR + } +} + +void foo(Person p) { + p.name = "Jenny"; // ERROR + p.family.add("Jenny"); // ERROR + p.family.getFamily().add("Jenny"); // OK +} + +// Mut class and its members +@Mutable class Person { + String name; + List family; + + Person(String n, List f) { + this.name = n; // OK + this.family = f; // OK + } + + void setName(String n) { + this.name = n; // OK + } + + List getFamily() { + return family; // OK + } +} + +void foo(Person p) { + p.name = "Jenny"; // OK + p.family.add("Jenny"); // OK + p.family.getFamily().add("Jenny"); // ERROR +} + From 70b3ff0f4cd737d3cbbf6c8fefe5759d3fa57953 Mon Sep 17 00:00:00 2001 From: Aosen Xiong <82676488+Ao-senXiong@users.noreply.github.com> Date: Fri, 26 Apr 2024 15:18:47 -0400 Subject: [PATCH 2/2] Add reference to previous thesis --- README.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/README.md b/README.md index ebe78de..27daf42 100644 --- a/README.md +++ b/README.md @@ -3,3 +3,8 @@ PICO is a type system that supports class level and object level immutability based on Checker Framework. + +### Reference +[Haifeng Shi: Context-Sensitive Optional Type Systems Meet Generics: A Uniform Treatment and Formalization](https://uwspace.uwaterloo.ca/handle/10012/20163)\ +[Lian Sun: An Immutability Type System for Classes and Objects: Improvements, Experiments, and Comparisons](https://uwspace.uwaterloo.ca/handle/10012/16882)\ +[Mier Ta: Context Sensitive Typechecking And Inference: Ownership And Immutability](https://uwspace.uwaterloo.ca/handle/10012/13185)