`reachable` is problematic

[mattulbrich]

The specification statement reachable is problematic since it requires an underapproximation of program behaviours to be sound while all others require an overapproximation.

Does the following verify?

class C {
  //@ normal_behaviour
  //@  ensures \result >= 0;
  static int zero() { return 0; }

  void m() {
    int i = zero();
    //@ reachable i == 42;
  }
}

It should not, but with contract-based abstraction it would, I presume.

If understand the construct correctly, I'd deprecate it since its liveness character does not fit into the language concept.

Since unreachable is also a mere syntactic sugar, I wonder whether it could not be cleared, too. (Especially with a condition, it seems difficult to grasp)

[wadoon]

reachable does not take an expression, but the problem remains.

class C {
  //@ normal_behaviour
  //@  ensures \result >= 0;
  static int zero() { return 0; }

  void m() {
    int i = zero();
    if(i == 42) { /*@ reachable; */ }
  }
}

[wadoon]

On the other side, it is an interesting feature for debugging specifications.

class C {
  //@ normal_behaviour
  //@  ensures \result >= 0;
  static int zero() { return 0; }

  void m() {
    int i = zero();
    if(i == 42) { /*@ reachable; */ }
  }
}

A similar, but I think, not identical behavior is achievable by ghost statemens.

class C {
  //@ normal_behaviour
  //@  ensures \result >= 0;
  static int zero() { return 0; }

  //ghost int i;

  //@ensures i==A_UNIQUE_VALUE;
  void m() {
    //@set i = 0;
    int i = zero();
    if(i == 42) { /*@ set i = A_UNIQUE_VALUE */ }
  }
}

[davidcok]

The point of reachable is to check feasibility -- that is are there any contradictory specifications that make the whole verification of a method trivially 'true'. OpenJML does this automatically at important points, such as at the beginning and end of the method body. An explicit reachable allows adding other check points. For example it can be used to ensure that a code branch is not dead. Another example is this: omitting a location from the frame condition in a callee, but yet claiming in an ensures clause that that location is modified can cause infeasibility that is not readily spotted by visual code review.

Mattias is correct that with modular, contract-based verification, his example succeeds.

I find 'reachable' to be an important tool and reachability testing to be essential for users, whether they realize it or not. That said, although OpenJML implements 'reachable' and 'unreachable' with optional expressions, those expressions are rarely used, can be implemented by if statements (and perhaps more clearly that way), and I would concur with omitting them from JML.

[davidcok]

Alexander's desugaring as ghost statements does not quite hit the mark because 'reachable' tests whether it is possible to reach a current execution point, not whether it always does so. And it takes more editing and is less clear about its purpose, to my reading.

[leavens]

Hi Alexander, Mattias, David, and all,

I thought in JML we had an unreachable statement, but not a reachable statement. Is "reachable" a KeY-specific?

Java prohibits unreachable statements in its semantics (see section 14.22 of the JLS: https://docs.oracle.com/javase/specs/jls/se17/html/jls-14.html#jls-14.22). So we probably shouldn't have unreachable as a statement in JML; historically this comes from ESC/Java.

It's fine to have reachable as a statement in JML, to help understand verification issues as in OpenJML. But probably reachable should not be a core feature.

    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: Tuesday, December 14, 2021 3:56 AM To: JavaModelingLanguage/RefMan @.> Cc: Subscribed @.***> Subject: Re: [JavaModelingLanguage/RefMan] reachable is problematic (Issue #27)

reachable does not take an expression, but the problem remains.

class C {

//@ normal_behaviour

//@ ensures \result >= 0;

static int zero() { return 0; }

void m() {

int i = zero();

if(i == 42) { /*@ reachable; */ }

}

}

- 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%2F27%23issuecomment-993315875&data=04%7C01%7CLeavens%40ucf.edu%7C6565d7d590b04fb29a0f08d9bedf8321%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637750689472701913%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=Vx4VZWWLE1XbrSV6o6dVyTnrP33ephajlbkVptF%2F3Ec%3D&reserved=0, or unsubscribehttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAC53NPPWXKCNTQYWU53W2G3UQ4BA7ANCNFSM5KAC7WVA&data=04%7C01%7CLeavens%40ucf.edu%7C6565d7d590b04fb29a0f08d9bedf8321%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637750689472711892%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=r6C27aSBKrFlBOyNbw7CJIJ1V3mUhqKjMLKB%2B9CceAg%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%7C6565d7d590b04fb29a0f08d9bedf8321%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637750689472711892%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=O3K4UfTXtUDyVKDH2SXO426Pmgz826U6TO8D%2BPyJU7Q%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%7C6565d7d590b04fb29a0f08d9bedf8321%7Cbb932f15ef3842ba91fcf3c59d5dd1f1%7C0%7C0%7C637750689472721875%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=GKWO%2FZkov6xYbbFlw4tQcQh1midbSe4t%2B4HBEyEY4bM%3D&reserved=0.

[davidcok]

Gary,

reachable is OpenJML and I think an essential part of verification

unreachable has been in JML. Java points out some kinds of dead code but not all. And it certainly does not point out code that is dead under the method's preconditions. It is syntactic sugar for 'assert false'. I used it in working on legacy code to check that certain error handling code was never executed under particular conditions.

I advocate for both being in JML, without the optional expressions, and not in Core.

[leavens]

Hi David and all,

I agree with you about keeping both reachable and unreachable in JML but not in the core.

    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 moved a summary comment to #25. Sorry for the error and the spam.

This one is resolved I think: JML has reachable and unreachable as Advanced features. No optional expressions.

[mattulbrich]

This discussion was way faster than me. I agree on unreachable.

I go along with reachable, but I strongly advise that we have a big disclaimer in the respective bit in the ref manual that this construct cannot (by construction) be treated soundly using ESC, nor can it be RAC'ed. It actually might be soundly treated using BMC (or similar) however.

It is thus more a sanity check indicator not a real specification artifact.

If all are ok, then feel free to close this again.

[davidcok]

I'm not sure why you say it is not sound. The claim of a reachable statement is that there is at least one pre-state that satisfies the preconditions and for which execution reaches the reachable statement. I believe that claim is, within the capabilities of the SMT solvers, correctly (soundly) determined.

It is not the ideal condition to test. I'd rather know: a) that at least one state satisfies the precondition, and b) that all states (ignoring divergence for now) satisfying the precondition will exit the program.

Feasibility checking (implicit and explicit reachable) has definitely been useful to me in practical legacy verification. But I'll grant it is also useful in sanity checking logical encodings.

[mattulbrich]

I think my example (or Alexander's variation) show that programs verify although they violate this property. If contracts are used, this is unsound by construction.

There is no run in the program in which the result value of zero is 42. The contract for zero is an overapproximation of the possible behaviours of the method, yet for the reachability check to be sound we would have to use an underapproximation of the method.

[davidcok]

Fair criticism. I did not take your point the first time around. Thus a violation of the reachable clause indicate non-feasiblity. But a non-violation may be the result of over-approximation of called methods and thus does not necessarily indicate feasibility. We can document this as firmly in the category of a specification debugging feature with caveats. If that means you would rather leave it off the JML list (while still on the OpenJML list) I'm fine with that. On the other hand if KeY uses anything similar we should name them the same.

[mattulbrich]

I'd rather exclude it from the the JML list because of the mentioned reason. It does not fit nicely. BUT it can be very helpful to find your way in a verification attempt. I do understand and see this. In this sense, this is perhaps more a prover guidance statement in the sense of #28.

[lks9]

EDIT: The following is partially based on refuted premises and can be ignored.

I also have an opinion on that:

1. I agree with David that Alexander's variation on Mattias's example succeeds. From the pre-conditions and assumptions, we could deduce that i==42 is reachable.
2. But if we would ignore the contract of zero() and just inline the method implementation than i==42 is not reachable.
3. This does not lead into inconsistencies as we cannot deduce anything from { /*@ reachable; unreachable; */ }. It just seems odd.
4. reachable does never guarantee that the branch is really reachable. There might be some unknown pre-conditions and assumptions at run-time that do not occur in the specification. Or some assumptions on input data which do not even occur in the implementation.
5. When annotating something with reachable one normally means: Given the assumptions and pre-conditions we have, the branch is reachable. So there could be other assumptions where it is not reachable.
6. reachable is currently not supported in KeY.
7. KeY does allow to print a symbolic execution tree though. So we can manually check reachability in that tree.
8. unreachable can be simulated with assert false. reachable cannot be simulated as far as I know.

So in conclusion, I see no point in deprecating reachable. On the contrary: I think we should try to support it in a future version of KeY.

[wadoon]

@lks9 There are some contradictions in your points. For example, of course you can claim to avoid method contracts and instead inline your method invocations, but this is not possible for loops. Reachability (in this case) is a liveness property, that does not perform soundly in an over-approximative contract-based verification. Therefore, you can not derive the reachability manually form the symbolic execution tree.

I think we should try to support it in a future version of KeY.

KeY is not the tool for reachability. Reachable requires the diamond as the model operator (with additional decreases and measured_by clauses) and existential quantification of the method parameters:

exists int i; pre -> \< method(i); \> reached=TRUE

You should rather use SAT/SMT-based bounded model-checking, like JJBMC (JML+JBMC), for such a task. @JonasKlamroth

---

I see reachable as an interesting feature for exploring specification and program behavior together. But I would follow @mattulbrich, especially, because JML mainly proposes a contract-based specification and verification paradigm.

[lks9]

EDIT: The following is partially based on refuted premises and can be ignored.

Yes, you are right. How about the following disclaimer after checking reachability: "CAUTION: reachable is only checked approaximatly, since it depends on assumptions and pre-conditions. You could get a different result with unrolling/inlining instead of using method/block contracts and loop invariants."

The same holds for bounded model-checking, their results would also be an approximation (for different reasons). So I am not sure if "you should rather use" is really right. The reason why it is only an approximation is of course that the problem is not decidable and this is true for nearly everything we do here. But reachability seems to be especially tricky.

I see reachable as an interesting feature for exploring specification and program behavior together. But I would follow @mattulbrich, especially, because JML mainly proposes a contract-based specification and verification paradigm.

True. I cannot say much more here. Perhaps, does someone has a better example, where we would need to check reachability rather then exploring? In any case, maybe I am lacking imagination, but I don't see how reachability could be transferred into a prover guidance statement. I think keeping it as an advanced JML feature is the best option.

[wadoon]

The same holds for bounded model-checking [...]

The difference in using bounded model-checking (BMC) is that you can easily under-approximate the reachable states, for example, by slightly increasing your execution and memory bounds. BMC often relies on SAT-solving and is therefore decidable for a given bound, resulting into a semi-decision. Note, that you only want to find one possible execution path from the pre-state to the reachable state, and therefore model search seems more natural than theorem proving.

Perhaps, does someone has a better example, where we would need to check reachability rather then exploring?

I give you one: Imagine JMLUnit, you want to check whether a certain line is reached when a specified test suite (or single test case) is executed.

[lks9]

Thank you very much. I have to apologize: I thought about it for a while and now I have a better understanding.

First, you are right about BMC: It may fail with the wrong parameters, but as it is semi-decidable, it will eventually work by increasing parameters for loop unwinding. So we can verify reachability with BMC.

Second, you are right that KeY is not the tool to do that. I don't know what I have been thinking, perhaps I somehow couldn't believe that reachability could not be easily checked in KeY.

Third, in the meantime, I learned how to verify reachability in KeY. It is a bit similar to what you wrote above.

Original:

class D {
  /*@
   public normal_behavior
   requires PRE;
   ensures POST;
  @*/ 
  void m() {
    // PLACEHOLDER
    if(i == 42) { /*@ reachable; */ }
  }
}

Modified for KeY:

class D {
  //@ ghost boolean reached;
  //@ ghost boolean reachCondition;

  /*@
   public normal_behavior
   requires PRE;
   ensures POST & (reachCondition ==> reached);
  @*/ 
  void m() {
    //@set reached = false;
    //@set reachCondition = REACH_FORMULA;
    // PLACEHOLDER
    if(i == 42) { /*@ set reached = true; */ }
  }
}

To verify reachability in KeY we would need to come up with a pre-condition REACH_FORMULA. The pre-condition does always exist, under the assumption that the execution of m() is deterministic. Additionally, we have to check that PRE & reachCondition is indeed satisfiable.

Thank you for being so patient with me.