search

JavaModelingLanguage / RefMan

4 stars 0 forks source link

old and forall #8

Closed davidcok closed 2 years ago

davidcok commented 2 years ago

I have often used the 'old' clause mixed in with 'requires' clauses. The 'old' clause is useful to extract out common subexpressions in preconditions and frame conditions, thereby making specs easier to read, easier to maintain, faster to reason about and possibly faster for RAC. In this use, old always has an initializer.

I have on occasion wished for an old that is initialized with a 'such that" predicate, meaning that the declared identifier has some (any) value that satisfies the predicate.

And I have never had occasion to use the 'forall' clause, which, it seems to me, declares a variable to have any value --- that is like my old such-that but with a predicate of 'true'.

So

wadoon commented 2 years ago

In KeY, we have no support for neither old or forall clauses. So I am not familiar with them. I remember old clause as a contract-wide let-expression which is evaluated in the previous (aka. old) state of the method.

I have on occasion wished for an old that is initialized with a 'such that" predicate, meaning that the declared identifier has some (any) value that satisfies the predicate.

This looks like the Hilbert's epsilon operator. In the KeY group, we recently discussed upon such a construct, but on the expression-level rather than as a clause. For example,

//@ ensure (\some int i; i > 0 && i < 3) == 1 || (\some int i; i > 0 && i < 3) == 2

Lately, I would have needed such a construct in JML, because we migrating our last JavaDL contracts to JML. Note, that backticks inside JML quote raw expressions in KeY's logic language. The \ifex (if-exists-then-else) is a similar construct to the epsilon operator, but also had an else-case. Maybe this is a use case for your proposal:

class String { ... 
   /*@
   public normal_behavior
      requires other != null && other instanceof java.lang.String;
      ensures \result ==
         `
            \ifEx int i;  ( i < seqLen(strContent(self))
                          & i < seqLen(strContent((String) other))
                          & int::seqGet(strContent(self), i)
                              != int::seqGet(strContent((String)other),i))
            \then (int::seqGet(strContent(self), i) - int::seqGet(strContent((String) other), i))
            \else (seqLen(strContent(self)) - seqLen(strContent((String) other)))
         `;
      assignable \strictly_nothing;
   also
   public exceptional_behavior
      requires other == null;
      signals (java.lang.NullPointerException) true;
      assignable \strictly_nothing;
    */
   public int compareTo(java.lang.Object other);
}
mattulbrich commented 2 years ago

I have never used the forall clause so far. However, I had an intuition which coupled it to ?x operators known from separation logic tools like Verifast.

For instance, I assume one would write

/*@ requires this.f |-> ?x;
   @ ensures this.f |-> ?x+1; */
void incF() { f++; }

with ?x binding the pre-value of o.f.

In JML, this would read:

/*@ forall int x;
   @ requires o.f == x;
   @ ensures o.f == x+1; */

I think the following cannot be expressed using old. Right, @davidcok? I reckon this is a nice way to specify square root.

/*@ forall int x;
   @ requires y == x*x;
   @ ensures \result == x;*/
int sqrt(int y) { ... }
mattulbrich commented 2 years ago

Adding to my last comment: Actually this "forall" may be a nice way to have ghost parameters to methods. ... Or perhaps ghost parameters would be a more natural way to describe this feature. At any rate, I think they need to be instantiated at call site. How does one do this?

davidcok commented 2 years ago

@ forall int x; @ requires y == x*x;

seems weird to me. I'd prefer forall int x | y = x*x where the | is some syntax that means 'such that' and the forall could just as well be old or let (though 'old' was originally chosen to emphasize that the expression is evaluated in the pre-state). But yes to your question, you cannot do the above with the current old-with-initializer. I think ghost parameters at the call site (do you mean ghost formal parameters?) are a different matter.

Also I'd interpret /@ forall int x; @ requires y == xx; @ ensures \result == x;*/ to mean that the result could be either positive or negative. Would you?

mattulbrich commented 2 years ago

the result could be either positive or negative

Absolutely! (same with the more conservative \result*\result == y)

I'd prefer forall int x | y = x*x

I think that 

forall int x;
requires phi;

is equivalent to forall int x | phi. Hence I'd apply Ockham's razor and ask: Why use additional syntax if it can be expressed equivalently with a standard clause?

mattulbrich commented 2 years ago

I'd have a corner case for using forall. Is this allowed? Does it make sense? If not, why not?

int f;
//@ ghost int g;

//@ forall \bigint large;
//@ ensures g == large && f == small;
void set(int small) {
   f = small;
   //@ set g = large;
}
leavens commented 2 years ago

Hi Mattias, David,

The forall clause was intended to declare universal meta-variables that scope over the whole of a specification case. It can connect both pre- and postconditions and comes from Hoare's theory.

One use for the forall clause is to eliminate use of \old() in a desugaring, converting two-state postconditions into one-state postconditions that refer to such universally quantified meta-variables.

public class Meter { private /@ spec_public @/ int counter;

//@ forall int oldcounter; //@ requires oldcounter == counter; //@ ensures counter == 1+oldcounter; public void inc() { count++; } }

I believe that this kind of universal quantification over entire specification cases gives some additional expressive power, in theory, to the specification language, and thus making a connection with the theory (David Naumann and I used this in our 2015 TOPLAS paper, for example).

However, this construct does seem like something that could be eliminated without too much harm to users.

    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: Wednesday, December 1, 2021 9:08 AM To: JavaModelingLanguage/RefMan @.> Cc: Subscribed @.***> Subject: Re: [JavaModelingLanguage/RefMan] old and forall (Issue #8)

the result could be either positive or negative

Absolutely! (same with the more conservative \result*\result == y)

I'd prefer forall int x | y = x*x

I think that

forall int x;

requires phi;

is equivalent to forall int x | phi. Hence I'd apply Ockham's razor and ask: Why use additional syntax if it can be expressed equivalently with a standard clause?

- 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%2F8%23issuecomment-983674983&data=04%7C01%7CLeavens%40ucf.edu%7C5d62a07f06994aa351a208d9b4d3ecbe%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637739644585090654%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=tMsOYni6t1c2bw%2BrMr6gtDbB0YiCJdp8tBj9BkIDG9g%3D&reserved=0, or unsubscribehttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAC53NPKY2O4O6T5C2FEZ5F3UOYT2NANCNFSM5JCXZNXQ&data=04%7C01%7CLeavens%40ucf.edu%7C5d62a07f06994aa351a208d9b4d3ecbe%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637739644585100654%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=qMGuOJKtHd8K%2F636Rrkq1tHaN5hBLpgCDjH9F9mxrkE%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%7C5d62a07f06994aa351a208d9b4d3ecbe%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637739644585100654%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=ebBWXUtxr2X2TIvchntnWLwvFdPON2LuEvqgr8jEhQM%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%7C5d62a07f06994aa351a208d9b4d3ecbe%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637739644585110643%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=lWB4DbGRPCkLJB%2FmYp7ybAIWW3F8TesPLAOjyB56Q6E%3D&reserved=0.

leavens commented 2 years ago

Hi Mattias,

I don't think that would be allowed, as I think that forall should only scope over a specification case, and so the scope wouldn't include the method's body.

    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: Wednesday, December 1, 2021 9:12 AM To: JavaModelingLanguage/RefMan @.> Cc: Subscribed @.***> Subject: Re: [JavaModelingLanguage/RefMan] old and forall (Issue #8)

I'd have a corner case for using forall. Is this allowed? Does it make sense? If not, why not?

int f;

//@ ghost int g;

//@ forall \bigint large;

//@ ensures g == large && f == small;

void set(int small) {

f = small;

//@ set g = large;

}

davidcok commented 2 years ago

1) As

forall int x; requires phi;

is equivalent to forall int i | phi So also is old int k = e; equivalent to forall int k; requires k == e;

I do concur with minimizing syntactical features, as long as they are intuitive to write and read.

2) Regarding your corner case. a) I concur with Gary that the current scope rules mean it would not pass name resolution. And having names from the specification in scope in JML annotations in the body is complicated as there can be multiple specification cases and only those with true preconditions are meaningful . b) But if the scope rules were not an issue, I'd say it could make sense, with the (somewhat convoluted) result that g is initialized with a specific but non-deterministic value; but also that the assignment to g might provoke a value out of range verification warning, depending on the arithmetic mode in force, and that might render the set statement not well-defined..

leavens commented 2 years ago

Hi David and all,

Yes, I would say that

old int k = e;

is equivalent in a specification case to

forall int k; requires k == e;

So the old clause can take on some of the functions of the forall clause in specification cases.

    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: Wednesday, December 1, 2021 9:30 AM To: JavaModelingLanguage/RefMan @.> Cc: Gary Leavens @.>; Comment @.> Subject: Re: [JavaModelingLanguage/RefMan] old and forall (Issue #8)

  1. As

forall int x; requires phi;

is equivalent to forall int i | phi So also is old int k = e; equivalent to forall int k; requires k == e;

I do concur with minimizing syntactical features, as long as they are intuitive to write and read.

  1. Regarding your corner case. a) I concur with Gary that the current scope rules mean it would not pass name resolution. And having names from the specification in scope in JML annotations in the body is complicated as there can be multiple specification cases and only those with true preconditions are meaningful . b) But if the scope rules were not an issue, I'd say it could make sense, with the (somewhat convoluted) result that g is initialized with a specific but non-deterministic value; but also that the assignment to g might provoke a value out of range verification warning, depending on the arithmetic mode in force, and that might render the set statement not well-defined..
davidcok commented 2 years ago

Actually, I think I'm going to change my opinion on all this. We've been interpreting forall as something like 'for some'. If forall means a universal quantification then neither Mattias's corner case nor

/@ forall int x; @ requires y == x x; @ ensures \result == x;/

is implementable. In the case just above for example, we are saying that for all x that satisfy y == x * x, \result == x. But more than one x satisfies the precondition and the postcondition cannot be satisfied for all of them.

Now something like this is ok, for what it is worth

/@ forall int x; @ requires k >= 0 && 0 <= x < k; @ ensures xx < \result;/ int m(int k) { return k*k; }

But perhaps by 'forall' we are meaning 'for some specific arbitrary value' ("forany") rather than 'for all possible values'

leavens commented 2 years ago

Hi David and all,

Yes, the "forall" clause is supposed to represent universal quantification, so the specification case needs to be satisfied for all possible values of the declared meta-variables.

Actually, I think I'm going to change my opinion on all this. We've been interpreting forall as something like 'for some'. If forall means a universal quantification then neither Mattias's corner case nor /@ forall int x; @ requires y == x x; @ ensures \result == x;/ is implementable. In the case just above for example, we are saying that for all x that satisfy y == x * x, \result == x. But more than one x satisfies the precondition and the postcondition cannot be satisfied for all of them.

This should mean that if we pick an x that satisfies the precondition (as otherwise the rest of the specification case doesn't need to hold), then the postcondition should be satisfied, so supposing y is a parameter that is 4, then the postcondition should be satisfied both when x is 2 and x is -2. However, that doesn't mean that the postcondition need to hold for both x == 2 and x == -2 simultaneously, it's just that for each x, if x satisfies the precondition, then it must also satisfy the postcondition.

    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: Wednesday, December 1, 2021 11:00 AM To: JavaModelingLanguage/RefMan @.> Cc: Gary Leavens @.>; Comment @.> Subject: Re: [JavaModelingLanguage/RefMan] old and forall (Issue #8)

Actually, I think I'm going to change my opinion on all this. We've been interpreting forall as something like 'for some'. If forall means a universal quantification then neither Mattias's corner case nor

/@ forall int x; @ requires y == x x; @ ensures \result == x;/

is implementable. In the case just above for example, we are saying that for all x that satisfy y == x * x, \result == x. But more than one x satisfies the precondition and the postcondition cannot be satisfied for all of them.

Now something like this is ok, for what it is worth

/@ forall int x; @ requires k >= 0 && 0 <= x < k; @ ensures xx < \result;/ int m(int k) { return k*k; }

But perhaps by 'forall' we are meaning 'for some specific arbitrary value' ("forany") rather than 'for all possible values'

- 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%2F8%23issuecomment-983784120&data=04%7C01%7CLeavens%40ucf.edu%7C6c881eaa26144a28045108d9b4e3acc0%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637739712400343256%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=3kJ0AqsKT5bfTBOxD04FD%2FeRglt45NhZ32BdgF4uN%2F4%3D&reserved=0, or unsubscribehttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAC53NPKPCWIM4E6DLJRHEUDUOZBBHANCNFSM5JCXZNXQ&data=04%7C01%7CLeavens%40ucf.edu%7C6c881eaa26144a28045108d9b4e3acc0%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637739712400343256%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=DQCShCYnkgcH8XFtin6PBZvijmmaMfK20OM4aTVsQ9Y%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%7C6c881eaa26144a28045108d9b4e3acc0%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637739712400353247%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=w16hJ0SffLAJS8Nm6vm8uPphhT15Js6ZnAvvvnY25MQ%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%7C6c881eaa26144a28045108d9b4e3acc0%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637739712400363241%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=3ipxrrSXaI5430Up0UNgmlJt1k%2BMaVEUuNiqjXov%2Bxw%3D&reserved=0.

mattulbrich commented 2 years ago

I still would like to see a really convincing use case for the general "forall".

I agree: old can be expressed with forall, and it can be desugared altogether by inlining the expression.

If forall means a universal quantification

then the square root example is indeed not implementable!

I think the forall x should translate to ∀ x. ({pre}code{post}) as a Hoare triple (if syntax would allow that).

I don't think that would be allowed, as I think that forall should only scope over a specification case, and so the scope wouldn't include the method's body.

I see. Why is this restricted?

leavens commented 2 years ago

Hi Mattias and all,

I don’t have a really convincing case for the forall clause. Indeed it was intended to translate to universal quantification over Hoare-style formulas. That was also the source of the restriction of scope to the specification.

    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: Wednesday, December 1, 2021 2:26 PM To: JavaModelingLanguage/RefMan @.> Cc: Gary Leavens @.>; Comment @.> Subject: Re: [JavaModelingLanguage/RefMan] old and forall (Issue #8)

I still would like to see a really convincing use case for the general "forall".

I agree: old can be expressed with forall, and it can be desugared altogether by inlining the expression.

If forall means a universal quantification

then the square root example is indeed not implementable!

I think the forall x should translate to ∀ x. ({pre}code{post}) as a Hoare triple (if syntax would allow that).

I don't think that would be allowed, as I think that forall should only scope over a specification case, and so the scope wouldn't include the method's body.

I see. Why is this restricted?

mattulbrich commented 2 years ago

I don’t have a really convincing case for the forall clause. Indeed it was intended to translate to universal quantification over Hoare-style formulas. That was also the source of the restriction of scope to the specification.

I see. Actually in the Hoare example the code would still in scope of the quantified variable.

leavens commented 2 years ago

Hi Mattias,

Right, so if we could declare the forall-quantified meta-variable as a ghost variable, then it would make sense to allow the use of that meta-variable in the code.

    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: Wednesday, December 1, 2021 3:11 PM To: JavaModelingLanguage/RefMan @.> Cc: Gary Leavens @.>; Comment @.> Subject: Re: [JavaModelingLanguage/RefMan] old and forall (Issue #8)

I don't have a really convincing case for the forall clause. Indeed it was intended to translate to universal quantification over Hoare-style formulas. That was also the source of the restriction of scope to the specification.

I see. Actually in the Hoare example the code would still in scope of the quantified variable.

davidcok commented 2 years ago

In thinking about scope of forall (or old for that matter) remember that there can be multiple spec cases, including inherited ones.

leavens commented 2 years ago

Yes, both old and forall would each apply to one specification case, although you could use nested specification cases to make the scope cover several specification cases.

I think that deprecating "forall" would be sensible; it's mostly there to be complete the theory. However, I think that old should remain.

mattulbrich commented 2 years ago

It took me a while to understand old as a kind of let. I understand the rationale behind the name, but it is not self-explaining.

I have not yet seen a real use case. My ideas above would be more for ghost parameters to methods. I'd like to introduce these one day perhaps, ... when we need them. They would have the same purpose, probably mean the same thing, but be way clearer since the analogon to normal parameters helps.

So consensus: old remains (needs to be implemented in KeY, but no problem, I think), forall leaves.

wadoon commented 2 years ago

It took me a while to understand old as a kind of let. I understand the rationale behind the name, but it is not self-explaining.

Maybe, we should rename it? let, ghost, and model seems good candidates.

leavens commented 2 years ago

The original motivation for the keyword old was that the abbreviation is made in the pre-state of the specification case, so that is why old seems sensible. If the syntax was let, then we users would have to remember that.

mattulbrich commented 2 years ago

I understand the rationale. (let x=y*y could imply that x is an abbreviation for y*y which it is not in the post-state)Plus: old is already established, so let's keep it. It should be well-explained, however.

leavens commented 2 years ago

I agree with Mattias completely.

davidcok commented 2 years ago

OK. Summarizing. We keep old. We deprecate forall. We have \choose for a such-that variation for the old with initialization (though the syntax is a bit clunky)