Explicit Naming for Contracts

[MarcoScaletta]

Motivation: in KeY if you want to verify the contract of a method with several behaviours you have to select it from a list of contracts that are named by default JML operation contract 0, JML operation contract 1, ..., JML operation contract n. Retrieving the right contract from this list can be trial and error. When the list is very long this becomes very annoying.

Suggested solution: extend the JML syntax in order to allow explicit names for contracts. This solution doesn't only make it easier to select immediately the right contract in KeY, but it also allows to refer to explicit names in external scripts/editors.

Example:

/*@ public normal_behavior  // <-- could be named from_true_to_false
  @ requires a == true;
  @ ensures \result == false;
  @
  @ also
  @
  @ public normal_behavior // <-- could be named from_false_to_true
  @ requires a == false;
  @ ensures \result == true;
  @*/
boolean not(boolean a) {
    return !a;
}

[MarcoScaletta]

Syntax suggestion: KIND_behavior(CONTRACT_NAME)

/*@ public normal_behavior(from_true_to_false)
  @ requires a == true;
  @ ensures \result == false;
  @
  @ also
  @
  @ public normal_behavior(from_false_to_true)
  @ requires a == false;
  @ ensures \result == true;
  @*/
boolean not(boolean a) {
    return !a;
}

[mattulbrich]

It might also make sense to be able to name individual clauses. Then error messages could say: "The postcondition 'sortedness' is not verified on method 'sort()'."

[wadoon]

I had this in #3.

The problem your suggestion is that it does not feel JMLish, and it does not work on nested contracts.

3 is currently missing a syntax proposal for named clauses. I suggest the use of the assignment expression.

//@ ensures sortedness = (\forall int i,j; 0<= i<j < a.length; a[i]<=a[j]);

Note, assignment expression are forbidden in JML-expression due to their side-effect.

[davidcok]

OpenJML takes care to preserve source location information, so verification failure messages can refer to line and column position of specification cases or clauses. I have no objection to naming them, if the syntax can be intuitive and not make parsing and error recovery harder.

OpenJML always verifies against all the behaviors (in one fell swoop), though I can see debugging advantages to being able to be selective.

• David

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

It might also make sense to be able to name individual clauses. Then error messages could say: "The postcondition 'sortedness' is not verified on method 'sort()'."

[lks9]

I wrote a paper which uses named assertions/assumptions (currently under review; though I am not considering named method contracts there). The syntax I propose is simply @ < CONTRACT_NAME > CONTRACT.

In the example I use the contract names not_true and not_false:

/*@ <not_true> public normal_behavior
  @ requires a == true;
  @ ensures \result == false;
  @
  @ also
  @
  @ <not_false> public normal_behavior
  @ requires a == false;
  @ ensures \result == true;
  @*/
boolean not(boolean a) {
    return !a;
}

This works also for non-KIND_behavior contracts like @ < XX > assume CONDITION; or @ < YY > loop_invariant .... I suppose it will not work on nested contracts. For nested specification cases, one could just add < XX > in front of each case.

I was already familiar with #3, although I did not know there is a proposal draft since 17 days, thanks for pointing it out! The #3 approach does not work for named assert/assume.

It might also make sense to be able to name individual clauses. Then error messages could say: "The postcondition 'sortedness' is not verified on method 'sort()'."

Personally, I think it is somewhat questionable to say that the postcondition is/is not verified. What we are really trying to verify is not the postcondition but the contract or specification case. And a specification case includes postcondition and precondition.

[davidcok]

Labels in Java use a colon. So does ACSL. Then

public A : normal_behavior ...

or

ensures A: o != null;

This looks natural to me, though the parser would need some lookahead and, if expression labels were allowed on subexpressions, disambiguation with ?:

[wadoon]

I would against the following /*@ <not_true> public normal_behavior ... as one could read not_true as a type parameter for the contract.

Also ensures<NAME> expr; would be blocked by KeY, as the angular brackets behind clause identifiers describe the heap in which the expression is evaluated. (A feature used on transaction management in JavaCard programs.)

I could live with David's suggestion. And I would only allow a label on top-level only. For labels on sub-expression we have \lblpos and \lblneg; (and maybe we could have neutral \lbl?).

What would be the syntax for an invariant?

//@ public A : invariant true; // or 
//@ public invariant A : true; // 

[davidcok]

OpenJML has \lbl and I use it far more than \lblpos or \lblneg. The syntax of these constructs is a nuisance, both for parsing and for editing

[lks9]

Yes, the colon notation feels JAVAish or C-ish. For the place of the A: I would think that in front of everything is more natural.

//@ A: public normal_behavior ...
//@ B: public invariant true;

[davidcok]

If anyone is thinking about an x: syntax for labeling subexpressions here is a strong caution.

1) Does a + x:b c mean a + x:(bc) or a + (x:b) * c

2) a b + c means (ab) + c. We don't want a x : b + c to be parsed as a x:(b+c)

The above argue for the label applying to just the next unary expression. But then

3) x: a + b * c

means the x: just applies to the a, not to the whole expression.

This can cause enough reader confusion that I have not advocated for (this syntax of) labels on sub-expressions

[mattulbrich]

If anyone is thinking about an x: syntax for labeling subexpressions here is a strong caution.

This can cause enough reader confusion that I have not advocated for (this syntax of) labels on sub-expressions

I do agree. the label syntax is suited for clauses / behaviours, but not within expressions. In Java, it cannot go inside expressions, too.

[leavens]

Hi Mattias, David, and all,

I agree that we shouldn't use : labels inside expressions. I should think that might cause problems with ? : expressions also.

    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 3:45 AM To: JavaModelingLanguage/RefMan @.> Cc: Subscribed @.***> Subject: Re: [JavaModelingLanguage/RefMan] Explicit Naming for Contracts (Issue #18)

If anyone is thinking about an x: syntax for labeling subexpressions here is a strong caution.

This can cause enough reader confusion that I have not advocated for (this syntax of) labels on sub-expressions

I do agree. the label syntax is suited for clauses / behaviours, but not within expressions. In Java, it cannot go inside expressions, too.

- 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%2F18%23issuecomment-992234992&data=04%7C01%7CLeavens%40ucf.edu%7C06633e10d9da480281fa08d9be14e962%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637749819310190808%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=4Wm0awZMOkHLQx8sx%2BuiWSU8lkGwGonki5un5fKQeic%3D&reserved=0, or unsubscribehttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAC53NPNGYUDZ45OTCF3AY63UQWXCNANCNFSM5JZKI5SQ&data=04%7C01%7CLeavens%40ucf.edu%7C06633e10d9da480281fa08d9be14e962%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637749819310200801%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=qEc89FBSvst4UquHL4TITiQov%2FbVA41MCS%2FaGHL4asg%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%7C06633e10d9da480281fa08d9be14e962%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637749819310200801%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=cEAdoHg%2FQ8AhLKl0P9bO8C5jhiJBI%2BVk1UEuvL9czJ8%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%7C06633e10d9da480281fa08d9be14e962%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637749819310210797%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=cHBytxnivag%2F7F0ZFE06eFZ8UY5SBCLuTsZmFFo%2FIS4%3D&reserved=0.

[leavens]

I would note that Eiffel has labels for clauses, but the more JML-ish way to name things is to make a model abstraction for them.

Still, if it's helpful, I would agree to the label : syntax on clauses and specification-cases, like normal_behavior Label1 : ... or ensures Label2 : ...

[wadoon]

Suggestion (A):

The name is put in front of the payload (terms, ...)

Examples:

• public invariant NAME0: true;

• public normal_behavior NAME1: 
  ensures   NAME2: true;
  requires  NAME3: true;
  NAME4 : {|
   assignable NAME5: o.f, NAME6: o.*;  //??
  |}

• LABEL: set NAME7 : a =  true; /??

---

Suggestion (B)

The name is the prefix of the complete JML annotation entity (incl. modifier, ...)

Examples:

• NAME0: public invariant true;

• NAME1: public normal_behavior  
  NAME2: ensures true;
  NAME3: requires  true;
  NAME4 : {|
   NAME5: assignable o.f, o.*;  //??
  |}

• LABEL: NAME7: set  a =  true; // name collides with label

[mattulbrich]

My vote: I love and would like to have the following:

public invariant nextInv: next != null ==> \invariant_for(next);

public normal_behaviour positive_case:
  requires x > 0;
  ...
and normal_behaviour negative_case:
  requires x < 0;
  ...

I also like

requires xIsPos: x>0;
requires arraySorted: (\forall ...);

I do not really like name : {| ... |}. I do not really like multiple names for/in one clause.

[davidcok]

Are these names (for behaviors and clauses) just names? Or can they be used as nicknames for expressions as well That is, if you write invariant positive: x >= 0; can you then use positive in an expression? Or is the name just for use in reporting errors or directing proofs.

[leavens]

I think they should just be names that can be used for feedback (e.g., in warnings). For abstraction, we should instead use model methods, model fields, or named meta-variables (with the old clause).

[davidcok]

Fine with me. Just checking.

[lks9]

Are these names (for behaviors and clauses) just names? Or can they be used as nicknames for expressions as well That is, if you write invariant positive: x >= 0; can you then use positive in an expression? Or is the name just for use in reporting errors or directing proofs.

Please, keep this left possible for potential JML extensions. But I think most importantly, the names as such are useful for writing, reading JML and running verification tools.

I think they should just be names that can be used for feedback (e.g., in warnings). For abstraction, we should instead use model methods, model fields, or named meta-variables (with the old clause).

We should not forget the original motivation by @MarcoScaletta!

[leavens]

I agree that JML should have abstraction mechanisms that allow naming (and parameterizing) abstractions of predicates. Is there some reason that model methods do not suffice for the use cases you and Marco have in mind? I think just naming them could work with proof tools for the original motivation, but that is somewhat outside the scope of the language design itself.

[mattulbrich]

I believe Marco's original proposal suggested to allow for contracts to be specifically selected prior to application such that not all spec cases need to be considered for a callsite. The naming mechanism would need a counter part on the proof guidance side like

//! apply bevahiour from_false_to_true;
y = not(x);

(We do this regularly in KeY via interaction. Not with the not method, but with a method with 50 lines of spec you really want to choose the contract to apply).

NB. I consider the above not a specification statement but a prove guidance (according to #28).

[MarcoScaletta]

Yes, the idea is that explicit names improve the user interaction (1) and allow customized automatic verification procedures (2):

1. It would be possible not only to easily retrieve the right contract from a (long) list but also manipulate the list of contracts, like sorting by name, hiding non explicitly name contracts etc., can really improve the user experience and make the interaction with the tools faster and less tiring.
2. It would be possible to design verification procedures like, for example: "load file_1,...,file_n, and then prove contract_name_1,..., contract_name_n" after which we are able to gather information about which contract from the list failed, and generate statistics linked to explicit names. Proofs have to be loaded in a tool via GUI only if it cannot be closed automatically or to indagate whether the size of the proof is suspiciously big. An automatic, compact, and accessible way to keep track of which contract succeeds and which does not is very useful during the specification process. Currently, this has to be done by hand and therefore is error-prone.

[lks9]

Sorry for answering so late! As I said, Marco's idea is reasonable and good but I have some own motivation, too.

The idea is to have assertions that only hold true when previous propositions holds true. I used the keyword assume for these propositions -- but know that I think about it, perhaps a new keyword propose would be more fitting. I have a simple example:

//@ propose a_le_b: a <= b;
//@ propose a_gt_b: a >  b;
a = max(a,b);
//@ assert equal: a == b assuming a_le_b;

The propositions do not need to be true in general. The assertion equal is also not true in general, but under assuming proposition a_le_b the assertion holds. assuming is also a new keyword. Also the assertion equal could used in the assuming of another assertion just like the other named propositions.

I would like to discuss this in a separate issue once I am more clear about syntax and semantics. If you have some comments, remarks, I would be eager to hear them. Also, if you know of some similar approach.

In the mean time it would be great if we could fix the syntax of the names/labels. I think the consensus goes for Suggestion A (with a few points unsolved; but for my main motivation, I only care about assertions). Suggestion A is also close to the ACSL specification I started to read now that I know about it.

[davidcok]

For the purpose of the example just above I would suggest using this syntax instead of a new kind of specification statement:

//@ ghost boolean a_le_b = a <= b;
//@ ghost boolean a_gt_b = a > b;
a = max(a,b);
//@ assert equal: a_le_b ==> (a==b)

[wadoon]

If we just add names to our constructs for the use outside of JML (in our tools), we only need to define the scope of the names (accordingly to the scope of member and local variables in Java), and then we have to go through our constructs and add the names.

If we want to make our constructs also be addressable inside JML, the naming thing becomes far more complex. Additional to the scoping, we have to add types to our constructs (leads to meta-model of JML), and discuss visibility and encapsulation.

I tend to leave the names just for the tools.

[lks9]

For the purpose of the example just above I would suggest using this syntax instead of a new kind of specification statement:

Thanks! _{I have some examples in mind where the translation into ordinary JML could get a bit more complicated. Btw. the paper (joint work with Reiner Hähnle and Richard Bubel) got accepted to FASE 2022. There we mention a different translation into ordinary JML (to verify with KeY and JBMC), and we will now carefully check which one is the best. In some sense, you could say it is only syntactic sugar but that is also true for modal logics which could be translated into first-order logic... Please, keep in mind that we only have a "New Ideas and Emerging Results" paper and I think it is not wise to issue an official JML extension proposal now; research can go on without official syntax.}

[leavens]

I'm happy with leaving the naming to the tools also.

[davidcok]

My summary of the consensus is this:

• JML permits optional naming of most constructs
• The name appears after the keyword of the construct and is followed by a colon; the name is a Java identifier.
• Names may be given to type clauses (e.g. invariant, axiom, represents, in, ...), method specification cases (behavior, normal_behavior, ...), statement specifications (assert, assume, set, ...), but not expressions. Note that all of the nameable constructs begin (aside from modifiers) with a JML keyword. The default is that any JML construct that begins with a specific keyword (including ones added in the future) can be so named.
• A "light-weight" specification case does not begin with a keyword and cannot be named.
• Declarations (including ghost or model declarations) may not themselves have a name of this sort. They already have names of their own by which they can be identified.
• These names are (at least currently) in a separate name-space and do not have types or values. They also do not have scope, as their use is determined by tools and the names have no meaning within JML. There is no restriction on duplicate names.

[davidcok]

I should add that this is specifically a tool/proof-assistance feature we are adding into standard (non-core) JML. I can see the value, though so far OpenJML has not needed such a feature.

[wadoon]

@davidcok I am fine with your conclusion.

[mattulbrich]

Consensus. See David's list above. There will be use cases, I promise :grinning: