OpenJML's syntax extensions

[wadoon]

Hi David,

I am testing my jmlparser against the OpenJML examples, and I found the following constructs that I couldn't match with the JML refman:

• feasible_behavior and return_behavior
• split modifier (on loops)
• set statements with tuples set (t,v) = (v+10,t+20);
• loop_writes and loop_modifies
• //@ reachable;
• Label expression (\lbl AAA k+1)
• havoc j;
• show jj,i,addresses[jj];
• assume i*(i+1)/2 == ((i-1)*i/2) + i;
• check i >= 0;

Which of them would you suggest for the ref manual? Otherwise I would ignore them for now.

[davidcok]

Good idea to do that.

• The Label expression is part of JML
• If assume is not part of JML, it should be

As for the others

• show is an OpenJML extension that I much recommend -- it outputs the values of the given expressions in the counterexample, when the proof fails
• I much prefer writes and loop_writes to assigns/assignable. And I don't like modifies because KeY has different semantics for it
• feasible_behavior is an experiment ; I don't recall return_behavior
• split is an OpenJML extension to break up large proofs at loop, if, and statement contract
• tuples are also an experimental OpenJML addition
• havoc does what it says. It is used internally in OpenJML, so it was easy to make it visible to the user
• check is a soft assert (gives a verify error if the expression can be false, but does not then force it to be true as assert does

[wadoon]

ad split.

We are also experimenting with proof annotations/commands in KeY, but decided for a separated way. We added comments with a bang, e.g., //! cut lemma;.

[wadoon]

ad havoc, assume. I would support both, they are nice for low-level specification. assume is supported in the upcoming KeY version 2.10.0.

[wadoon]

ad show.

show seems similar to creating a ghost variable, and assign them the value

//@ show x; // vs.
//@ ghost var _saved_x = x;

How is this related to debug?

ad check.

check seems not suitable for KeY. It mainly aims for automatic prover.

[wadoon]

I also notice that OpenJML uses <- on represents clauses.

// Origin: openjml/test/gitbug590a/Sequence.java@(line 1,col 1)
model instance JMLObjectSequence theSequence;
private represents theSequence <- abstractionFunction();

JML ref manual only allows = or \such_that.

[davidcok]

show -- The point of show is that along with verification error messages you get the values of the expressions in the show statement -- without having to explore the counterexample for a specific named variable. It is highly convenient in my work.

havoc and assume are both statement specs

As for check -- I think you are misunderstanding. But I'll explain some other time.

Yes <- in represents is deprecated. There are tests in the OpenJML test suite for deprecated syntax. And note that all the tests whose names start with gitbug are derived from GitHub reported problems -- and so will not necessarily be correct.

[wadoon]

Also found in OpenJML:

recommends o != null else NullPointerException;

[wadoon]

Also found in OpenJML:

function as a modifier for methods.

Example:

public static model function pure long spec_factorial(int n){ ...

[mattulbrich]

I think we should compare KeY's and OpenJML JML-specialties and decide what exists in both worlds, what should be considered core, and what should be considered tool-specific.

I think it is totally ok to have JML and two dialects that have a few differences in supported constructs.

[wadoon]

I think it is totally ok to have JML and two dialects that have a few differences in supported constructs.

It would be nice if we could have a concept of extension points in the reference manual.

For example, we should simple allow arbitrary function with escaped identifiers in the grammar, hence \abc(x) would be syntactical allowed. For some of the constructs, the manual defines the semantics, e.g., \invariant_of(x), and other semantics are defined by the tool.

Of course, there might be extension that are not possible to collapse under a general grammar.

Possible Extension Points

• Functions with escaped identifiers and escaped identifiers
• Arbitrary quantified expression:
  • (\bsum int i; 0<i; i<n; i*2)
  • General (<JML_IDENTIFIER> <var-decl> ; <exprs>*)

• Annotation (instead of Modifiers)

  Modifiers are tricky because they occur on prominent places in the grammar. For parseability, I would only allow annotation (prefixed with an @) instead of modifier.

  • public /*@ @function */ void foo()
  • /*@ @Bounded(5,10) */ void foo = 2

Other points in the grammar are desiderable to be extended, like clauses, but these may crucial to the parsing.

[leavens]

Hi Alexander, Mattias, David, and all,

I would greatly prefer to have no dialects of JML or at least to minimize differences. This would make writing educational materials easier and make learning JML simpler for all users.

Allowing extensions at only some specified places in the grammar (extension points) would be a sensible way to keep tools more aligned than they would be otherwise, so that is a good suggestion.

    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 Alexander, David, and all,

Also found in OpenJML:

recommends o != null else NullPointerException; What is this supposed to mean?

    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: Sunday, December 12, 2021 7:26 PM To: JavaModelingLanguage/RefMan @.> Cc: Subscribed @.***> Subject: Re: [JavaModelingLanguage/RefMan] OpenJML's syntax extensions (Issue #19)

Also found in OpenJML:

recommends o != null else NullPointerException;

- 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%2F19%23issuecomment-992004062&data=04%7C01%7CLeavens%40ucf.edu%7C729e7db622864c44b0e408d9bdcf319c%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637749519872376897%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=K9ahFotucZ9B37iL3bQHDJ%2FzoSjZGyjHiA5Ylvrfr4M%3D&reserved=0, or unsubscribehttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAC53NPMWBWYJIXOP5S5QBHTUQU4S7ANCNFSM5J3UJSLA&data=04%7C01%7CLeavens%40ucf.edu%7C729e7db622864c44b0e408d9bdcf319c%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637749519872386888%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=7aAub7z4tV6%2FF%2BoQGO1RcYDU1ZCSgDi4aYytLGqOCkE%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%7C729e7db622864c44b0e408d9bdcf319c%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637749519872386888%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=qr4SgGcbJItcJiB26VTum5x44GrnydoMKL9l9sWQZAA%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%7C729e7db622864c44b0e408d9bdcf319c%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637749519872396883%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=YyuF3tU96BEEq72G%2Bmk5ZVYnMaoq9pnu%2BsBS%2BZHyT7s%3D&reserved=0.

[leavens]

Hi Alexander, and all,

ad split.

We are also experimenting with proof annotations/commands in KeY, but decided for a separated way. We added comments with a bang, e.g., //! cut lemma;. I am opposed to adding proof directives to JML's syntax, as that seems to be very tool-specific and a complication that many users could and would ignore.

    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: Saturday, December 11, 2021 11:01 PM To: JavaModelingLanguage/RefMan @.> Cc: Subscribed @.***> Subject: Re: [JavaModelingLanguage/RefMan] OpenJML's syntax extensions (Issue #19)

ad split.

We are also experimenting with proof annotations/commands in KeY, but decided for a separated way. We added comments with a bang, e.g., //! cut lemma;.

- 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%2F19%23issuecomment-991830991&data=04%7C01%7CLeavens%40ucf.edu%7C9acf279fb5e046f6075b08d9bd240e0b%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637748784819316177%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=G0O3iHtF5f3afKnJENU%2BOn6ONxeHrn6M%2BuCN2v7CZDY%3D&reserved=0, or unsubscribehttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAC53NPJFYDP5Z5ZHBNP6K2TUQQNA7ANCNFSM5J3UJSLA&data=04%7C01%7CLeavens%40ucf.edu%7C9acf279fb5e046f6075b08d9bd240e0b%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637748784819326171%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=8yyGUw4sgDy4hLJenrK43MxgboAP7UAI4LNjmUXw6HQ%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%7C9acf279fb5e046f6075b08d9bd240e0b%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637748784819326171%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=wIjoPKX1cxQZba4TUkSRaG6AkBPQjzEOL6t6aINW%2Bmw%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%7C9acf279fb5e046f6075b08d9bd240e0b%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637748784819336175%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=OMaJA5kTpBofPggaEyH4ifk12682Kbj6UPxMEQ0ZK3A%3D&reserved=0.

[davidcok]

OK. But they could certainly be tool-specific additions.

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

I am opposed to adding proof directives to JML's syntax, as that seems to be very tool-specific and a complication that many users could and would ignore.

[leavens]

Hi David, Mattias, Alexander and all,

I would prefer we just have one kind of keyword for specifying what locations are threated (could be assigned or modified) in a method or statement. The rationale behind "assignable" was that it would be a better notion for concurrency specification (as Doug Lea mentioned long ago); the usual semantics of "modifies" allows temporary changes to a location during a method's execution.

So, I have a preference for keeping the syntax as "assignable" and allowing "modifies" with the same meaning, as that will work better for concurrency and also is backwards compatible.

if havoc is only used internally, then is it needed for user-visible syntax?

Would it make sense to have some other kind of file be used to contain proof annotations?

The check statement may be reasonable. During RAC would it just issue an advisory message if the expression checked is false?

    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 11:10 AM, Gary T. Leavens @.***> wrote:

recommends o != null else NullPointerException; What is this supposed to mean?

This is a (language-agnostic) method specification clause that Rustan and I devised in a paper that we recently wrote but won’t be published until next summer. I implemented it in OpenJML as an experimental implementation to cite in the paper.

//@ recommends P else E;

Is approximately, but not quite,

//@ requires P;
//@ …
//@ also 
//@ requires !P;  // but not allowed to verified callers, unless the caller is ‘expecting’ an exception
//@ ensures false;
//@ signals_only E;

But is intended in part to deal with the situation where we really want the precondition (P) to hold but the method might be called from an unverified caller. In that case we have to have a exception handling path that is also verified. The problem is that the callee, where the specs are written, does not know the context in which it will be used or the expectations of its caller

We devised this feature to deal with the following limitation of current preconditions.

If you specify with just require P then

• a caller must satisfy P, which an unverified caller might not do
• any code in the callee that handles !P is dead code and won’t be verified

If you specify with requires P and a exceptional behavior, then

• a caller does not have to satisfy P (which is not what we think caller’s usually want) because the composite precondition of the callee is P || !P
• instead the caller has to handle a potential exception

With the recommends clause

• a verified caller must satisfy P — it is a verification error if it does not
• the callee must verify the exception handling path, so it is verified even when called by an unverified caller

There is a bit more (allow and forbid annotations), but that is the gist.

[davidcok]

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

Hi David, Mattias, Alexander and all,

I would prefer we just have one kind of keyword for specifying what locations are threated (could be assigned or modified) in a method or statement. The rationale behind "assignable" was that it would be a better notion for concurrency specification (as Doug Lea mentioned long ago); the usual semantics of "modifies" allows temporary changes to a location during a method's execution.

So, I have a preference for keeping the syntax as "assignable" and allowing "modifies" with the same meaning, as that will work better for concurrency and also is backwards compatible.

If we are going to have just one keyword, I would rather choose assigns or writes (and then reads for accessible) They are active verbs, like requires and ensures and signals (which perhaps ought to be throws)

I have been avoiding modifies because I know KeY has a different semantics which I thought we might want to incorporate into JML some day.

I realize that assignable has a history to it.

We should do something similar for loops — and I’d rather we choose a different keyword there so there is a different name between the method clause and the statement clause. Say loop_writes or loop_assigns.

if havoc is only used internally, then is it needed for user-visible syntax?

Havoc is a statement specification (like assert, set). I find it useful in summarizing otherwise too-difficult-to-verify code. But I could keep it as a OpenJML proof-assisting extension

Would it make sense to have some other kind of file be used to contain proof annotations?

The check statement may be reasonable. During RAC would it just issue an advisory message if the expression checked is false?

Yes.

[leavens]

I like the "recommends" idea and am interested in seeing the paper.

The keyword "assume" is definitely in JML.

Another thing about "assignable" (and other -able keywords) is that they give permission to the method to assign or modify locations. Since these changes are not required, "assignable" seems to capture that idea more precisely than "assigns" does. (I also believe that words ending in -able are unlikely to be chosen as identifiers by programmers.)

[mattulbrich]

I have a "being-used-to bias" on preferring assignable and follow Gary's reasoning.

recommends sounds interesting but should not be in the standard, I think