Skip to content

Commit

Permalink
Remove outdated section about JavaDL in JML
Browse files Browse the repository at this point in the history
  • Loading branch information
FliegendeWurst committed Nov 4, 2023
1 parent 927ecb8 commit 6dd2d39
Showing 1 changed file with 0 additions and 29 deletions.
29 changes: 0 additions & 29 deletions docs/user/JavaDLinJML.md
Original file line number Diff line number Diff line change
@@ -1,11 +1,6 @@
# Embedding JavaDL expressions and functions into JML expressions

*Mattias Ulbrich, 2011-08-31*

: !!! danger

This page is only accurate for KeY 1.x.


Currently, JML is the standard specification for KeY (JML★ more
precisely). Though it is still possible to specify JavaDL-contracts in `.key`
Expand All @@ -18,30 +13,6 @@ in the code directly.

An extension of the parser provides us with this possibility now.

## DL expressions in JML

In JML declarative specifications (i.e., anywhere but in set statements), we can
write JavaDL expressions if they are embedded into `"(* *)"`. This notation is
JML-speak for a natural-language-constraint. We use it for JavaDL expressions.

This is helpful if syntactical concepts like binding function symbols,
new sorts, ... need to be mentioned in specifications.

Example:
```
class A {
int a;
int b;
/*@ invariant (* a = javaAddInt(b, 1) *); */
/*@ invariant a == (* javaAddInt(b, 1) *); */
/*@ invariant a == b + 1; */
}
```

All three invariants have identical meaning.


## Escaping JavaDL function symbol names

In all JML specifications (also in set statements), function symbols known in
Expand Down

0 comments on commit 6dd2d39

Please sign in to comment.