Wand is not correctly documented.

[sakehl]

I was trying to write a simple example of wands, and the tutorial does not help at the moment: link

This example does work, so maybe we could replace it in the tutorial.

class LinkedList {
  int value;
  LinkedList next;

}

resource state(LinkedList l) = Perm(l.value, write) ** Perm(l.next, write) **
  (l != null ==> state(l.next)) ;

  requires l != null ** state(l);
  ensures l != null ** state(l);
int sum(LinkedList l) {
  int s = 0;
  LinkedList p = l;

  package state(p) -* state(l) {

  }

    loop_invariant state(p);
    loop_invariant state(p) -* state(l);
  while(p != null) {
    LinkedList old = p;
    unfold state(p);
    s = s + p.value;
    p = p.next;
    package state(p) -* state(l) {
      fold state(old);
      apply state(old) -* state(l);
    }
  }

  apply state(p) -* state(l);
  return s;
}

[ArmborstL]

Indeed, the tutorial was written for old VerCors, where wands were encoded into methods. PR #760 changed that, instead mapping VerCors wands to Viper wands, also modifying the syntax in the process. It seems that the wiki wasn't updated accordingly. Feel free to update the wiki :) Some notes:

• create is now package, as you already realised
• use is no longer needed for the permission footprint, Viper usually figures it out automatically
• use for boolean facts can be expressed as an assert statement inside the package block if needed, IIRC. You didn't need it in your example, so I'm not sure how relevant this is (or if it really works that way). I think this is also how you guide the automatic footprint inference if that fails, but I'm not sure.
• qed became obsolete
• the "more complex expressions" no longer need to be wrapped in functions