block contracts

[davidcok]

Moving a discussion from Issue#6 to here.

AW commented that KeY has difficulty with

class A {
    void m(int i) {
        /*@ loop_invariant true;
          @ ensures 3 != 2;
          @ decreases 0;
          @*/
        while(i>0) i--;
    }
}

because it sees a loop contract and then a block contract. In OpenJML I required a block contract to start with a keyword (I used 'refining') to help detect unintentional misplaced specs. But that does not solve this problem in general. But perhaps it shouldn't. In

class A {
        //@ requires i >= 0;
    void m(int i) {
        /*@ loop_invariant i >= 0;
          @ decreases i;
          @ ensures I == 0;
          @*/
        while(i>0) i--;
    }
}

is it plausible (correct?) to think of this as a loop contract preceding a (block contract + loop). Where a (block contract + loop) is still a loop, summarized by the ensures. Or in that case should the ensures be first?

class A {
        //@ requires i >= 0;
    void m(int i) {
        /*@ ensures I == 0;
                   @ loop_invariant i >= 0;
          @ decreases i;
          @*/
        while(i>0) i--;
    }
}

[leavens]

Hi David, Mattias, and all,

I wonder if the refining statements in the original JML design don't work for KeY? To me, it would be simpler to just have one kind of specification for a statement instead of both refining statements and block contracts. The following is the refining-statement syntax from the old reference manual:

refining-statement ::= refining spec-statement statement | refining generic-spec-statement-case statement

    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]

I mean the same thing by the terms ‘refining statements’ and ‘block contract’. On looking cat it, I used the same basic grammar but overall I’ve simplified the grammar in favor of some post-parsing checks, as they make error reporting and recovery easier and clearer.

On Dec 8, 2021, at 2:07 PM, Gary T. Leavens @.***> wrote:

Hi David, Mattias, and all,

I wonder if the refining statements in the original JML design don't work for KeY? To me, it would be simpler to just have one kind of specification for a statement instead of both refining statements and block contracts. The following is the refining-statement syntax from the old reference manual:

refining-statement ::= refining spec-statement statement | refining generic-spec-statement-case statement

[davidcok]

When using block contracts (a.k.a statement specs) in legacy code, I found I needed two additional features.

A block contract applies to the next statement, which is usually a block statement. In legacy code I found that I needed to write specs for a sequence of statements that were not a grammatical block. I could not change the code. Even if I could have added in { }, that would have changed the scopes of declared variables in unacceptable ways.

So I implemented a specificationL-defined block using begin - end, as in

//@ begin Sequence of Java statements //@ end The begin and end have to be paired and in the same block (and not one more nested than the other) But one can have (and I did) nested block contracts as in //@ begin Sequence of Java statements //@ begin Java statements //@ end More Java statements //@ end I would say this was essential, and operated in precisely the same way that a conventional block-contract did: one can separately verify (a) the execution path that goes into the block, ending at the ‘end’, and verifying the postconditions and (b) the execution paths in which the block is replaced by the summary contained in the specification, assuming the postconditions. Breaking up the verification into two pieces made some overly big verification attempts achievable in pieces. Or alternately, it enabled isolating an unverifiable portion, or a portion to be dealt with later. But it did lead to needing one other feature. Variables could be declared between the begin and end whose scope extended beyond the end. So the block contract needed an ‘exports’ clause that listed any variables introduced in the block (and extending beyond it) Then when used as a summary, the block contract simply includes declarations of those variables. Their properties are expressed in the postconditions. As in //@ exports int n; // grammatically this looks like a formal parameter list //@ ensures n == 1299709 //@ begin Int n = computeNthPrimeNumber(100000); //@ end Thoughts?

[wadoon]

Sounds like an interesting concept.

From the syntactical point of view I would try to be more Java-ish:

1. I would put the variables which are subject of the contract/block in a formal parameter list, rather than an explicit export.
2. I would try to reuse brace bracket instead of begin/end.
3. I would allow a label on the JML-block for usage in \old(..., lbl)
4. I would consider using a keyword to introduce such a contract. loop_contract is also mandatory.

int n = foo();
/*@
 block_behavior(int n, int x)
 ensures n == 1337;
 requires x == 42;
 assignable x;
 */
//@ lbl : {
x = n/n*42;
//@ }

• Is this semantics identical to block contracts?
• What happens if a variable is not mentioned in the export statement?

[davidcok]

1. The variables though are output, not inputs as a formal parameter list implies. Thus my choice of 'exports'. Making the list parenthesized is OK.

2: I considered that. //@ { and //@ } are easy substitutions for begin and end. But they do imply a block with scope.

3: Though it is not in current JML, OpenJML allows labels added in annotations, in general.

a = b; //@ here: c = d;

I would consider this a separate issue and am in favor of it.

4. Strict JML already requires 'refining' to open a block contract (I should have put it my example). Though arguably something with behavior in the name would be more consistent.

[davidcok]

And, well, this is what I mean by clock contract. Is it what KeY implements?

If a variable is not mentioned in the import statement then OpenJML will give an error message upon a use of the variable after the block. On thinking about it, I suppose the list of exported variables can be determined automatically by inspection, so the exports clause could be implicit, but as this is a behavior contract being explicit about the exports is good for readability.

[leavens]

So, it seems that we would like to have something like a statement specification, like the "refining" statement of the old reference manual, but with the ability to delimit an arbitrary set of Java statements and the ability to declare (ghost) variables.

As long as the blocks involved nest properly, then I support such a generalization of refining statements, provided we deprecate refining and the loop contracts that are in KeY at the same time as we add that. I would prefer to keep the keyword refining, but block_behavior is acceptable to me.

[davidcok]

So

• the spec begins with either refining or block_behavior: either is fine with me, but the latter fits with naming of other specification cases

• do we allow multiple behaviors, connected with also?

• do we prefer //@ begin, //@ end or //@ { or //@ } - I prefer the first pair because the second implies a restriction on scope

• in the absence of the block delimiters the spec applies to the next Java statement (which might well be a block)

• the block might include ghost declarations but it might also simply capture regular Java declarations

• we still need to discuss what clauses are permitted (JML has some extra ones)

• I see this as a slight generalization of what is in KeY

• I don't understand what Gary means by deprecating loop_contracts in KeY. JML has loop contracts also. Gary are you saying that the regular loop contracts should begin with refining or block_contract? I'd rather leave loop contracts untouched (there are a lot of them already written).

[leavens]

I'm okay with all that. But I am thinking that there is no need for a loop contract feature as a block contract around the loop should work, so why do we also need loop contracts?

[davidcok]

A loop contract has very different clauses: a loop_invariant, a loop frame condition and a decreases. There are lots of those written and people are quite familiar with them. I don't think it is a good idea to change that.

If one really needed to I could see a block contract around the loop contract or a block contract on the loop block, but that would be an unlikely situation. A block contract (refining spec) has most of the regular method spec clauses, plus some abrupt ending clauses like returns and breaks and continues (with which there is little experience)

[mattulbrich]

Caution: KeY has loop contracts and loop specifications. The former having requires and ensures etc., the latter having invariants.

A block contract (refining spec) has most of the regular method spec clauses, plus some abrupt ending clauses like returns and breaks and continues (with which there is little experience)

I have used them occasionally in KeY. Mostly, they are stating the obvious; but needed for full abstraction.

[davidcok]

Mattias, can you say more about Loop contracts then. I did not see them described in The Key Book. But if they are something different than loop specs then I expect I'll agree with Gary that they should be combined into block contracts.

[mattulbrich]

This is more recent. You can find information about the work on block contracts and loop contracts in Florian's BSc thesis. https://formal.kastel.kit.edu/lanzinger/pdf/lanzingerBA2018.pdf

[davidcok]

OK. Give me some time to absorb this. On a quick first look, the discussion about splitting up proofs mirrors what I was doing about the same time in OpenJML, implemented to make proofs of legacy code achievable. The 'split' feature in OpenJML does something similar -- splits the proof at if/switch/loop branch points to treat each branch as a separate proof. The is both a proof reduction technique and a debugging technique, as it can help narrow the area to be inspected to find a specification or program bug.

[wadoon]

On the grammatical side, we do not distinguish between block contracts and loop contracts strongly. Only the leading keyword makes the difference. This implies

• Only the "normal" clauses are allowed in loop contracts:

  clause
  :
  ( ensures_clause   | requires_clause     | measured_by_clause
  | captures_clause  | diverges_clause     | working_space_clause
  | duration_clause  | when_clause         | assignable_clause | accessible_clause
  | signals_clause   | signals_only_clause | variant_function  | name_clause
  | breaks_clause    | continues_clause    | returns_clause    | separates_clause
  | determines_clause
  );

• Therefore, loop_invariant is not allowed in loop contracts. In contrast, the loop clauses

  loop_specification
  : loop_invariant
  ( loop_invariant
  | determines_clause
  | loop_separates_clause
  | loop_determines_clause
  | assignable_clause
  | variant_function)*;

• The differences/error checks are only applied later in the processing.

[flo2702]

• I would prefer refining to block_behavior since block_behavior seems like it would disallow us from using other behavior keywords on block contracts. With refining, we could still write something like refining normal_behavior.
• KeY actually has more behavior keywords for block contracts. In addition to normal_behavior or exceptional_behavior, there are return_behavior, break_behavior, and continue_behavior; the latter two can be parametrized with a label: continue_behavior(lbl) cond; There are also clause types returns, breaks, and continues to complement ensures and signals. Should these also be included in the standard? How does OpenJML deal with these termination possibilities on block contracts?
• Either syntax for specification-defined blocks seems sensible, but I wonder if the exports clause is necessary. It seems like it can always be inferred. Requiring it to be explicit raises the question about what to do if the user forgets a variable.

[wadoon]

• I would prefer refining to block_behavior since block_behavior seems like it would disallow us from using other behavior keywords on block contracts. With refining, we could still write something like refining normal_behavior.

I am not a fan of the refining keyword. For example, "refining normal_behavior" reads like the contract is a refinement of the (block) statement. But it is the other direction: the (block) statements is a refinement of the contract.

Currently, I am not aware of a better keyword.

@flo2702, note that 15.2 already contains clauses for returns, breaks, and continues.

• Either syntax for specification-defined blocks seems sensible, but I wonder if the exports clause is necessary. It seems like it can always be inferred. Requiring it to be explicit raises the question about what to do if the user forgets a variable.

I have not completely understand the export clause.

In my opinion, every specification entity should be able to be specified manually. This means, if something, like exports or assignable might be inferable, we want still the possibility to specify them explicitly.

Background. Imagine a tool pipeline. In the first steps you would like to infer implicit or un(der)-specified entries. This information must be presentable to the user (then it is good to have them in JML) and also we want to transfer them through the pipeline (from tool to tool) in standardized way.

[flo2702]

I am not a fan of the refining keyword. For example, "refining normal_behavior" reads like the contract is a refinement of the (block) statement. But it is the other direction: the (block) statements is a refinement of the contract.

Perhaps the plain and self-explanatory block_contract or statement_contract would be better.

In my opinion, every specification entity should be able to be specified manually. This means, if something, like exports or assignable might be inferable, we want still the possibility to specify them explicitly.

I agree for the other specification entities. But the exports clause simply tells us which variables that were declared in the specification-defined block are available to use after the block, and I cannot think of a use case where we would want to restrict this set instead of having all variables available. Doing that also leads to some weird consequences, e.g.

//@ exports int x;
//@ {
int x = 42;
int y = 43;
//@ }
int y = 43;

This is obviously not a correct Java program, since y is declared multiple times; but from the perspective of the symbolic execution, it's fine because the scope of the first y doesn't extend beyond the block. I know that the static checks of KeY and OpenJML both rely on the checked program being a correct Java program, which makes this problem void, but I think it still presents a source of confusion for the user. And again, I can't think of a use case where we would actually want to forbid a variable declared in a spec-defined block from being used later.

But maybe David has more insight on this.

[leavens]

We can argue over syntax endlessly, but refining has the advantage that it is already in JML and so is backwards compatible. The historical reason for it is that it fits in with the grey-box (or model program) specification idea discussed in the paper "Modular Verification of Higher-Order Methods with Mandatory Calls Specified by Model Programs" by Shaner, Leavens, and Naumann at OOPSLA 2007 (see http://doi.acm.org/10.1145/1297027.1297053). The idea is the other way around of course, that the statement's meaning refines the specification given.

Every program specified with JML should pass all of Java's static checks (first), in addition to JML's static checks.