Inductive datatypes

Dec 17, 2012 at 1:44 PM
Edited Dec 17, 2012 at 2:02 PM

Hi,


Consider the following use of inductive datatypes:

#include <vcc.h>

_(
  datatype \Seq {
  case some(\integer);
  case cat(\Seq, \Seq);
  }
  )

_(
  def \integer first(\Seq t) {
    switch (t) {
    case some(i):
      return i;
    case cat(t1, t2):
      return first (t1);
    }
  }
  )

int main(int argc, char** argv) {
  //_(assert first(some(1)) == 1)

    _(assert first(cat(
                     cat(
                         cat(
                              some(1),
                              some(2))
                          , some(3))
                     , some(4)
                     )) == 1)

    return 0;
}

If I uncomment the first line,  vcc is able to derive both assertions but otherwise not. It looks as if the first line is needed as inductive hypothesis, but at the same time the definition of first() already defines the induction ... I am having trouble interpreting these results.

Can you please provide some advice on this issue? 

Thanks, best regards,

Eduardo

Editor
Dec 17, 2012 at 5:52 PM

By default, VCC only unrolls 3 levels of inductive def calls. By explicitly adding the first one, you let VCC prove the second assertion without having to unroll the last recursive call. There are several solutions:

  • The command line option /defexpansion:<n> lets you change the depth of the expansion. If n is 0, the definition is always expanded (which will most likely get z3 in a lot of trouble further down the line). In your case, /defexpansion:4 would do the trick but be warned: every depth level you add makes the size of the proof search space explode (exponentially in the number of def functions), and may be the cause of horrible performance in z3.
  • You can add a contract to the definition of first, that essentially repeats its body. For example, you could add the following contract to first: _(ensures (\exists \integer i; t = some(i)) ==> \forall \integer i; t = some(i) ==> \result == i) (and similarly for the second case). Essentially, this is twice the work for you (as opposed to writing an axiomatic version of first()), but it allows you to convince yourself that your model is consistent (and also lets VCC infer smart triggers for you).

In practice, when using such an inductive definition as specification, my experience is that recursive calls usually appear in loop invariants, and only one or two levels need to be unrolled at a time, but it probably depends on your code and your specification style. Also, you definitely shouldn't be ashamed of giving VCC lots of hints when dealing with inductive specs: SMT is notoriously bad at dealing with induction and most likely will need someone to hold its hand and guide it along in a lot of cases.

I hope this helps,
Francois

Dec 17, 2012 at 7:43 PM
Edited Dec 17, 2012 at 7:44 PM

Thanks a lot.