assigns clause appears unprovable
ID0001638: This issue was created automatically from Mantis Issue 1638. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001638 | Frama-C | Plug-in > wp | public | 2014-02-01 | 2014-07-17 |
| Reporter | jens | Assigned To | correnson | Resolution | open |
| Priority | urgent | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Fluorine-20130601 | Target Version | - | Fixed in Version | - |
Description :
It appears that assigns clauses of functions that modify an array cannot be verified at all. I attach a simple example of a function set_zero that sets all elements of an array to zero (file set_zero.c). Attached is also an attempt to prove the assigns clause with Coq (see file wp0.script). I do not see how from 0 <= n 0 < i one can conclude i <= n
Please, correct me if I am totally missing something.
Additional Information :
Here is my proof attempt for the assigns clause:
Proof. forward. remember a_0 as a. remember n_0 as n. remember i_0 as i. remember Mint_0 as M0. remember Mint_1 as M1.
cut (i <= n). auto with zarith.
assert(less_equal: 0 <= n). assumption. apply Zle_lt_or_eq in less_equal. rewrite or_comm in less_equal.
destruct less_equal as [equal | less]. (* case equal *) rewrite <- equal. assert (~(i <= 0)). auto with zarith. contradict H7.
(* what now ? *)
Qed.
Attachments
- set_zero.c
- pb_assigns.c <- now verified.