Array indices

[mattulbrich]

A common pattern for quantifications is

(\forall int i; 0 <= i && i < a.length; ...)

We have agreed to support 0 <= i < a.length and I think both tools do.

We had discussed to support "i is a valid index for array a", too, but have never finalised the discussion on the concrete syntax.

Candidates include:

1. i \in a
2. a.hasIdx(i)
3. \index(i, a)
4. i \index_for a

I think 1 is very short, but it will have the possible misinterpretation of "value i is in a", i.e. "there is an index k in a such that a[k]==i".

What do you think?

[davidcok]

I agree that k \in a is ambiguous. Doe sit mean k is an element of a or ranges over the indices of a or ranges over the values of a

I would prefer k \in a.indices or k \in a.keys . The latter matches well with iterating over sets in general (here the keys of a map). Then k \in a.values is also natural.

The extension is then k \in (some Iterable or class with a .iterable() member), where a.keys (or .indices) is just one such example.

Then additionally, I would then also advocate for .. to be a real operator, creating a \range (a value type like \bigint and \locset), which is also an Iterable, So you can write k \in 4..6

• David

[leavens]

Hi David, Mattias, and all,

I think a while ago someone (David?) proposed that we should have syntax for taking a quantified variable from an iterator, and that seems to be a more general solution than special syntax for array indexes. (However, it might not be as convenient, as one would need to write an iterator to return the indexes of an array, and that doesn't seem to be part of standard Java, but see https://stackoverflow.com/questions/477550/is-there-a-way-to-access-an-iteration-counter-in-javas-for-each-loop.)

How about extending the syntax for a quantified-var-declarator to support something like the syntax in the Java extended for loop? Concretely this would be:

quantified-var-declarator ::= ident: expression | ident [ dims ]

The expression following the colon in the first form of a quantified-var-declarator must denote an iterator (an object with next() and hasNext() methods).

For example, one could write:

  (\forall  int i :JMLArrays.indexesOf(a); 0 < i; a[i] > 0)

with a new class JMLArrays having a static method indexOf providing an iterator for its argument array that supplies the indexes of that array. In this way, one could also iterate over the indexes in reverse order and one could provide similar iterators for other types.

    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
    ***@***.******@***.***>

[mattulbrich]

(\forall int i : JMLArrays.indexesOf(a); 0 < i; a[i] > 0)

I do not like the colon here, this is very different from JML so far.

[leavens]

Hi Mattias, David, and all,

Mattias wrote:

(\forall int i : JMLArrays.indexesOf(a); 0 < i; a[i] > 0)

I do not like the colon here, this is very different from JML so far.

I agree it's not very JML-like, but this colon is modeled on the extended for loop syntax in Java. Java seems to use this syntax with the intention of ":" meaning "element of". So I would think that Java programmers would find it fairly natural as a syntax.

    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]

On Dec 13, 2021, at 10:59 AM, Gary T. Leavens @.***> wrote:

For example, one could write:

(\forall int i :JMLArrays.indexesOf(a); 0 < i; a[i] > 0)

with a new class JMLArrays

There already is, at least in OpenJML, a class org.jmlspecs.lang.JML that contains various utility methods. I’d recommend that rather than a new class. One could even add a model method to java.util.Arrays. Recall that org.jmlspecs.lang.* is automatically imported into JML environments.

So then one can write JML.indices(a), as (\forall int k; k \in JML.indices(a); … ) I probably still would prefer (\forall int k; k \in a.indices; … )

Like Mattias, I’m not ready to break with the classic JML syntax.

• David

[leavens]

Hi David and all,

Sure, putting such a method in org.jmlspecs.lang.JML would be fine, although that would privilege some types (the ones with such methods) over others.

I am okay with the proposal (perhaps that was your original proposal, David) to have a method to return a set of indexes and to use that with a syntax like \in in the range predicate, as you wrote:

I probably still would prefer (\forall int k; k \in a.indices; ... )

That would also require adding a model field to arrays (and other collection types) to hold a set of such indexes in the field (indices).

    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]

On Dec 13, 2021, at 1:32 PM, Gary T. Leavens @.***> wrote:

Sure, putting such a method in org.jmlspecs.lang.JML would be fine, although that would privilege some types (the ones with such methods) over others.

I’m not sure what you meant by that, Gary.

What I’m proposing is

1) Allow the predicate x \in o in quantifiers, where o is any Iterable. So that includes all collections, for example. And also keySet and valueSet of maps. 1’) In fact \in would be a boolean operator allowed anywhere to test membership.

2) The only thing missing then is arrays. So we define a.indices (or some such syntax) whose value is an Iterable yielding the \bigints 0 to a.length-1

3) We can use x \in a to mean x is in the values of a, or we also add a.values to return an appropriate List, or just use x \in Arrays.asList(a). Just using asList requires no new syntax, but does make reasoning more difficult.

• David

[wadoon]

1) Allow the predicate x \in o in quantifiers, where o is any Iterable. So that includes all collections, for example. And also keySet and valueSet of maps.

Would this mean, that an iterator is created when I evaluate a (\forall int k; k \in a.indices; ... )?

Maybe where is no intuitive way for generalizing the bound in quantifiers. So I propose a solution based on lambdas:

ary.\all(it -> p(it))  // ==> (\forall int x; 0<= x < ary.length; p(a[x])
ary.\any(it -> p(it))  // ==> (\exists int x; 0<= x < ary.length; p(a[x])
ary.\allIndexed((idx,it) -> p(idx, it))  // ==> (\exists int x; 0<= x < ary.length; p(x, a[x])
...
map.\anyKey(k -> k>2)  // ==> (\exists K k; k \in map.entrySet(); k>2)
map.\allEntries((k,v) -> p(k,v)) // ==> (\forall K k; (\forall V v; map.get(k) == v && v != null; p(k,v))

The idea is that we extend the built-in data types with (virtual) model-methods, which basically encapsulate different quantification over these data structure. Via method contract (or by built-in support of the verification) the quantified claim is translated back to the basic JML. The advantage is that everyone can define its own quantification type, it is easily extendable, object-oriented, and follows Java-idioms.

[davidcok]

That is a lot more complexity than we are looking for. Plus the desugaring should make it easier to reason about rather than more difficult, by involving lambda.

An additional question though is whether \in uses == or equals

[wadoon]

That is a lot more complexity than we are looking for. Plus the desugaring should make it easier to reason about rather than more difficult, by involving lambda.

On the parser side, you have no additional complexity. Everything is Java syntax with escaped identifiers. Of course, you can decide to have a desugaring (direct transformation into a quantified expression), or try to solve it with a more general concept of lambda and method contracts. And Java lambda is going to be a hot discussion topic for JML.

An additional question though is whether \in uses == or equals

I would go for equals, but I know that this is very stressful. Therefore, I ask a different question:

In elem \in seq, which interface must the type of seq implement?

If the type must be an Iterable, do we follow the (JLS 14.14.2)(https://docs.oracle.com/javase/specs/jls/se7/html/jls-14.html#jls-14.14.2). Then the equivalent of elem \in seq is in JavaDL the following:

  elem \in seq <->  \[ 
    boolean b = false;
    for (Iterator<T> iter = (seq).iterator(); iter.hasNext(); ) {
       T e = (T) iter.next();
       if(e.equals(elem)) b = true;
    } \] b; 

Therefore, the creation of an iterator, and the iterator itself must be pure. In my opinion, this is not the way we want to follow. The same for the interpretation via java.util.Collection#contains.

[davidcok]

You can (and OpenJML does) model an Iterator as a sequence of values that the iterator produces (and will eventually produce if it keeps iterating). Then \in is just a matter of finding either a == or equals match in that sequence.

[wadoon]

You can (and OpenJML does) model an Iterator as a sequence of values that the iterator produces (and will eventually produce if it keeps iterating). Then \in is just a matter of finding either a == or equals match in that sequence.

Do you also model the relation between the objects returned by Iterator#next() and the original collection data type? Hence, are you able to conclude that seq.iterator().next() \in seq is valid (for non-empty collection seq)?

[davidcok]

Yes, or at least we could -- I have not checked that example. This is a re-doing of the specs that is underway as the implementation of these new primitive data types in OpenJML is recent.

[mattulbrich]

I am a little reluctant to think of "iterables" here in the sense of instance of interface "Iterable". Creating and then modifying an object for evaluation of a specification expression is a little scary.

I am very happy with x \in s where s is of type JMLList / \seq, ie. a value type.

There might be a model field

 interface Iterable { 
    //@ model \seq values;
    // ...
 }

and x \in iterable is an abbreviation for x \in iterable.values. Then no iterator ever needs to be created.

[mattulbrich]

An additional question though is whether \in uses == or equals

I vote for ==.

[wadoon]

I am not so sure, whether == is a good choice when we come to auto-boxing:

Integer[] seq = new Integer[]{1,2,3};
//@ assert 2 \in seq   // should be true, because integers from -128 upto 127 are cached
//@ assert new Integer(2) \in seq // should be false

[wadoon]

I would also not pledge for obj.equals(other). I would go for the NPE-safe variant Objects.equals(obj,other).

[leavens]

Hi Mattias, David, and all,

This is a basic problem with Java: there is no established convention for equality in collections that makes sense in all cases. My feeling is that collections are fundamentally broken because it’s not clear if the user-defined notion of equality should be used, and if a collection is a collection of object identities or the abstract values represented by objects.

(Begin gratuitous aside) As to how it could be done, I note that CLU had 3 operators for equality: object identity, object similarity (user-defined), and similar one level down, (user-defined, but by convention using object identity to compare sub-objects). CLU also had corresponding copy operators (copy returned an object that was similar and copy1 returned a 1-level copy that was similar1). Functional languages tend to require that a comparison function be given as an argument, and that could be a solution for Java now, but it’s too late to change the libraries… (End gratuitous aside)

At least in Java == has no side effects, but it’s the wrong way to compare immutable objects… However, for pure value types we define, we could say that == compares values.

    Regards,

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

On Dec 13, 2021, at 7:42 PM, Mattias Ulbrich @.***> wrote:



An additional question though is whether \in uses == or equals

I vote for ==.

— 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%2F23%23issuecomment-993047470&data=04%7C01%7CLeavens%40ucf.edu%7Cc6128257b4c84f657da008d9be9aa2f5%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637750393633538367%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=fXoyZMmIqAj1nslVwltEX8IGcp9myRFfZes7G7jD1UU%3D&reserved=0, or unsubscribehttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAC53NPMSC7VNPBF63QW6BH3UQ2HIDANCNFSM5J6MQOZA&data=04%7C01%7CLeavens%40ucf.edu%7Cc6128257b4c84f657da008d9be9aa2f5%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637750393633548366%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=RTfZUKdkzFGc1ucxKS0aStxjbMX2Deh3F8pdasP4XmA%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%7Cc6128257b4c84f657da008d9be9aa2f5%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637750393633558366%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=5EHcL%2FHa4V%2Fp7o6MPJXyGaysg3My6Ph8hJhYP1aMT1c%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%7Cc6128257b4c84f657da008d9be9aa2f5%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637750393633558366%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=bcm2WPej2pLsMWGCXj2KHomSPmQqNi7fZyqRD4TiFuM%3D&reserved=0.

[wadoon]

But could we not just extend JML's notion of java.lang.Object with a new equivalence notion?

package java.lang;

class Object {
    //@ axiom           (\forall Object a, b; a == b ==> a.\eq(b));
    //@ axiom symmetry: (\forall Object a, b; eq(a,b)= b ==> b.\eq(a));

    public /*@ pure */ boolean \eq(Object other); 
}

And for different objects and primitive types, we can define a safe variant.

class String {
   //@ model \seq<char> content;

   /*@
    requires (other instanceOf java.lang.String s);
    ensures  other.content.size == content.size && 
               (\forall int i; 0 <= i < content.size; content[i] == other.content[i]);
    */
   @Override   
   public /*@ pure */ boolean \eq(Object other);
} 

[leavens]

Hi Alexander, Mattias, David, and all,

It's an interesting suggestion to require users to define an appropriate notion of equality for each type. That could work, but would require some effort on the part of users.

However, as I mentioned before, we may actually need several notions of equality, at least for mutable types (i.e., types with time-varying state and thus with non-pure methods). For mutable types, we sometimes want to talk about equality of object identities (== in Java) and sometimes about value equality. I suppose value equality could be defined by the equals method, but that isn't a clearly established convention in Java; so there is a problem if a type has an equals method that doesn't give value equality according to our notion of what the abstract value of the type's objects should be?

So, I do see value in having a specification-only operator with a name that is not a Java name (like the proposed \eq) for value equality. But the meaning of such an operator needs to be constrained more than just by reflexivity, symmetry, and transitivity, we also need to say something like that the result of calling clone is not the same identity, but a object whose value is equal to the cloned object (as in \eq) and that if two objects have equal values, then all model methods applied to them give equal (values of) results.

With subtyping, the behavior of value equality should be based on the static type of the arguments (which should have the same type, so that the dynamic type of the actual arguments is a subtype of the argument type), and thus should only be concerned with the abstract values of the arguments' static type. So this makes value equality more of a specification notion than a Java method, as it would not be subject to dynamic dispatch. There are some semantic issues related to such a static-type based notion of value equality and the dynamic dispatch that applies to model methods. One solution might be to put the type of the value equality comparison into the operator's name (perhaps as a generic argument), but I wonder if that solves the issue of having all (dynamically dispatched) model methods agree on the results of two objects that are value equal at a given type (T) but whose dynamic types are (different) subtypes of T.

What I wonder about is if such a proposal could be detailed and further if it would work for users. It would be worth doing a case study of a mutable type, and some collection of elements of that type, and some generic collection that might contain it. Both static verification and dynamic checking (RAC) should be considered.

    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: Alexander Weigl @.> Sent: Tuesday, December 14, 2021 6:06 AM To: JavaModelingLanguage/RefMan @.> Cc: Gary Leavens @.>; Comment @.> Subject: Re: [JavaModelingLanguage/RefMan] Array indices (Issue #23)

But could we not just extend JML's notion of java.lang.Object with a new equivalence notion?

package java.lang;

class Object {

//@ axiom           (\forall Object a, b; a == b ==> a.\eq(b));

//@ axiom symmetry: (\forall Object a, b; eq(a,b)= b ==> b.\eq(a));

public /*@ pure */ boolean \eq(Object other);

}

And for different objects and primitive types, we can define a safe variant.

class String {

//@ model \seq content;

/*@

requires (other instanceOf java.lang.String s);

ensures  other.content.size == content.size &&

           (\forall int i; 0 <= i < content.size; content[i] == other.content[i]);

*/

@Override

public /@ pure / boolean \eq(Object other);

}

``

`

- 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%2F23%23issuecomment-993428454&data=04%7C01%7CLeavens%40ucf.edu%7C55a695a8767d43627ad808d9bef1b4a9%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637750767596442882%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=8IhIQNsXyb5hjJ3Mu9mSPFOYnhXDH%2BFsjiSnfpKU6QU%3D&reserved=0, or unsubscribehttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAC53NPLBBKNGDAD5GP3RNJ3UQ4QJLANCNFSM5J6MQOZA&data=04%7C01%7CLeavens%40ucf.edu%7C55a695a8767d43627ad808d9bef1b4a9%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637750767596442882%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=5B0mTWeJg2JuuZSvIeROlzPORoGtqY9h6LQwzzZB80g%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%7C55a695a8767d43627ad808d9bef1b4a9%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637750767596452876%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=BjXS2zAOYQwXrvecPs1jTyCPdsqzo0BA%2FExcm1%2BFuqM%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%7C55a695a8767d43627ad808d9bef1b4a9%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637750767596452876%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=cfSxJZWEX2Eg5ZrM4ZpziPioWa8QZFO1OXmgKWt43So%3D&reserved=0.

[leavens]

Hi Mattias, David, and all,

I think converting an abstract collection of values or objects to a mathematical sequence (or set) is a promising idea for specification and verification/checking.

However, I wonder if Java iterators are the right notion for doing that, as iterators themselves are not pure, and may not ever terminate. So would we support infinite sequences and sets in JML? I suppose we could, but that would cause issues for RAC implementations. Those issues could be solved by using lazy evaluation, but that would introduce more mutation (laziness is typically implemented by using an imperative cell). Perhaps a compromise is requiring iterators to be finite by some proof obligations, which would allow the use of finite sequences and sets in specification (and RAC).

On second thought, maybe a better idea is to require users to specify (potentially infinite) sequences and sets by stating a predicate that describes their elements, there might be a verification methodology that could be created that would ensure that every result produced by an iterator satisfies such a predicate. That is one would specify an iterator in part by giving a predicate that describes the elements in the sequence it generates (as a relation between indexes and values, say) and then correctness of an iterator would be established by showing that that predicate holds for all generated elements. To me this seems like an interesting idea; anyone want to write a paper about it with me?

    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 7:41 PM To: JavaModelingLanguage/RefMan @.> Cc: Gary Leavens @.>; Comment @.> Subject: Re: [JavaModelingLanguage/RefMan] Array indices (Issue #23)

I am a little reluctant to think of "iterables" here in the sense of instance of interface "Iterable". Creating and then modifying an object for evaluation of a specification expression is a little scary.

I am very happy with x \in s where s is of type JMLList / \seq, ie. a value type.

There might be a model field

interface Iterable {

//@ model \seq values;

// ...

}

and x \in iterable is an abbreviation for x \in iterable.values. Then no iterator ever needs to be created.

- 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%2F23%23issuecomment-993046514&data=04%7C01%7CLeavens%40ucf.edu%7C5f71d063c9974ae0d39708d9be9a76b6%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637750392908835753%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=hEFmV5s3XUbbECSVYKdFkcRcYlXQrf2sKudfg81BLWY%3D&reserved=0, or unsubscribehttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAC53NPMF2US4I6AMRJJXKFLUQ2HDPANCNFSM5J6MQOZA&data=04%7C01%7CLeavens%40ucf.edu%7C5f71d063c9974ae0d39708d9be9a76b6%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637750392908835753%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=W0k2XXlHqyHjLRdVMcy2EAbU8pqIMMz3I3aAx%2F7beKk%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%7C5f71d063c9974ae0d39708d9be9a76b6%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637750392908845744%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=vdbinVqh1ZuSlbr70prFmkjHSuWQq08POybhfdcxSpQ%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%7C5f71d063c9974ae0d39708d9be9a76b6%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637750392908845744%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=IL%2FNwjHOwsz4hQgRi6dN6zB8R2S7p3EJegJ%2FCd5y9N0%3D&reserved=0.

[mattulbrich]

We really should support both notions of equality in general.

Having said this, I have the feeling that dealing with equals in deductive verification is way more complicated than with identity. The requirements on equals (transitivity, reflexivity, etc.) are quite difficult to capture, in particular with mutable objects.

I am reluctant to use Iterator objects too, they may change state and could run indefinitely.

[mattulbrich]

I think we have consensus for

• t \in a..b is the same as a <= t <= b
• t \in array is the same as (\exists int i; 0 <= i < array.length; array[i] == t) for primitive arrays
• t \in seq is the same as (\exists int i; 0 <= i < seq.length; seq[i] == t) for primitive sequences
• t \in a.XXX is the same as 0 <= t < a.length with XXX either keys or indices or idx or ... should be short.

Right?

[leavens]

Hi Mattias, David, and all,

About a .. b, I wonder if t \in a..b should mean a <= t && t < b instead of a <= t && t <= b. For example, in Dafny and Python, those are half-open intervals, in Python range(0,5) means the sequence [0,1,2,3,4] and does not include 5. Note that the proposal for arrays and sequences uses < on the right.

I would rather have \in be based on some user-defined notion of equality, rather than ==, but it does make sense to base it on ==.

If we used functional notation for these notions, we could use a name to indicate the kind of interval we have in mind (like indexes()) and for membership we could pass an equality parameter as an argument. But there's no problem for value types like int.

The idea of having an "indices" model method is a good one along these lines.

    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
    ***@***.******@***.***>

[mattulbrich]

About a .. b, I wonder if t \in a..b should mean a <= t && t < b instead of a <= t && t <= b. For example, in Dafny and Python, those are half-open intervals, in Python range(0,5) means the sequence [0,1,2,3,4] and does not include 5. Note that the proposal for arrays and sequences uses < on the right.

I totally agree, but I believe this is the semantics built in into JML, in array[a..b]. These two should have the same meaning. I'd favour "<".

I would rather have \in be based on some user-defined notion of equality, rather than ==, but it does make sense to base it on ==.

That's why I only mentioned primitive values. I assumed that there == is without alternative. Right?

[davidcok]

High on my wish list of things that I'd like to change about JML but would be too backwards-incompatible is .. That is, I wish it were a half-open interval, but as Mattias says, we have a long history of it being closed, in storers. So I think we have to remain consistent with that old definition. However, we could use, for example, a...b for half-open intervals, if we wanted to migrate in that direction.

[leavens]

Hi Mattias and all,

Yes, we should have the same consistent semantics for a[l..h] as for this range, but by using a functional notation, such as indexesFrom(l,h) we could avoid the compatibility issue.

If \in only works for primitive value types (and possibly other mathematical value types we define), then it would make sense to only use ==, I agree.

    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 David,

I think if we used a functional notation (like indexes()), we could avoid incompatibility issues. Sure the token ... is different than .. but it's not easy to tell the difference between them.

    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
    ***@***.******@***.***>

[mattulbrich]

If a function, then I'd suggest range(a, b) because it is for general integer ranges not only if they are indices.

From my experiences with Dafny: I have really come to like the brevity in Dafny. And .. is shorter than range. And it is already there ....

[wadoon]

Kotlin uses a..b and a until b; the first one is a <= i <= b and the second is a <= i < b.

Note, that Kotlin allows new definitions of infix operators, and hence until is defined via Kotlin receiver functions.

[leavens]

I like the "until" notation that Alexander is proposing to borrow from Kotlin.

Mattias wrote that he thought we agreed on:

• t \in a..b is the same as a <= t <= b
• t \in array is the same as (\exists int i; 0 <= i < array.length; array[i] == t) for primitive arrays
• t \in seq is the same as (\exists int i; 0 <= i < seq.length; seq[i] == t) for primitive sequences
• t \in a.XXX is the same as 0 <= t < a.length, with XXX either keys or indices or idx or ... should be short.

I am willing to agree to these if we can also add this "until " notation. I would prefer keys as the model field containing the set of indices of an array. I dislike using ... as it is too close to ...

[leavens]

I should add that my preference would be to add intervals as a mathematical value type, assuming we are adding mathematical value types to JML for specification purposes, and to have some syntax for constructing these intervals and some easy way to extract intervals from arrays and sequences (and maps?). This seems more orthogonal and matches Python, for example.

[mattulbrich]

Scala has 1 to 3 == 1,2,3 and 1 until 3 == 1,2.

May I suggest to use \until to not capture another possible identifier name. Would be JMLish. I am happy with a.keys

[leavens]

I agree with that (using \until and .keys).

[WolframPfeifer]

I think that we can not use \until for the same reason as \union is not possible (Unicode escapes in Java), right?

[leavens]

Sigh, you are right, of course. We should have thought of that...

[davidcok]

Perhaps \till ?

[leavens]

Yes, \till would work, I would agree to that.

[mattulbrich]

I think \to would be misleading, right. I am not a native speaker; hence, if you are happy with \till, so am I.

[wadoon]

I am happy with a.keys

I would go for a.\keys. Who knows maybe and a.key will be occupied by JLS in the future.

Where do we book this?

• It is independent of quantifiers.
• It seems that a \till b opens the "infix operators box" and brings new expression kind.
• a.\keys is an extension of the Java meta-model by using a model method. A category that is not present in JML ref.

Both constructs have the potential of introducing extension points (arbitrary infix operators and model fields/methods).

[leavens]

I think we should try to avoid as many backslash keywords as we can, so I think a.keys would be good. Having a new kind of extension is a good reason to avoid this.

However, I agree that there is the possibility that Java would build that into the language at some point in the future. On the other hand, I think that is unlikely, as they would try to avoid it probably, for the same reasons you are worried about it, Alexander.

[mattulbrich]

I agree with Gary. Actually, I would even say that we formally introduce a ghost field keys of type \seq or JMLList into the array types. So a backslash would actually not even be appropriate.

I do not quite get your question, Alexander @wadoon. Does my explanation above answer the question?

[mattulbrich]

Agreement:

• t \in a..b is the same as a <= t <= b
• t \in a \till b is the same as a <= t < b
• t \in array is the same as (\exists int i; 0 <= i < array.length; array[i] == t) for primitive arrays
• t \in seq is the same as (\exists int i; 0 <= i < seq.length; seq[i] == t) for primitive sequences
• t \in a.keys is the same as 0 <= t < a.length for a an array or sequence.

Remains the question what t \in array means for an array of a ref type.

1. t \in array <==> (\exists int i; 0 <= i < array.length; array[i] == t) like for primitive arrays
2. t \in array <==> (\exists int i; 0 <= i < array.length; Objects.equals(array[i], t))

For practical and theoretical reasons, I'd favour 1. The second can still be Arrays.asList(array).contains(t).

[wadoon]

I agree with Gary. Actually, I would even say that we formally introduce a ghost field keys of type \seq or JMLList into the array types. So a backslash would actually not even be appropriate.

I do not quite get your question, Alexander @wadoon. Does my explanation above answer the question?

There was no question. There was just findings that we a making rag rug, without having the proper skeleton.

ad a.keys. It does not matter how we named, I just wanted to on the safe side. But I think this is a new construct, that the JML ref defines a set of model methods.

Moreover, we are just doing the same thing that we have abandon in #5. In #5 we avoid complexity and agreed that JML annotations are all overridden and never combined for a class. Now we define a model field keys for Arrays, are these standard defined constructs also overridden by a JML file?

ad \till. What is precedence of \till (and other infix operators)? Is a \till a + 1 equal to a \till (a + 1) or (a \till a) + 1.

[mattulbrich]

Alexander, you asked "where do we book this?" above. I do not see the rag rug problem here. I see .keys similar as .length for arrays. It can be a special syntactical construct (like its brother .length in Java) or be seen as said implicit model field because that is how it behaves. It's not a model method.

I do not see the connection to #5. Where are the (possibly contradicting) annotations that need to be combined?

The precedence of \till is that of ... The grammar will easily clarify this.

Btw: length is an allowed identifier in Java, so would keys remain one.

[wadoon]

@mattulbrich

It can be a special syntactical construct (like its brother .length in Java)

I hate "special syntax constructs", and .length is treated as a field which is normally resolved during type and name resolution.

or be seen as said implicit model field because that is how it behaves.

I am completely with you at this point. I see .key as a model field for all iterable types, and not as "another exceptional construct" in the JML refernece. But now, I would say we have an issue: The JML ref would define a new default model field. (As far as I know, this would be the first pre-defined model field/method.) If the user would add a JML file for the same type, would the model fields/methods defined by the JML ref be overridden?

I do not see the connection to #5. Where are the (possibly contradicting) annotations that need to be combined?

In #5, we decided on how to resolve contradictions between JML and Java files by preferring the contents of a single JML file. IMHO there could also arise contraction between JML reference, the JML and Java files, because the JML reference just pre-defines a JML file for iterable types.

[mattulbrich]

Array types cannot be respecified in .jml files. The problem does not arise for arrays. If the interface Iterable should have an equally named field could be discussed. It could then be part of the default specification and not of the language.

[wadoon]

Array types cannot be respecified in .jml files.

I do not see any technical obstacles why need to forbid this: Arrays are JVM types due to performance considerations, but behave as regular Java types.

[davidcok]

This issue is marked as a consensus candidate. But I'm not sure what the consensus is. Perhaps

• a \till b as a half-open range, with same precedence as .. However, so far .. has been seen as a syntactic construct only used in store-ref expressions a[j .. k ] and not as a first-class operator. Are we changing that?
• a.keys to represent the sequence of indices of an array. And does a.keys have a type? or are we holding for a built-in mathematical sequence type? Or is it only usable in a quantifier range as x \in a.keys so that no type needs to be user-explicit?
• x \in o where o is an Iterable or array type and means x is a value in the range of o. \quant T x; x \in o; ... has analogous semantics to for (T x: o) {} in Java

[leavens]

About .., yes, I believe that the proper way to define this is to allow it as a first class operator that constructs a mathematical sequence (value). The same would go for \till.

About .keys, I think the type should be \seq

About \in, I agree, and I believe we are agreeing to use == to compare elements for that.