Library specs and language levels

[davidcok]

In thinking through language levels I had this concern about library specs.

While we can say that a small set of language features are Core, the library specs are likely to use more than Core. Their specs are often complex and need advanced features to be reasoned about. Indeed specifying them is sometimes the reason for advanced features. I routinely use nested method specs, normal_ and exceptional_behaviors, model programs in support of lambda functions, embedded conditional annotations to guard RAC from unexecutable features. Some (but only some) of these features could be desugared away, but that would certainly make the specs less readable and less maintainable.

So it is not a problem if one tool supports a Core for educational use but has more sophisticated features behind the scenes.

But if the library specs are used by multiple tools then those specs can only use features that the tools agree on.

But that gets to the crux: do you think we will ever be at the point of having common specs for system libraries, or should we just acknowledge that OpenJML and KeY will be writing specs differently as long as those projects last?

That said, the effort to write the 2nd edition, be clearer about semantics, and to unify JML drives conversations like these GitHub issues that benefit JML and both tools. I wouldn't want to lose that by removing driving forces.

[mattulbrich]

But if the library specs are used by multiple tools then those specs can only use features that the tools agree on.

Since we have the //+TOOL@ feature, it might very well be possible to have a common part of a contract and have the different tool specs in parallel.

It might even be instructive for a reader to see the different specification pragmatics next to each other.

But it might also be quite confusing for a reader.

[davidcok]

Using //+TOOL@ would be a way to combine the specs from different tools, at least syntactically. Where can I see the current KeY system library specs to get a sense for how this would merge?

[wadoon]

Using //+TOOL@ would be a way to combine the specs from different tools, at least syntactically. Where can I see the current KeY system library specs to get a sense for how this would merge?

We do not have separated specifications, instead we have a JavaRedux which is a copy of the essential classes of Java.

For example java.math.BigInteger: You should notice that the method bodies are missing.

[davidcok]

OK. These mostly look like .jml files, except that constructors have bodies. I do not see a lot of specifications.

Does KeY support .jml files for binary classes? If so, why not use them here?

[mattulbrich]

I must admit that KeY does not have a standing specification of libraries. We have experienced that we require different specs for each case study, so we usually do them specifically for a situation.

I think System.arraycopy is the only really specified thing in the standard.

I would like to be able to select (by code annotation) which named contract is to be applied, ... then having such a collection would really be helpful.

[mattulbrich]

While it is not the JDK standard library, we have library examples like this that use typical KeY JML.

Does KeY support .jml files for binary classes? If so, why not use them here?

Yes, our redux classes can be considered .jml files. I remember implementing support for .class files (via Recoder) in KeY. Has never been used though I think. Moreover, the stub classes that we expose here are not the full interface of the classes. The class files are not needed.

[davidcok]

So if KeY were to be used for a class (that is, a university class), where students would want to use Java system library classes, what would they use?

On Dec 13, 2021, at 10:08 AM, Mattias Ulbrich @.***> wrote:

While it is not the JDK standard library, we have library examples like this https://git.key-project.org/key-public/key/-/tree/stable/key/key.ui/examples/heap/list_seq/src that use typical KeY JML.

Does KeY support .jml files for binary classes? If so, why not use them here?

Yes, our redux classes can be considered .jml files. I remember implementing support for .class files (via Recoder) in KeY. Has never been used though I think. Moreover, the stub classes that we expose here are not the full interface of the classes. The class files are not needed.

[wadoon]

I also have the KeY examples as test cases for my tool:

https://github.com/wadoon/jmlparser/tree/master/jmlparser-jml-tests/src/test/resources/fullexamples/key

There is also a folder with already extracted JML annotation texts (of KeY and OpenJML):

https://github.com/wadoon/jmlparser/tree/master/jmlparser-jml-tests/src/test/resources/fragments

These are primary used for tool debugging.

[davidcok]

Could this be done with //+TOOL@ or do you need names for specification behaviors?

On Dec 13, 2021, at 10:02 AM, Mattias Ulbrich @.***> wrote:

I would like to be able to select (by code annotation) which named contract is to be applied, ... then having such a collection would really be helpful.

[mattulbrich]

Could this be done with //+TOOL@ or do you need names for specification behaviors?

I can easily think of a situation where one callsite requires one contract and another callsite requires another contract. So the context has to be switched after parsing.

I consider //+TOOL@ as a kind of preprocessing on a pre-parser level (as we have discussed) such that not-supported spec is not even parsed.

I would not mix that with switching between behaviours, that seems to be a different level.

[wadoon]

So if KeY were to be used for a class (that is, a university class), where students would want to use Java system library classes, what would they use?

They would just use KeY with the given JavaRedux as the bootclasspath.

If a desired class is not defined in JavaRedux, they have to create their own folder and set it as the bootclasspath in KeY. The tricky thingy is, that KeY requires certain classes to be defined in JavaRedux. So normally, they would copy the JavaRedux folder, and add their class.

[mattulbrich]

Moreover: We usually consider self-contained implementation that do not depend on much library specifications. Existing libraries are hard to specify and verify faithfully because they allow for more side effects than one wishes. We tend to have our own collections in many cases. If we work on JDK collections, then we would replace the base classes in KeY like Alexander pointed out.

[leavens]

Hi Mattias, David, and all,

I understand that for papers one might not want to rely on the JDK libraries. However, in practical programming, these libraries are used very heavily. So I do think it's important to have specifications for them, although it's a big job to do that.

    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: Mattias Ulbrich @.> Sent: Monday, December 13, 2021 10:21 AM To: JavaModelingLanguage/RefMan @.> Cc: Subscribed @.***> Subject: Re: [JavaModelingLanguage/RefMan] Library specs and language levels (Issue #22)

Moreover: We usually consider self-contained implementation that do not depend on much library specifications. Existing libraries are hard to specify and verify faithfully because they allow for more side effects than one wishes. We tend to have our own collections in many cases. If we work on JDK collections, then we would replace the base classes in KeY like Alexander pointed out.

- You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHubhttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FJavaModelingLanguage%2FRefMan%2Fissues%2F22%23issuecomment-992585081&data=04%7C01%7CLeavens%40ucf.edu%7Ce9a66cdef2394c41bef708d9be4c1a7d%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637750056340439036%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=7EA6qmaYW5ea9JwmTkeWwbnFw%2BKxOz0ARJWZyYIdNfI%3D&reserved=0, or unsubscribehttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAC53NPJH433UGVNBOO2A2EDUQYFL7ANCNFSM5J6I576A&data=04%7C01%7CLeavens%40ucf.edu%7Ce9a66cdef2394c41bef708d9be4c1a7d%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637750056340449022%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=F7X65KGPiPTM98tbb9ZDlo%2FH0BBYAcjDKT1busYSiCM%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%7Ce9a66cdef2394c41bef708d9be4c1a7d%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637750056340459018%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=B7zT9YXhF3GnBjkxk3eb9NxyBIpCXUEo2KOun1DnTrw%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%7Ce9a66cdef2394c41bef708d9be4c1a7d%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637750056340459018%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=oiq5Eigvcl0mRNlWid6xxwMi8ihDyiTDbhODovRAles%3D&reserved=0.

[wadoon]

I consider //+TOOL@ as a kind of preprocessing on a pre-parser level (as we have discussed) such that not-supported spec is not even parsed.

Yes, this is right. But you can consider to parse the JML multiple times with different active keys.

I am current thinking about my meta-model for my jmlparser. In the quintessence, I am defining the relationship between a MethodDeclaration and a JmlContracts. For me, a method can have multiple contracts, and this assocation has an attribute: the used active key set. In UML:

┌────────────────────────┐           ┌─────────────────┐
│                        │ 1       * │                 │
│   MethodDeclaration    ├────┬─────►│  JmlContract    │
│                        │    │      │                 │
└────────────────────────┘    │      └─────────────────┘
                              │
                              │
                       ┌──────┴─────────────────────┐
                       │ activeKeys : Set<String>   │ 
                       └────────────────────────────┘

[mattulbrich]

I understand that for papers one might not want to rely on the JDK libraries. However, in practical programming, these libraries are used very heavily. So I do think it's important to have specifications for them, although it's a big job to do that.

Absolutely.

But it is also tough to get them sound, waterproof for the general JDK.

Let's make an experiment: I'd like to check OpenJML's j.u.List spec and see how we can find common grounds there.

[leavens]

Hi Mattias, David, and all,

It may be a good idea to try an experiment to agree on syntax and annotations and their semantics, however, I wonder if a class like ArrayList, which has code, might be better than the List interface in java.util?

    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]

java.util.List (and collection classes in general) is challenging. I’m sure it is wrong in various respects, likely having to do with equals. I have been revising the specs of all the Collection classes to use built-in value types Also because one can’t count on equals() of List elements to be pure, I’m still thinking about how best to specify equals and to apply it in a specification. Perhaps we need a pure model method that is specified to do the same thing as equals but without any side-effects, and then that can be used in further specifications.

Similarly sorted collection in Java is open to a problem if the sort function of the object is changed while things are in the sorted heap

You could also try System.arrayCopy, though it makes heavy use of \type and \TYPE and \elemtype

In any case I welcome such experiments as a way to expose specification bugs and drive toward commonality.

On Dec 13, 2021, at 11:17 AM, Mattias Ulbrich @.***> wrote:

Let's make an experiment: I'd like to check OpenJML's j.u.List spec and see how we can find common grounds there.

[wadoon]

java.util.List (and collection classes in general) is challenging.

We have plans to go for algebraic data types for the specification, and currently explore CASL in a bachelor thesis.

I am not sure whether JML has a built-in map and sequence datatype.

[davidcok]

OpenJML has (experimentally) added primitive datatypes with value semantics: string, array, sequence, map, set. They are defined with respect to underlying arrays that are modeled with SMT's array sort, rather than explicitly with algebraic relationships, though the latter could be tried as well.

[mattulbrich]

Great. I am sure this will prove very helpful! (see also my comment on #26 using "\seq".)

[leavens]

Having built-in mathematical types used in specifications, which are themselves specified algebraically, takes us back to the Larch approach to specification. I agree that either doing that or specifying that such primitive types have a meaning specified in SMT-LIB is a good thing, however.