Skip to content

Commit b6c6621

Browse files
rcosta358codex
andcommitted
Add a ghost state tracking playground example
Co-authored-by: Codex <codex@openai.com>
1 parent 52af72b commit b6c6621

2 files changed

Lines changed: 22 additions & 0 deletions

File tree

‎playground/index.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ Run the LiquidJava verification directly in your browser. Edit an example and se
2121
<option value="bounds">Parameter bounds</option>
2222
<option value="alias">Refinement aliases</option>
2323
<option value="state">Object states</option>
24+
<option value="ghost">Ghost state tracking</option>
2425
</select>
2526
</div>
2627
<button id="lj-reset" type="button">Reset</button>

‎scripts/playground/examples.mjs‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -47,5 +47,26 @@ class Example {
4747
resource.read();
4848
}
4949
}
50+
`,
51+
ghost: `import liquidjava.specification.*;
52+
53+
@Ghost("int count")
54+
class Example {
55+
@StateRefinement(to="count(this) == 0")
56+
Example() {}
57+
58+
@StateRefinement(to="count(this) == count(old(this)) + 1")
59+
void increment() {}
60+
61+
@StateRefinement(from="count(this) > 0", to="count(this) == count(old(this)) - 1")
62+
void decrement() {}
63+
64+
static void demo() {
65+
Example counter = new Example();
66+
counter.increment();
67+
counter.decrement();
68+
counter.decrement();
69+
}
70+
}
5071
`
5172
};

0 commit comments

Comments
 (0)