Skip to content

Commit ba4c8d9

Browse files
rcosta358rcosta358
committed
Add Example Pages
1 parent 4904119 commit ba4c8d9

File tree

10 files changed

+384
-14
lines changed

10 files changed

+384
-14
lines changed

‎pages/concepts/state-refinements.md‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -18,13 +18,13 @@ import liquidjava.specification.*;
1818

1919
@StateSet({"open", "closed"})
2020
public class File {
21-
@StateRefinement(to = "open()")
21+
@StateRefinement(to="open()")
2222
public File() {}
2323

24-
@StateRefinement(from = "open()")
24+
@StateRefinement(from="open()")
2525
public void read() {}
2626

27-
@StateRefinement(from = "open()", to = "closed()")
27+
@StateRefinement(from="open()", to="closed()")
2828
public void close() {}
2929
}
3030
```

‎pages/examples.md‎

Lines changed: 0 additions & 11 deletions
This file was deleted.

‎pages/examples/arraylist.md‎

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
---
2+
title: ArrayList
3+
parent: Examples
4+
nav_order: 7
5+
permalink: /examples/arraylist/
6+
description: An external refinement for ArrayList that prevents out-of-bounds access.
7+
---
8+
9+
# ArrayList
10+
11+
This example refines the `java.util.ArrayList` standard-library class without modifying its source code. A ghost variable tracks the size of the list, and method refinements to prevent out-of-bounds accesses.
12+
13+
```java
14+
import liquidjava.specification.*;
15+
16+
@ExternalRefinementsFor("java.util.ArrayList")
17+
@Ghost("int size")
18+
public interface ArrayListRefinements<E> {
19+
public void ArrayList();
20+
21+
@StateRefinement(to="size() == size(old(this)) + 1")
22+
public boolean add(E elem);
23+
24+
public E get(@Refinement("_ < size()") int index);
25+
}
26+
```
27+
28+
```java
29+
ArrayList<Integer> list = new ArrayList<>();
30+
list.add(1);
31+
list.get(0);
32+
list.get(1); // type error!
33+
```
34+
35+
The key idea is that LiquidJava turns the usual runtime condition for `get(i)` into a static precondition over the tracked `size` ghost variable.

‎pages/examples/counter.md‎

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
---
2+
title: Counter
3+
parent: Examples
4+
nav_order: 1
5+
permalink: /examples/counter/
6+
description: A small refinement example for exact method postconditions and safe decrementing.
7+
---
8+
9+
# Counter
10+
11+
This example uses plain refinements on method parameters and return values to ensure a counter never decrements below zero.
12+
13+
```java
14+
import liquidjava.specification.Refinement;
15+
16+
public class Counter {
17+
@Refinement("_ == count + 1")
18+
public static int increment(@Refinement("count >= 0") int count) {
19+
return count + 1;
20+
}
21+
22+
@Refinement("_ == count - 1")
23+
public static int decrement(@Refinement("count > 0") int count) {
24+
return count - 1;
25+
}
26+
}
27+
```
28+
29+
```java
30+
int c = 0;
31+
c = Counter.increment(c);
32+
c = Counter.decrement(c);
33+
c = Counter.decrement(c); // type error!
34+
```
35+
36+
The parameter refinement on `decrement` requires the input to be strictly positive, so LiquidJava rejects the final call when `c` is already `0`.

‎pages/examples/downloader.md‎

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
---
2+
title: Downloader
3+
parent: Examples
4+
nav_order: 5
5+
permalink: /examples/downloader/
6+
description: A typestate protocol for a downloader object.
7+
---
8+
9+
# Downloader
10+
11+
This example models a simple downloader object that tracks the progress of a download operation by combining typestates and ghost variables.
12+
13+
```java
14+
@Ghost("int progress")
15+
@StateSet({"created", "downloading", "completed"})
16+
public class Downloader {
17+
@StateRefinement(to="created(this) && progress(this) == 0")
18+
public Downloader() {}
19+
20+
@StateRefinement(from="created(this) && progress(this) == 0", to="downloading(this) && progress(this) == 0")
21+
public void start() {}
22+
23+
@StateRefinement(from="downloading(this)", to="downloading(this) && progress(this) == percentage")
24+
public void update(@Refinement("percentage > progress(this)") int percentage) {}
25+
26+
@StateRefinement(from="downloading(this) && progress(this) == 100", to="completed(this)")
27+
public void finish() {}
28+
}
29+
```
30+
31+
```java
32+
Downloader d = new Downloader();
33+
d.start();
34+
d.update(50);
35+
d.update(100);
36+
d.finish();
37+
```
38+
39+
```java
40+
Downloader d = new Downloader();
41+
d.start();
42+
d.update(50);
43+
d.finish(); // type error!
44+
```

‎pages/examples/email.md‎

Lines changed: 85 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,85 @@
1+
---
2+
title: Email
3+
parent: Examples
4+
nav_order: 3
5+
permalink: /examples/email/
6+
description: A typestate protocol for a Email builder API.
7+
---
8+
9+
# Email
10+
11+
This example models a builder-style API where methods must be called in a specific order to create a valid `Email` object.
12+
13+
```java
14+
import java.util.ArrayList;
15+
import java.util.List;
16+
import liquidjava.specification.*;
17+
18+
@StateSet({"empty", "senderSet", "receiverSet", "bodySet"})
19+
public class Email {
20+
private String sender;
21+
private List<String> receiver;
22+
private String subject;
23+
private String body;
24+
25+
@StateRefinement(to="empty()")
26+
public Email() {
27+
receiver = new ArrayList<>();
28+
}
29+
30+
@StateRefinement(from="empty()", to="senderSet()")
31+
public void from(String s) {
32+
sender = s;
33+
}
34+
35+
@StateRefinement(from="senderSet() || receiverSet()", to="receiverSet()")
36+
public void to(String s) {
37+
receiver.add(s);
38+
}
39+
40+
@StateRefinement(from="receiverSet()", to="receiverSet()")
41+
public void subject(String s) {
42+
subject = s;
43+
}
44+
45+
@StateRefinement(from="receiverSet()", to="bodySet()")
46+
public void body(String s) {
47+
body = s;
48+
}
49+
50+
@StateRefinement(from="bodySet()", to="bodySet()")
51+
public String build() {
52+
StringBuilder sb = new StringBuilder();
53+
sb.append("From: " + sender + "\n");
54+
sb.append("To: " + String.join(", ", receiver) + "\n");
55+
sb.append("Subject: " + subject + "\n");
56+
sb.append("\n");
57+
sb.append(body);
58+
return sb.toString();
59+
}
60+
}
61+
```
62+
63+
```java
64+
Email email = new Email();
65+
email.from("me");
66+
.to("bob");
67+
.to("alice");
68+
.subject("greetings");
69+
.body("hello!");
70+
.build();
71+
```
72+
73+
```java
74+
Email email = new Email();
75+
email.from("me");
76+
.to("bob");
77+
.build(); // type error!
78+
```
79+
80+
LiquidJava enforces the intended protocol:
81+
82+
- The `from` must be set first
83+
- The `to` must be set at least once before setting the `body`
84+
- The `subject` is optional
85+
- The `build` is only allowed to be set after the body

‎pages/examples/index.md‎

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
---
2+
title: Examples
3+
nav_order: 6
4+
has_children: true
5+
permalink: /examples/
6+
description: LiquidJava example usages with focused code snippets.
7+
has_toc: false
8+
cards:
9+
- title: Counter
10+
url: /examples/counter/
11+
description: A small refinement example for safely decrementing a counter without going below zero.
12+
- title: Media Player
13+
url: /examples/media-player/
14+
description: A typestate protocol for a simple media player with stopped, playing, and paused states.
15+
- title: Email
16+
url: /examples/email/
17+
description: A typestate protocol for a Email builder API.
18+
- title: Order
19+
url: /examples/order/
20+
description: A typestate protocol for a simple order processing system.
21+
- title: Downloader
22+
url: /examples/downloader/
23+
description: A typestate protocol for a downloader object.
24+
- title: ReentrantLock
25+
url: /examples/reentrant-lock/
26+
description: An external typestate refinement for java.util.concurrent.locks.ReentrantLock.
27+
- title: ArrayList
28+
url: /examples/arraylist/
29+
description: An external refinement for java.util.ArrayList that statically prevents out-of-bounds accesses.
30+
---
31+
32+
# Examples
33+
34+
In this section you can explore various example usages of LiquidJava, with focused code snippets to illustrate specific features and use cases.
35+
36+
{% include card_grid.html cards=page.cards %}

‎pages/examples/media-player.md‎

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
---
2+
title: Media Player
3+
parent: Examples
4+
nav_order: 2
5+
permalink: /examples/media-player/
6+
description: A typestate protocol for a simple media player with stopped, playing, and paused states.
7+
---
8+
9+
# Media Player
10+
11+
This example models a small object protocol with three states and transitions that describe when playback actions are allowed.
12+
13+
```java
14+
import liquidjava.specification.*;
15+
16+
@StateSet({"stopped", "playing", "paused"})
17+
public class MediaPlayer {
18+
@StateRefinement(to="stopped()")
19+
public MediaPlayer() {}
20+
21+
@StateRefinement(from="stopped()", to="playing()")
22+
public void play() {}
23+
24+
@StateRefinement(from="playing()", to="paused()")
25+
public void pause() {}
26+
27+
@StateRefinement(from="paused()", to="playing()")
28+
public void resume() {}
29+
30+
@StateRefinement(from="!stopped()", to="stopped()")
31+
public void stop() {}
32+
}
33+
```
34+
35+
```java
36+
MediaPlayer player = new MediaPlayer();
37+
player.play();
38+
player.pause();
39+
player.resume();
40+
player.stop();
41+
player.resume(); // type error!
42+
```
43+
44+
Because `resume` is only valid from `paused()`, the final call is rejected after `stop()` puts the object back in `stopped()`.

‎pages/examples/order.md‎

Lines changed: 61 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,61 @@
1+
---
2+
title: Order
3+
parent: Examples
4+
nav_order: 4
5+
permalink: /examples/order/
6+
description: A typestate protocol for a simple order processing system.
7+
---
8+
9+
# Order
10+
11+
This example shows a more expressive protocol that combines typestates, ghost variables, and value-dependent conditions.
12+
13+
```java
14+
import liquidjava.specification.*;
15+
16+
@StateSet({"ordering", "checkout", "finished"})
17+
@Ghost("int total")
18+
public class Order {
19+
@StateRefinement(to="ordering() && total() == 0")
20+
public Order() {}
21+
22+
@StateRefinement(from="ordering()", to="ordering() && total() == total(old(this)) + price")
23+
@Refinement("_ == this")
24+
public Order addItem(String name, @Refinement("_ > 0") int price) {
25+
return this;
26+
}
27+
28+
@StateRefinement(from="ordering() && total() > 0", to="checkout() && total() == total(old(this))")
29+
@Refinement("_ == this")
30+
public Order checkout() {
31+
return this;
32+
}
33+
34+
@StateRefinement(from="checkout() && amount == total()", to="finished()")
35+
@Refinement("_ == this")
36+
public Order pay(@Refinement("_ > 0") int amount) {
37+
return this;
38+
}
39+
}
40+
```
41+
42+
```java
43+
Order order = new Order();
44+
order.addItem("shirt", 60)
45+
.addItem("shoes", 80)
46+
.checkout()
47+
.pay(140);
48+
```
49+
50+
```java
51+
Order order = new Order();
52+
order.addItem("shirt", 60)
53+
.addItem("shoes", 80)
54+
.checkout()
55+
.pay(120); // type error!
56+
```
57+
58+
This example enforces the intended protocol:
59+
- Items can only be added in the `ordering` state, and the total is updated accordingly
60+
- The `checkout` can only be called after at least one item has been added, and the total must remain the same
61+
- The `pay` can only be called after checkout, and the amount must match the total order value

0 commit comments

Comments
 (0)