From c843a867a2993bc13767b312373b094bbe53cbfd Mon Sep 17 00:00:00 2001 From: Jenny Xiang Date: Fri, 26 Apr 2024 12:05:25 -0700 Subject: [PATCH 1/5] 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 10a07e33a5505447acda8b0ccd7f10509462770a Mon Sep 17 00:00:00 2001 From: Jenny Xiang Date: Fri, 26 Apr 2024 12:20:27 -0700 Subject: [PATCH 2/5] Update JavaExamples with more examples --- JavaExamples => JavaExamples.java | 28 ++++++++++++++++------------ 1 file changed, 16 insertions(+), 12 deletions(-) rename JavaExamples => JavaExamples.java (70%) diff --git a/JavaExamples b/JavaExamples.java similarity index 70% rename from JavaExamples rename to JavaExamples.java index c0259e3..4c2ccaf 100644 --- a/JavaExamples +++ b/JavaExamples.java @@ -1,32 +1,35 @@ /// Java Examples +import java.util.*; +import qual.Mutable; // Mutating immut set, `s` is immut void foo(Set s) { Set new_s = s; + @Mutable Set new_s1 = s; // ERROR new_s.add("x"); // ERROR } // Mutating immut set, `new_s` is immut -void foo(@Mutable Set s) { +void foo1(@Mutable Set s) { Set new_s = new HashSet<>(s); new_s.add("x"); // ERROR } // Mutating mut set -void foo(Set s) { +void foo2(Set s) { @Mutable Set new_s = new HashSet<>(s); new_s.add("x"); // OK } // Type parameter mutability -void foo(Set> s, List l) { +void foo3(Set> s, List l) { assert s.get(l) != null; List v = s.get(l); - l.add("x"); // ERROR + @Mutable List v2 = s.get(l); // ERROR v.add("x"); // ERROR } -// Immut class and its members +// Class and its immut members class Person { String name; List family; @@ -34,6 +37,7 @@ class Person { Person(String n, List f) { this.name = n; // OK this.family = f; // OK + this.family.add("Mom"); // ERROR } void setName(String n) { @@ -45,20 +49,21 @@ void setName(String n) { } } -void foo(Person p) { +void foo4(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; +// Class and its mut members +class MutPerson { + @Mutable String name; + @Mutable List family; Person(String n, List f) { this.name = n; // OK this.family = f; // OK + this.family.add("Mom"); // OK } void setName(String n) { @@ -70,9 +75,8 @@ List getFamily() { } } -void foo(Person p) { +void foo5(MutPerson p) { p.name = "Jenny"; // OK p.family.add("Jenny"); // OK p.family.getFamily().add("Jenny"); // ERROR } - From 15c5406923cda51c0a87dbf84e22dfc984ace55e Mon Sep 17 00:00:00 2001 From: Jenny Xiang Date: Fri, 26 Apr 2024 12:24:50 -0700 Subject: [PATCH 3/5] Update JavaExamples.java --- JavaExamples.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/JavaExamples.java b/JavaExamples.java index 4c2ccaf..3babfd7 100644 --- a/JavaExamples.java +++ b/JavaExamples.java @@ -12,7 +12,9 @@ void foo(Set s) { // Mutating immut set, `new_s` is immut void foo1(@Mutable Set s) { Set new_s = new HashSet<>(s); + Set new_s1 = s; new_s.add("x"); // ERROR + new_s1.add("x"); //OK } // Mutating mut set From 0e26006c60b4ef0d1b8fd2fd28b1701a1fce911a Mon Sep 17 00:00:00 2001 From: Aosen Xiong <82676488+Ao-senXiong@users.noreply.github.com> Date: Mon, 29 Apr 2024 14:07:30 -0400 Subject: [PATCH 4/5] Update JavaExamples.java --- JavaExamples.java | 126 +++++++++++++++++++++++----------------------- 1 file changed, 64 insertions(+), 62 deletions(-) diff --git a/JavaExamples.java b/JavaExamples.java index 3babfd7..3a18640 100644 --- a/JavaExamples.java +++ b/JavaExamples.java @@ -1,84 +1,86 @@ /// Java Examples import java.util.*; +import qual.Immutable; import qual.Mutable; -// Mutating immut set, `s` is immut -void foo(Set s) { - Set new_s = s; - @Mutable Set new_s1 = s; // ERROR - new_s.add("x"); // ERROR -} +public class JavaExamples { + // Mutating immut set, `s` is immut + void foo(@Immutable Set s) { + Set new_s = s; // Flow sensitive will refine this to @Immutable + @Mutable Set new_s1 = s; // ERROR, type incompatible + new_s.add("x"); // ERROR + } -// Mutating immut set, `new_s` is immut -void foo1(@Mutable Set s) { - Set new_s = new HashSet<>(s); - Set new_s1 = s; - new_s.add("x"); // ERROR - new_s1.add("x"); //OK -} + // Mutating immut set, `new_s` is immut + void foo1(@Mutable Set s) { + @Immutable Set new_s = new @Immutable HashSet<>(s); + Set new_s1 = s; // Flow sensitive will refine this to @Mutable + new_s.add("x"); // ERROR + new_s1.add("x"); //OK + } -// Mutating mut set -void foo2(Set s) { - @Mutable Set new_s = new HashSet<>(s); - new_s.add("x"); // OK -} + // Mutating mut set + void foo2(Set s) { + @Mutable Set new_s = new HashSet<>(s); + new_s.add("x"); // OK + } + + // Type parameter mutability + void foo3(Set> s, List l) { + assert s.get(l) != null; + List v = s.get(l); + @Mutable List v2 = s.get(l); // ERROR + v.add("x"); // ERROR + } + + void foo4(Person p) { + p.name = "Jenny"; // ERROR, this should be forbid by compiler by adding final before String + p.family.add("Jenny"); // ERROR, can not mutate immut list + } -// Type parameter mutability -void foo3(Set> s, List l) { - assert s.get(l) != null; - List v = s.get(l); - @Mutable List v2 = s.get(l); // ERROR - v.add("x"); // ERROR + void foo5(MutPerson p) { + p.name = "Jenny"; // OK + p.family.add("Jenny"); // OK + p.getFamily().add("Jenny"); // OK + } } // Class and its immut members class Person { - String name; - List family; + String name; // String is default @Immutable, use final to prevent reassignment + @Immutable List family; - Person(String n, List f) { - this.name = n; // OK - this.family = f; // OK - this.family.add("Mom"); // ERROR - } + Person(String n, @Immutable List f) { + this.name = n; // OK + this.family = f; // OK + this.family.add("Mom"); // ERROR + } - void setName(String n) { - this.name = n; // ERROR - } + void setName(String n) { + this.name = n; // ERROR, this should be forbid by compiler by adding final before String + } - @Mutable List getFamily() { - return family; // ERROR - } -} - -void foo4(Person p) { - p.name = "Jenny"; // ERROR - p.family.add("Jenny"); // ERROR - p.family.getFamily().add("Jenny"); // OK + @Mutable List getFamily() { + return family; // ERROR, type incompatible + } } // Class and its mut members class MutPerson { - @Mutable String name; - @Mutable List family; + String name; // String is default @Immutable in PICO + @Mutable List family; - Person(String n, List f) { - this.name = n; // OK - this.family = f; // OK - this.family.add("Mom"); // OK - } + MutPerson(String n, List f) { + this.name = n; // OK + this.family = f; // OK + this.family.add("Mom"); // OK + } - void setName(String n) { - this.name = n; // OK - } - - List getFamily() { - return family; // OK - } -} + void setName(String n) { + this.name = n; // OK + } -void foo5(MutPerson p) { - p.name = "Jenny"; // OK - p.family.add("Jenny"); // OK - p.family.getFamily().add("Jenny"); // ERROR + List getFamily() { + return family; // OK + } } From 05471c513025161f2a061645995ba013bf6225cd Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Tue, 7 May 2024 20:59:07 -0400 Subject: [PATCH 5/5] Refine the example and add generics example --- JavaExamples.java | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/JavaExamples.java b/JavaExamples.java index 3a18640..845ded3 100644 --- a/JavaExamples.java +++ b/JavaExamples.java @@ -25,16 +25,14 @@ void foo2(Set s) { new_s.add("x"); // OK } - // Type parameter mutability - void foo3(Set> s, List l) { - assert s.get(l) != null; + void foo3(List<@Immutable List> s, int l) { List v = s.get(l); @Mutable List v2 = s.get(l); // ERROR v.add("x"); // ERROR } void foo4(Person p) { - p.name = "Jenny"; // ERROR, this should be forbid by compiler by adding final before String + p.name = "Jenny"; // Ok, this should be forbid by compiler by adding final before String p.family.add("Jenny"); // ERROR, can not mutate immut list } @@ -57,7 +55,7 @@ class Person { } void setName(String n) { - this.name = n; // ERROR, this should be forbid by compiler by adding final before String + this.name = n; // Ok, this should be forbid by compiler by adding final before String } @Mutable List getFamily() { @@ -84,3 +82,12 @@ List getFamily() { return family; // OK } } + +class ImmutSet { + void foo1 (ImmutSet> s) { // ERROR + } + void foo2(MutList> s) { // OK + } +} + +@Mutable class MutList<@Mutable T> {}