Is it possible to use induction on inductive predicates defined in ACSL?
Consider the following example from the ACSL manual:
struct List {
int value;
struct List* next;
};
/*@ inductive reachable{L}(struct List* root, struct List* to) {
@ case empty{L}: \forall struct List* l; reachable(l, l);
@ case non_empty{L}: \forall struct List *l1,*l2;
@ \valid(l1) && reachable(l1->next, l2) ==> reachable(l1, l2);
@ }
*/
I am trying to prove the following lemma:
/*@ lemma next_null_reachable: \forall struct List* l;
@ \valid(l) && reachable(l, \null) ==> reachable(l->next, \null);
*/
Alt-Ergo fails here, so I resort to manual Coq reasoning:
Goal
forall (t : array Z),
forall (t_1 : farray addr addr),
forall (a : addr),
((valid_rw t a 2%Z)) ->
((P_reachable t t_1 a (null))) ->
((P_reachable t t_1 (t_1.[ (shiftfield_F_List_next a) ]) (null))).
But when I Search P_reachable, I find only two axioms generated:
Q_non_empty:
forall (t : array int) (t_1 : farray addr addr) (a_1 a : addr),
valid_rw t a_1 2 ->
P_reachable t t_1 (t_1 .[ shiftfield_F_List_next a_1]) a ->
P_reachable t t_1 a_1 a
Q_empty:
forall (t : array int) (t_1 : farray addr addr) (a : addr),
P_reachable t t_1 a a
And no induction principle. So I can not apply induction P_reachable or destruct P_reachable.
I use WP plugin of frama-c version Sodium-20150201.
To reproduce, you could run frama-c -wp -wp-rte -wp-prover coqide file.c, where file.c contains the List and reachable definitions and the next_null_reachable lemma.
From the form of your goals, I'm assuming you're using the WP plugin. Indeed, it does not provide a lemma indicating that reachable is the smallest predicate verifying the two cases empty and non_empty, meaning that you can't use induction.
If I remember correctly, adding such an axiom would confuse first-order theorem provers (who would repeatedly construct instances of reachable through empty or non_empty and destruct them with the induction principle). However, the Coq output of WP could very well provide a complete translation.
A workaround is to provide an appropriate set of specialized lemmas (that will not be provable through WP) instead of the induction principle. See e.g. binary_search_proved.c in this archive.