Skip to content

Commit 7204b7e

Browse files
committed
add sample to Java25 category
1 parent b4e73f3 commit 7204b7e

4 files changed

Lines changed: 51 additions & 0 deletions

File tree

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
example.name = Try With Resources
2+
example.path = Java 25
3+
example.file = project.key
4+
example.additionalFile.1 = TryWithResources.java
5+
6+
Try-With-Resources statements are supported in KeY. They are reduced to nested try/finally blocks with proper exception suppression handling.
7+
8+
The proof obligation is verifiable without user interaction.
Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
public final class TryWithResources {
2+
/*@ ensures true; requires true; */
3+
public void m() throws Exception {
4+
// Simple try-with-resources
5+
try (Resource r = new Resource()) {
6+
r.use();
7+
}
8+
9+
// Multiple resources
10+
try (Resource r1 = new Resource(); Resource r2 = new Resource()) {
11+
r1.use();
12+
r2.use();
13+
}
14+
15+
// Java 9+ style with existing variable
16+
Resource existing = new Resource();
17+
try (existing) {
18+
existing.use();
19+
}
20+
}
21+
22+
static class Resource implements AutoCloseable {
23+
/*@ ensures true; requires true; */
24+
public void use() {
25+
// use the resource
26+
}
27+
28+
/*@ ensures true; requires true; */
29+
@Override
30+
public void close() throws Exception {
31+
// close the resource
32+
}
33+
}
34+
}
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
\profile "Java Profile";
2+
\javaSource ".";
3+
4+
\proofObligation {
5+
"class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO",
6+
"contract" : "TryWithResources[TryWithResources::m()].JML operation contract.0",
7+
"name" : "TryWithResources[TryWithResources::m()].JML operation contract.0"
8+
}

key.ui/examples/index/samplesIndex.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ Java/MultiCatch/README.txt
2525
Java/Records/README.txt
2626
Java/Records+CompactConstructor/README.txt
2727
Java/TextBlockLiterals/README.txt
28+
Java/TryWithResources/README.txt
2829

2930
# The KeY Book (note: the comments here are only for maintainability, if you want to move an entry to a different section, look into the individual txt file!)
3031
## Chapter 15 - Using the KeY Prover

0 commit comments

Comments
 (0)