storeref expressions

[davidcok]

The phrase store-ref expression has always seemed odd to me. It doesn't really connect to other PL literature. l-value expression would be more intuitive (to me).

I'd prefer to talk about program state, which consists of a set of (memory) locations, which are referred to by l-value expressions.

But I'd be interested in knowing what terminology is actually used in teaching these concepts.

[wadoon]

I have no opinion against store-ref. I find it very intuitive as an abbreviation of storage/reference-expression.

On the other side, l-value and r-value are commonly used in C++, but (at least in my courses) they were not prominent in the education of the Java language. Also the analogy breaks if we allow o.* and o[*] which are definitiv not a lhs expression.

I have no obstacle against a re-labeling of the store-refs, e.g., to memory location (set) expression, but I would avoid calling them l-values excessively.

[leavens]

Hi Alexander, David, and all,

I agree. It's a good point that o.I and o[*] cannot be used on the left-hand side of an assignment.

    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: Thursday, December 9, 2021 9:19 AM To: JavaModelingLanguage/RefMan @.> Cc: Subscribed @.***> Subject: Re: [JavaModelingLanguage/RefMan] storeref expressions (Issue #15)

I have no opinion against store-ref. I find it very intuitive as an abbreviation of storage/reference-expression.

On the other side, l-value and r-value are commonly used in C++, but (at least in my courses) they were not prominent in the education of the Java language. Also the analogy breaks if we allow o. and o[] which are definitiv not a lhs expression.

I have no obstacle against a re-labeling of the store-refs, e.g., to memory location (set) expression, but I would avoid calling them l-values excessively.

- 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%2F15%23issuecomment-989894587&data=04%7C01%7CLeavens%40ucf.edu%7C6b55189767da4f3a651f08d9bb1ed25c%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637746563323055657%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=qPXzBk9mx%2FKShX%2BFnWJ6nQfS0%2Fnf2T9y3lY95LT4Twk%3D&reserved=0, or unsubscribehttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAC53NPMNYVBCJQI5OY7TWE3UQC3ETANCNFSM5JWOCBNA&data=04%7C01%7CLeavens%40ucf.edu%7C6b55189767da4f3a651f08d9bb1ed25c%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637746563323065649%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=p2fxCOp7yDFKA%2FdSXHxQJORiu1rFJQ4awMsaATb0AWE%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%7C6b55189767da4f3a651f08d9bb1ed25c%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637746563323065649%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=0zKmT8gEoip4eaPIAQlMhmdrWPOix8gqAjPquPrFXRk%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%7C6b55189767da4f3a651f08d9bb1ed25c%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637746563323075644%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=izB4ZlCiSrPzFkK7C6B4mMOqpbI246m7VEUvOCO2AMg%3D&reserved=0.

[davidcok]

True, but they stand for sets of l-values.

So Gary, are you saying you want to stick with storeref expression?

On Dec 9, 2021, at 9:21 AM, Gary T. Leavens @.***> wrote:

Hi Alexander, David, and all,

I agree. It's a good point that o.I and o[*] cannot be used on the left-hand side of an assignment.

[leavens]

Hi David and all,

Yes, I think the term "store-ref expression" is fine, and it's somewhat traditional in language references to coin new terms for notions that don't precisely match old terms.

    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: Thursday, December 9, 2021 9:36 AM To: JavaModelingLanguage/RefMan @.> Cc: Gary Leavens @.>; Comment @.> Subject: Re: [JavaModelingLanguage/RefMan] storeref expressions (Issue #15)

True, but they stand for sets of l-values.

So Gary, are you saying you want to stick with storeref expression?

On Dec 9, 2021, at 9:21 AM, Gary T. Leavens @.<mailto:@.>> wrote:

Hi Alexander, David, and all,

I agree. It's a good point that o.I and o[*] cannot be used on the left-hand side of an assignment.

- 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%2F15%23issuecomment-989909498&data=04%7C01%7CLeavens%40ucf.edu%7Cf24302e2834a489567ec08d9bb212ce8%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637746573433292189%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=WwIJpJZSXESjuDtAdkeToaJycSf9vX%2BC4KkqBZU4DQI%3D&reserved=0, or unsubscribehttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAC53NPLDYZT72ET6CRCGCY3UQC5DZANCNFSM5JWOCBNA&data=04%7C01%7CLeavens%40ucf.edu%7Cf24302e2834a489567ec08d9bb212ce8%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637746573433302188%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=cSK09FfnR05QDQpNho8MmClQJN%2F%2FY6YIiv%2FHLJ1pRDY%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%7Cf24302e2834a489567ec08d9bb212ce8%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637746573433302188%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=PnawY0plPObmTbbSuW3hLiVfOb30kMfe%2Fe8bV5Gx260%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%7Cf24302e2834a489567ec08d9bb212ce8%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637746573433312178%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=18YPmga%2BryN3%2FpJw3SlMod6Sg6Q0YEUrAqv7eSDT3ro%3D&reserved=0.

[mattulbrich]

I am also in favor of not using l-value. From my KeY perspective, I'd say there are memory locations, location set expressions (with their own type \locset) and location expressions (referencing to a single location). storerefs is the unifying notion for the syntactical units.

[davidcok]

OK. I'll go with

(program) state -- the set of all (memory) locations (fields and array elements of classes and reachable object references)

location set expressions (type \locset) -- expressions denoting some number of locations, including the literals below and terms like \set_union (and others)

no way to express a single element of a \locset -- always at least a singleton \locset

storeref -- syntactical means to express \locset literals: x o.f o. a[1] a[1..2] a[ ] \nothing \everything

[leavens]

David's last comment is all fine with me.

[mattulbrich]

Just to verify: Locations are memory places on the heap, not on the stack. A local variable is not a location in KeY-speak.

Do you agree?

[leavens]

No, I would say that a location can also be on the stack, but your terminology is often used in the literature. For an assignable clause, we want to specify both locations on the heap and on the stack.

[mattulbrich]

Now that is an interesting subtlety.

It is easier to model location sets as "heap-only". So I'd suggest they remain such. Perhaps that is a difference between location sets and storeref in that storeref can also refer to local variables. Since location is a new term in JML, we could make it refer to heap locations.

(Local variables are only relevant inside methods and thus actually never used in dynamic frames imho. They may occur in local assignable clauses, but KeY infers them there automatically.)

[davidcok]

Now that we have statement (block) specs, I thought we needed to have local variables in location sets. The block spec summarizes the action of a bock of code, so the summary has to state what stack variables might have been assigned as well as heap locations. As long as we only had method specs this was not an issue.

[leavens]

I agree with David's thought on this.

[mattulbrich]

We need them in storerefs, yes, but not in location sets, I'd say. At least that's KeY's representation. We would have problems in having a \locset variable containing a local variable.

On major problem is that local variables have a limited lifetime, but may endure after their expiring in a location set, yield a situation of "dangling reference". Moreover, there is the problem that a local variable can exist multiple times:

class C {
   //@ ghost \locset l;

   void m(int n) {
      //@ set l = l + \locset(x);    // nevermind the concrete syntax for a singleton location set.
      if(n > 0) {
         m(n-1);
      }
   }

   void main() {
      //@ set l = \locset();  // or \set_empty to speak KeY.
      m(10);
      //@ assert \cardinality(l) == 10; // or
      //@ assert \cardinality(l) == 1;                 // (cardinality is not defined in JML, but you get its idea.)
   }
}

[wadoon]

Before we forget, here is a special behavior on storerefs in KeY.

Consider the following example:

class A {
  ... 
  //@ private \locset footprint = \locset(this.a);
  //@ assignable footprint;
  public void foo() {}
} 

If a variable occurring in a storeref expression is of type \locset, then the content of this variable is added to the storeref and not the variable itself. In the example, the assignable clause includes this.a and not this.footprint. If you want to add footprint to the assignable heap locations, you need to "quote" it by using \locset(footprint).

[leavens]

I think we may have a consensus on this. I agree with Alexander's comment about needing to "quote" footprints to prevent them from being expanded if you want to refer to the ghost field that holds a location set.

[davidcok]

The original post was about terminology -- on that there is a consensus.

We've morphed to a discussion of local variables in locsets. As I see it,

• in block contracts, assignable clauses need to be able to refer to in-scope local variables
• if locsets are a stand-in/desugaring for assignable clauses, local variables need to be a part of locsets as well, otherwise an assignable clause is not quite an equivalent to a locset expression
• but this opens up the possibility of exporting a locset containing a scope-restricted location outside of that scope
• (lambda expression rules constrain capturing/exporting local variables by requiring them to be "effectively final", by which I presume just the value is used)

I see two possible resolutions: a) allow local variables in assignable clauses (they can only be simple names), but do not allow them in locsets, so they have to be treated separately from non-local variables b) find a way to disallow having local variables in locsets be captured outside their scopes (that is, assigned to variables/fields outside their scope) To me (a) seems less aesthetically pleasing but simpler, and it is my understanding of what KeY does. And even if Key infers the local variables that are assigned, it still is appropriate to be able to write down explicitly what that inference is. For example, in a block contract

//@ refining
//@ assignable ...
{
... very long block...
}

Where the block contract is seen as a summary of the actions of the block, one wants very much for the assignable clause to list what local variables (in scope outside the block) are written to by the block.

Note though that array elements and object fields of local variables are in the heap and can very much be altered and inspected outside the scope of the local variable that originally held them. Consider the following example (you can do the same for array elements).

public class Cap {

int k = 42;

public static java.util.function.Consumer<Integer> c;
public static java.util.function.Supplier<Integer> s;

public static void m() {
  final Cap localcap = new Cap();
  c = i->{localcap.k = 10 + i;};
  s = ()->localcap.k;
}

public static void main(String... args) {
  m();
  c.accept(20);
  System.out.println(s.get());
  c.accept(100);
  System.out.println(s.get());
}
}

There is no way to refer the to Cap object that contains the k field being altered and read outside of m(), even though it still exists on the heap. To specify this I think one would need to declare a ghost variable (say ghostcap)that holds the value of localcap in order to specify what c.accept() modifies and s.get() reads. And then there would be a locset containing ghostcap.k

[mattulbrich]

I see two possible resolutions: a) allow local variables in assignable clauses (they can only be simple names), but do not allow them in locsets, so they have to be treated separately from non-local variables b) find a way to disallow having local variables in locsets be captured outside their scopes (that is, assigned to variables/fields outside their scope) To me (a) seems less aesthetically pleasing but simpler, and it is my understanding of what KeY does. And even if Key infers the local variables that are assigned, it still is appropriate to be able to write down explicitly what that inference is.

I quite like (a). Locations are memory places on the heap, that is where the whole framing business takes place, only there can be aliasing etc. The stack is harmless, so it is not in my mental model of locations, and thus the situation does not displease me particularly.

the expressions in assignable clauses would indeed be locations and local variables. But that's all I think. Our student swallow that usually quite happily.

[leavens]

I agree to (a) also, let the local variables be named explicitly.

[mattulbrich]

And even if Key infers the local variables that are assigned, it still is appropriate to be able to write down explicitly what that inference is.

And in KeY, you can write that down. It is currently bluntly ignored, so you can write a super/subset of the modified variables, nobody cares. There might be a warning in order.