Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add reference to previous thesis #44

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
78 changes: 78 additions & 0 deletions JavaExamples
Original file line number Diff line number Diff line change
@@ -0,0 +1,78 @@
/// Java Examples

// Mutating immut set, `s` is immut
void foo(Set<String> s) {
Set<String> new_s = s;
new_s.add("x"); // ERROR
}

// Mutating immut set, `new_s` is immut
void foo(@Mutable Set<String> s) {
Set<String> new_s = new HashSet<>(s);
new_s.add("x"); // ERROR
}

// Mutating mut set
void foo(Set<String> s) {
@Mutable Set<String> new_s = new HashSet<>(s);
new_s.add("x"); // OK
}

// Type parameter mutability
void foo(Set<List<String>> s, List<String> l) {
assert s.get(l) != null;
List<String> v = s.get(l);
l.add("x"); // ERROR
v.add("x"); // ERROR
}

// Immut class and its members
class Person {
String name;
List<String> family;

Person(String n, List<String> f) {
this.name = n; // OK
this.family = f; // OK
}

void setName(String n) {
this.name = n; // ERROR
}

@Mutable List<String> 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<String> family;

Person(String n, List<String> f) {
this.name = n; // OK
this.family = f; // OK
}

void setName(String n) {
this.name = n; // OK
}

List<String> getFamily() {
return family; // OK
}
}

void foo(Person p) {
p.name = "Jenny"; // OK
p.family.add("Jenny"); // OK
p.family.getFamily().add("Jenny"); // ERROR
}

5 changes: 5 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Loading