Please describe your proposal in a ONE sentence
Parametric Type Declarations (\dl_Set<[String]>) are not possible in ghost state declarations.
Underlying problem
When creating the logic abstraction of a class,
one should be able to use the new parametric types.
When we have complex parametric types (with more, recursive definitions),
it makes sense to use the alias definition.
However, for simple sorts, like Set<[String]>, Set<[Int]>, List<[Int]>,… it would be great,
to just be able to define them when declaring a field of such type.
If one wants to read the code later and stumbles across such a alias definition,
one has to look up the definition in a different file
which is quite some effort for just a simple type definition.
Usage Scenario
Declaration of the abstract state of a class:
class MyCollection {
//@ public ghost \dl_Set<[String]> elements;
}Alternatives
Using alias definitions in .key
Every type we want to represent as a parametric type,
we have to add an extra sort in our sort definitions via an alias.
\sorts {
\alias myStringSet = Set<[String]>;
}
Problems:
We separate the definition of the type from the place it is used.
As a consequence when we want to edit the alias,
we might run into the problem that is used somewhere else too.
Also, the current approach makes code generation using this parametric sorts much harder.
Allow alias definitions in classes
Add an alias statement, that can declare such an additional sort alias locally, like:
class MyCollection {
//@ \dl_alias myset = Set<[String]>;
//@ public ghost \dl_myset tasks;
}Problem: The scope where this alias is allowed needs to be determined,
as name conflicts might appear.
Estimated effort
-
Discussion of best practices and (allowed) syntax
-
Adaption to jmlparser to support the new syntax
-
The changes in KeY's logic should be minimal as the parametric types already exist,
and only the new places where they can appear need to be adapted.
Additional context
- Local alias definitions as described in the alternatives might be helpful for more complex type declarations,
without fragmentation across multiple files.
Compare:
Please describe your proposal in a ONE sentence
Parametric Type Declarations (
\dl_Set<[String]>) are not possible in ghost state declarations.Underlying problem
When creating the logic abstraction of a class,
one should be able to use the new parametric types.
When we have complex parametric types (with more, recursive definitions),
it makes sense to use the alias definition.
However, for simple sorts, like
Set<[String]>, Set<[Int]>, List<[Int]>,…it would be great,to just be able to define them when declaring a field of such type.
If one wants to read the code later and stumbles across such a alias definition,
one has to look up the definition in a different file
which is quite some effort for just a simple type definition.
Usage Scenario
Declaration of the abstract state of a class:
Alternatives
Using alias definitions in
.keyEvery type we want to represent as a parametric type,
we have to add an extra sort in our sort definitions via an alias.
Problems:
We separate the definition of the type from the place it is used.
As a consequence when we want to edit the alias,
we might run into the problem that is used somewhere else too.
Also, the current approach makes code generation using this parametric sorts much harder.
Allow alias definitions in classes
Add an alias statement, that can declare such an additional sort alias locally, like:
Problem: The scope where this alias is allowed needs to be determined,
as name conflicts might appear.
Estimated effort
Discussion of best practices and (allowed) syntax
Adaption to
jmlparserto support the new syntaxThe changes in KeY's logic should be minimal as the parametric types already exist,
and only the new places where they can appear need to be adapted.
Additional context
without fragmentation across multiple files.
Compare: