Non-trivial diverges clauses make you prove things twice.

[wadoon]

This issue was created at git.key-project.org where the discussions are preserved.

---

• Mantis: MT-1499
• Submitted on: 2014-10-28 by (at)mulbrich
• Updated: 2014-10-29

Description

When KeY encounters a non-trivial (i.e. neither true nor false) diverges clause,
it creates two contracts: one with <>- and one with []-modality.

The negation of the diverges condition is added as an assumption to the
<> contract, but no assumption is made for the [] case.

This implies that the cases proved in <> need to repeated in [].
Adding another assumption would reduce verification effort in such cases.

Steps to reproduce

Load the following class into KeY
class A {
    boolean div, post;

    /*@ diverges div; 
      @ ensures post;*/
    void m() {}
}

you will get 2 proof obligations which read (essentially)

   !div -> <m()> post
and 
    [m()] post

The latter should be 
   div -> [m()] post

Files

Notes

(at)grahl at 2014-10-29

An alternative PO would be [m()]post & (!div -> <m()>true). This is equivalent to the two above and easier to prove than the current version (but maybe not easier than Mattias' suggestion).

This formulation reflects more the intuition behind diverges. But Mattias' suggestion is better for proving, since it provides usable DL contracts (with nontrivial postconditions).

History

• (at)mulbrich -- (NEW_BUG) 2014-10-28

• (at)grahl -- (BUGNOTE_ADDED) 2014-10-29

• (at)grahl -- (BUGNOTE_UPDATED) 2014-10-29

Attributes

• Category: JML (semantics)
• Status: NEW
• Severity: MINOR
• OS:
• Target Version:
• Resolution: OPEN
• Priority: LOW
• Reproducibility: HAVENOTTRIED
• Platform:
• Commit: 56061ba8f523ccb3a8d58d92447c4bad60b7c372
• Build:
• Tags []
• Labels: ~JML (Semantics) ~Bug ~LOW

---

View in Mantis

---

Information:

• created_at: 2017-05-29T02:26:22.421Z
• updated_at: 2021-11-07T13:41:41.579Z
• closed_at: None (closed_by: )
• milestone:
• user_notes_count: 0