text blocks

[davidcok]

Java now allows text blocks. In

        String s = 
            """
            abc
              def
            ghi
            """;

s is "abc\n def\nghi\n". Note that common indentation is removed.

Text blocks can be put in JML block annotations

/*@     ghost String s = 
  @     """
  @     abc
  @       def
  @         ghi
  @         """;
  @*/

The question is do we ignore the white space and @ symbols at the beginning of the line, omitting them from the resulting string? Or do we not permit the @ symbols here (they would become part of the string)?

[lks9]

I think this would be a similar case:

/*@ ghost String s = "abc  @ def ghi @"; @*/

The @ should be treated in a string block as it would be treated in a normal string. So they would become part of the string.

[wadoon]

@davidcok Yes, I would say the leading \s@+ should not considered to be in the content of the String literal. I see the "@"-sign just as a part of the outer encoding layer.

The only problem might be, that someone wants to declare a string with lines leaded by an "@" sign. Both strings s1, s2 would not have the same content:

/*@
  @ ghost String s1 = """
  @            @ X 
  @            @ Y 
  @            @ Z 
  @            """;
  @ 
  @ ghost String s2 = """
              @ X 
              @ Y 
              @ Z 
              """;
  @*/

Do we need an escape sequence for this? Or do we consider this as a very rare case.

Implementaton detail: This can be done in two ways: (1) You have sanitation phase in which the (un-)conditional comments are preprocessed for parsing (current state in jmlparser); or (2) you replace the literal post-processing with String.stripIndent defined by JLS 3.10.6 with a custom post-processing.

@lks9 Text blocks are far more fancier than expected at the first glance, especially, a text block does not directly deliver the sequence of characters inside the literal. See JLS 3.10.6. In Kotlin, text blocks are far more identical to normal string literals.

[lks9]

Thank you for the background info.

Yes, this would also be an option. But then, also a new escape sequence would be needed. How about \@. Or one could use @ @ to escape (the first @ is ignored by JML, the space is ignored by text-block pre-processing (depending on the indentation level), the second @ is then treated as string literal). Also the question arises whether a leading @ is treated as ws or simply removed:

/*@ ghost String s3 = """
  @ X
    Y
    @Z""";
  @*/

Would you treat s3 as "X\n Y\n Z", "X\nY\n Z", "X\nY\n@Z" or "X\n Y\n @Z"?

I still think that treating @ just like a normal non-ws character is more logical. Also, there would be no need for an escape sequence. In the example, the string would be s3 = "@ X\n Y\n @Z". But this is my personal opinion.

[wadoon]

I would currently see it as: "X\nY\n@Z", because the rule say [\n\s+@+ ] should treated as whitespace.

In the example, the string would be s3 = "@ X\n Y\n @Z". But this is my personal opinion.

Would it not be two spaces before "Y" and "@Z"? Because the "@" determines the indentation.

[lks9]

I would currently see it as: "X\nY\n@Z", because the rule say [\n\s+@+ ] should treated as whitespace.

Ok. But then, why not "X\nY\n Z"? This would treat @ as whitespace.

In the example, the string would be s3 = "@ X\n Y\n @z". But this is my personal opinion.

Would it not be two spaces before "Y" and "@z"? Because the "@" determines the indentation.

It should. I have these spaces in my comment but somehow github does not display them correctly and makes one out of two spaces.

Again, I think that the @ should not be treated as whitespace in a text block. This would be one exception to the JML rule but I think it is easier than the alternatives.

[davidcok]

I agree with the last point made above. For simplicity: "I think that the @ should not be treated as whitespace in a text block. This would be one exception to the JML rule but I think it is easier than the alternatives."

[leavens]

The decision to not treat @ as whitespace in text blocks is sensible, I agree.

[davidcok]

Proposed closure (@mattulbrich ?):

String text blocks are legitimate String tokens in JML, however

• as a text block is a single token spanning multiple lines, it must be in a JML block annotation (not a line annotation)
• any @ symbols in the text block are considered part of the string literal (in contrast to the usual JML rule that considers \s@+ at the beginning of lines within block annotations to be white space)

[wadoon]

I am not happy with this rule: It complicates the sanitation of JML annotation texts and the pretty printing. Both need to be aware of text blocks now.

The "@"-leading syntax option ...

1. is in alignment to Javadoc. And in Javadoc, there is no different meaning of leading stars when Text Blocks occurs.
2. is only present due to aesthetic consideration. I think, if we drop it in Text Block we could also drop leading "@"-signs in general.

There is also a different way: We could tighten the leading "@"-sign rule to "\s{n}@" (instead of \s+@+), where n is the depth-1 is the column of the "@"-sign in /*@. Hence the "@"-signs must be perfectly align in their columns.

[mattulbrich]

I do not have a strong opinion. Since it will be a not much-used feature, I assume, I'd be ok with not special-casing '@' as it might make trouble.

[lks9]

I just came up with a compromise:

1. If we have a multi-line JML annotation /*@ ... */ and every line begins at least with one @: Then in each line of a text block, only the first @ is ignored.

   Example:

   /*@
     @ ghost String s1 = """ 
     @            @ X 
     @            @ Y 
     @            @ Z 
     @            """;
     @*/

2. If we have a multi-line JML annotation /*@ ... */ and there is at least one line that does not begin with @: Then all @ in the text block are treated as non-whitespace, including any leading @. This is exactly as in outside-Java. Example:

   /*@
       ghost String s2 = """ 
                  @ X 
                  @ Y 
                  @ Z 
                  """;
     @*/

   Note that s1 and s2 equal "@ X\n@ Y\n@ Z\n".

   /*@ ghost String s3 = """
     @ X
       Y
       @Z""";
     @*/

   In s3 there is no @ in line 3. If there would be, then rule 1 instead of this rule 2 would apply. s3 corresponds to the following Java text block:

   String s3 = """
   @ X
   Y
   @Z""";

3. JML text blocks with //@ on each line are allowed two. The trailing //@ would be ignored, any @ following would be treated as is. Example:

   //@    ghost String s4 = """ 
   //@               @ X 
   //@               @ Y 
   //@               @ Z 
   //@               """;

   Again, s1 == s4.

4. But mixing single line with multi-line comment styles inside text blocks is forbidden and would lead to a parsing error.

This may sound complicated. But if you don't know the rule and you have a preferred style (either 1, 2 or 3), then it still works as you would probably expect. What do you think?

[leavens]

I’m okay with a combination of 1 and 2.

[wadoon]

• Case 1 is fine for me, as it is covered by the current rule. There are spaces between the "@" signs. Only the first run of @-signs are removed.

• Case 2 needs an extra detection step and is error prone. One missing "@"-sign (which does not have any meaning yet) changes the parsing behavior.

• Case 3 is forbidden: A text block is one token. Tokens do not span over JML comments.