JML Core

[davidcok]

I have seriously revised and checked over the tables documenting language levels. Also worked to include every language feature.

So please review Section 3.18 -- pdf extract attached,

Everyone -- propose additions or subtractions from Core; comment on any feature forgotten Mattias, Alexander -- fix whether or not KeY supports each of the features JMLCore.pdf

[mattulbrich]

I wonder if code is really core. Is that at teaching level?

[wadoon]

• I am not sure, whether we should list the tool support in the reference manual. I think we should just have links to specific pages on the tool web pages, which states and explain the degree of support, as the support may change or differ subtle.

• The statement specifications should be separated from the loop specification.

• Some constructs of KeY are missing, like loop_contract or information flow for loops. But I wouldn't consider to add tool-specific construct to the manual. I would like to keep them separated.

• Also, I am considering a different presentation of the language levels, because some of the features play together and come only together with other features. For example, considering the support for different math semantics, you need to consider all three modifiers; or information flow brings clauses and keywords on methods and loops. This structure is lost, but at the moment I have no concluding opinion on the presentation.

[mattulbrich]

I do not think that the tool specific constructs will be covered in the ref manual. But we should have them listed here to see what we have in common and what is different.

[leavens]

Hi Mattias, David, and all,

I do think that code contracts are an important concept in JML, but I can agree to leaving them out of the core.

    Regards,

    Gary T. Leavens
    329 L3Harris Center
    Computer Science, University of Central Florida
    4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
    http://www.cs.ucf.edu/~leavens phone: +1-407-823-4758
    ***@***.******@***.***>

[leavens]

Hi Mattias and all,

I agree that we should leave out tool-specific constructs. They will tend to be obsolete faster than the rest of the language (I think). I also agree that we could discuss them here.

    Regards,

    Gary T. Leavens
    329 L3Harris Center
    Computer Science, University of Central Florida
    4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
    http://www.cs.ucf.edu/~leavens phone: +1-407-823-4758
    ***@***.******@***.***>

[davidcok]

I should have made clear that I included tool-specific constructs in the JmlCore lists to be sure they were candidates for discussion. I did not intend for them to remain permanently.

[davidcok]

Changed code to Advanced rather than Core

[davidcok]

Here I think are the open questions for this topic:

Should tool extensions be listed in the document? Consensus is NO.

Should the tables list which features OpenJML and KeY support? This is not strictly the language and does get obsolete, but might be helpful to the reader.

If the answer to the above question is Yes, then KeY needs to correct the KeY column of the tables

Candidates for additions to Core?

adding: strictly_pure (KeY) moving: measured_by -- we need lots of discussion about this one -- current form is unusable I think adding: show statement (OpenJML) -- this is very handy for users in understanding counterexamples when a proof fails. It is like print-statement debugging. I could not imagine doing practical work without it. Candidates for deprecating: I advocate deprecating debug. Not much used and can be accomplished by //+DEBUG@ set ... Candidates for experimental status instead of Advanced implies_that, for_example Candidates for adding to JML (Advanced category): immutable no_state (KeY) === function (OpenJML) -- model method that does not depend on state, or only on mutable state? two_state (KeY) XXX_free (KeY) inline_loop (OpenJML) -- needs discussion, but I find it necessary in specifying library methods with implicit loops (like ones involving streams or lambda functions) check, havoc (OpenJML) -- would be nice to add, but not as essential \bsum - KeY - what is this? \new_elems_fresh - KeY Naming discussion needed: assignable, loop_invariant, loop_assigns

Many of these need more discussion about semantics, which can happen in the future (and which may end up changing their category). The main point here is to identify where there is consensus and where there is a need for further discussion.

[leavens]

Hi David and all,

I agree about listing tool extensions in the reference manual (so I agree to not list them).

I think that a table listing features in OpenJML and KeY that are supported should not be in the reference manual. It would be best to have a web site for each list, and to point to those websites in the reference manual.

About deprecation of parts of JML, I'm okay with all of that, but I think that by implies_that you mean hence_by? Personally I'm sad to see for_example go, as it seems very useful as documentation and for testing, so I'd prefer to just make it not be in the core. But I'm okay with deprecating it.

For what to add, I would prefer that we discuss any additions before adding them. This is in the general interest of not growing JML more than we need to...

    Regards,

    Gary T. Leavens
    329 L3Harris Center
    Computer Science, University of Central Florida
    4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
    http://www.cs.ucf.edu/~leavens phone: +1-407-823-4758
    ***@***.******@***.***>

[davidcok]

OK - we'll just keep the material (columns and rows) about tools while we are discussing additions/deletions/Core, and then remove them.

Gary - implies_that and for_example aren't deprecated, just proposed to be moved to experimental. To me the experimental category has defined grammar but the use cases and semantics are still under discussion. (And by implies_that Mattias meant implies_that not hence_by)

But agreed then to deprecate debug

Mattias - do you concur with this?

I've identified everything I think needs discussion and agreement with a ?. To keep some order to this, I'd ask everyone to add comments but not change the text (except in the column of your tool) until we have come to agreement.

And we'll have separate discussions about each of the items proposed for Core or proposed to be added to JML.

[leavens]

Hi David, Mattias, and all,

OK, that sounds fine to me, David. I'm fine with moving implies_that and for_example to experimental features.

Thanks for all of this...

    Regards,

    Gary T. Leavens
    329 L3Harris Center
    Computer Science, University of Central Florida
    4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
    http://www.cs.ucf.edu/~leavens phone: +1-407-823-4758
    ***@***.******@***.***>

From: David Cok @.> Sent: Tuesday, December 14, 2021 3:52 PM To: JavaModelingLanguage/RefMan @.> Cc: Gary Leavens @.>; Comment @.> Subject: Re: [JavaModelingLanguage/RefMan] JML Core (Issue #25)

OK - we'll just keep the material (columns and rows) about tools while we are discussing additions/deletions/Core, and then remove them.

Gary - implies_that and for_example aren't deprecated, just proposed to be moved to experimental. To me the experimental category has defined grammar but the use cases and semantics are still under discussion. (And by implies_that Mattias meant implies_that not hence_by)

But agreed then to deprecate debug

Mattias - do you concur with this?

I've identified everything I think needs discussion and agreement with a ?. To keep some order to this, I'd ask everyone to add comments but not change the text (except in the column of your tool) until we have come to agreement.

And we'll have separate discussions about each of the items proposed for Core or proposed to be added to JML.

- You are receiving this because you commented. Reply to this email directly, view it on GitHubhttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FJavaModelingLanguage%2FRefMan%2Fissues%2F25%23issuecomment-993987738&data=04%7C01%7CLeavens%40ucf.edu%7Cf8c0d37ee8c942f79c9d08d9bf438ff3%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637751119164864062%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=%2BS3l1zcIp3hz6BPgTJInOqEcX5hg1FdgedoW2JaaWBY%3D&reserved=0, or unsubscribehttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAC53NPN2XHO4NQAKCPRBM6LUQ6U6VANCNFSM5J7KHDXQ&data=04%7C01%7CLeavens%40ucf.edu%7Cf8c0d37ee8c942f79c9d08d9bf438ff3%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637751119164874052%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=TIXF1rilfh%2BBkW03G1AfoQ30jUQljFuBvMRW7QbCM84%3D&reserved=0. Triage notifications on the go with GitHub Mobile for iOShttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fapps.apple.com%2Fapp%2Fapple-store%2Fid1477376905%3Fct%3Dnotification-email%26mt%3D8%26pt%3D524675&data=04%7C01%7CLeavens%40ucf.edu%7Cf8c0d37ee8c942f79c9d08d9bf438ff3%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637751119164874052%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=JpHBsTff9hXv8GDSLl7jLnQPwJZRlw7wPdDTlSWn1Mw%3D&reserved=0 or Androidhttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fplay.google.com%2Fstore%2Fapps%2Fdetails%3Fid%3Dcom.github.android%26referrer%3Dutm_campaign%253Dnotification-email%2526utm_medium%253Demail%2526utm_source%253Dgithub&data=04%7C01%7CLeavens%40ucf.edu%7Cf8c0d37ee8c942f79c9d08d9bf438ff3%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637751119164884049%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=fWpr2KrCuzIOKa2fw%2BktvdrfjI8YMTBR%2F5gcGVjc%2FIY%3D&reserved=0.

[wadoon]

\bsum - KeY - what is this?

Bounded Sum:

(\bsum int i; <lowerbound>; <upperbound>; <expr>)

Example:

(\forall int n; n > 1; 
  n*(n-1)/2
  == 
  (\bsum int i; 0; n; i))`

\bsum has some advantages in the deduction.

[davidcok]

So how is it different than \sum ? (that it should be added to JML?)

[mattulbrich]

The major benefit is that it can be treated nice with rules like:

b > a ==> (\bsum int i; a, b, term) == term{i/a} + (\sum int i; a+1, b, term)
(\bsum int i; a, a, term) == 0

With the general sum, one always has to pattern match against a <= i < b.

People tend to use arbitrary sum terms which are difficult to handle (well KeY cannot). These bounded sums can be handled rather well. It guides user in what they can use. But it does not increase expressiveness.

[mattulbrich]

Should tool extensions be listed in the document? Consensus is NO.

I'd still like to see a webpage that lists all the language features of all tools in a table with very short descriptions and/or links. Someone working on Java verification can then go and look for, for instance, information flow specification and can come to KeY. (just one example)

Moreover, it is a nice table to show what all can be done and expressed in JML, that it is a living language that is advanced not only by a single team but with various ideas at various places.

It should be referenced from the refman. We should keep that table moderately accurate, but not super-accurately-updated.

[mattulbrich]

moving: measured_by -- we need lots of discussion about this one -- current form is unusable I think

Would be interested to discuss this. It works very well in KeY, and for any recursive algorithm, you need it. We have generalised it so that you can not only specify integers but also pairs, boolean, sequences, ...

[mattulbrich]

no_state (KeY) === function (OpenJML) -- model method that does not depend on state, or only on mutable state?

In KeY, no_state means that no heap is available for evaluation. This may (in future) include following final field references if we can accomodate that. What's the semantics of function? Same?

[mattulbrich]

Gary @leavens, how does for_example work? Can you thus specify test cases?

[mattulbrich]

we'll need a few days to fill the table, but it is helpful indeed.

[dmzimmerman]

The tables currently list model as a modifier in Core when applied to fields and methods, but "model fields" and "model methods" as Advanced features; I imagine that model fields and methods should be Core in both places. And if model fields are Core, perhaps datagroups (and in) ought also to be Core.

[leavens]

@mattulbrich Yes, for_example can be used to specify test cases. More generally it can also just give examples of a method's behavior.

[davidcok]

Gary, do you think of for_example as just another specification case that must be obeyed and can be checked against the method body just like the usual spec cases? Or should it be provable from the usual spec cases alone?

Similarly the name implies_that implies to me that one should prove the implies_that spec cases from the usual ones. Is that the intent?

[leavens]

I agree with Dan Zimmerman (@dmzimmerman) that model fields and model methods should be core features.

David (@davidcok) I think of for_example as something that should be provable from the usual spec cases and as redundant documentation.

Also the implies_that spec cases should be provable from the usual spec cases. This is another redundancy feature (that is intended to be useful for highlighting behaviors that might not be obvious but which might nevertheless be important).

These are both described in the paper: Gary T. Leavens and Albert L. Baker, "Enhancing the Pre- and Postcondition Technique for More Expressive Specifications", in (Jeannette M. Wing and Jim Woodcock and Jim Davies (eds.), FM'99 --- Formal Methods: World Congress on Formal Methods in the Development of Computing Systems Toulouse, France, September 1999, Proceedings, Springer-Verlag, LNCS Vol. 1709, pp. 1087-1106, 1999, http://dx.doi.org/10.1007/3-540-48118-4_8 . (I can provide a copy if you can't access that.) That paper says: "A redundant part of a specification does not itself form part of the contract, but instead is a formalized commentary on it."