Repository navigation
Expand file tree
/
Copy pathexamples.mjs
More file actions
72 lines (60 loc) · 1.47 KB
/
Copy pathexamples.mjs
File metadata and controls
72 lines (60 loc) · 1.47 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
export const examples = {
positive: `import liquidjava.specification.*;
class Example {
void positiveNumbers() {
@Refinement("_ > 0")
int count = -1;
}
}
`,
bounds: `import liquidjava.specification.*;
class Example {
void setPercentage(@Refinement("_ >= 0 && _ <= 100") int percentage) {}
void demo() {
setPercentage(125);
}
}
`,
alias: `import liquidjava.specification.*;
@RefinementAlias("Positive(int x) { x > 0 }")
class Example {
void demo() {
@Refinement("Positive(_)")
int amount = 0;
}
}
`,
state: `import liquidjava.specification.*;
@StateSet({"open", "closed"})
class Example {
@StateRefinement(to="open(this)")
Example() {}
@StateRefinement(from="open(this)", to="closed(this)")
void close() {}
@StateRefinement(from="open(this)")
void read() {}
static void demo() {
Example resource = new Example();
resource.close();
resource.read();
}
}
`,
ghost: `import liquidjava.specification.*;
@Ghost("int count")
class Example {
@StateRefinement(to="count(this) == 0")
Example() {}
@StateRefinement(to="count(this) == count(old(this)) + 1")
void increment() {}
@StateRefinement(from="count(this) > 0", to="count(this) == count(old(this)) - 1")
void decrement() {}
static void demo() {
Example counter = new Example();
counter.increment();
counter.decrement();
counter.decrement();
}
}
`
};