@Deprecated
public abstract class JMLUtils
extends java.lang.Object
Constructor and Description |
---|
JMLUtils()
Deprecated.
|
Modifier and Type | Method and Description |
---|---|
static boolean |
isJmlCommentStarter(java.lang.String starter)
Deprecated.
Decides whether the given string is a JML marker
that symbolise a recognisable JML comment.
|
static boolean |
isJmlCommentStarter(java.lang.String jmlMarkers,
java.lang.String tool)
Deprecated.
Decides whether the given string is a JML marker
that symbolise a recognisable JML comment for the given marker of the
tool . |
static java.util.Set<java.lang.String> |
splitJmlMarker(java.lang.String starter)
Deprecated.
Split a given string of JML marker into the single markers.
|
@Nonnull public static java.util.Set<java.lang.String> splitJmlMarker(@Nonnull java.lang.String starter)
@
sign
or by the end of the string. It also is aware of potential
comment starters, i.e., "//" or "/*".public static boolean isJmlCommentStarter(@Nonnull java.lang.String starter)
Uses KEY_TOOL_IDENTIFIER
as the marker for this KeY.
public static boolean isJmlCommentStarter(java.lang.String jmlMarkers, java.lang.String tool)
tool
.
Refer to chapter 4.4. in the jml ref manual.jmlMarkers
- the marker string at the beginning of an JML comment.tool
- the marker of the current toolCopyright © 2003-2019 The KeY-Project.