Introduce global block contracts

[wadoon]

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

---

Description

Currently a proof obligation is created for every block contract in a Java project regardless of whether the block is proved as external (global) proof obligation or during verification of the enclosing method (inline, local).

This implies that there may be open proof obligations although all relevant proofs have actually been closed.

Reproducible

Always. This has actually been the intended behaviour.

Feature Request

Implement a new modifier that can be used for block contracts that indicate whether a block is valid locally or globally. This is mainly intended as a help for the proof tool on how to verify the block contract. However, it also specifies the semantics of the block (local vs. global validity). Block contracts are mostly used for prover control anyway.

Details

Add global as a keyword for block contracts. It may be used as a modifier before the behaviour keywords. If left out, local context is implied, there is no explicit keyword for that.

If a block contract is declared global, a proof obligation will be added ("external proofs" as they are implemented currently)

Otherwise, no such obligation is created and the block is treated locally.

Example

void m(int a) {
  // ...
  /*@ global normal_behaviour
    @   requires (\forall int i; 0<=i && i<a.length; a[i]>=0);
    @   ensures (\sum int i; 0<=i && i<a.length; a[i]) >= 0;
    @   assignable \strictly_nothing;
    (at)*/
  { /* empty block */ }
  // ...
}

An external proof obligation for this global proof obligation would be generated.

Adaptations

• [ ] JML parser must support global
• [ ] Proof obligation generation for block contracts
• [ ] Strategy option still needed? adapted?
• [ ] Builtin rule is only applicable for the respective class

---

• Commit: 71c6106271fa1b9c7abb25418cc893d03e339f53

---

Information:

• created_at: 2020-05-08T12:56:56.122Z
• updated_at: 2020-08-20T11:18:53.573Z
• closed_at: None (closed_by: )
• milestone:
• user_notes_count: 3