How can ghost code call methods with side effects?


Ghost code may not have any effect on non-ghost state, but ghost code can have effects on ghost state. So a ghost method may modify ghost fields, as long as the specifications list the appropriate fields in the appropriate modifies clauses. The example code below demonstrates this:

  class C {
    ghost var c: int

    ghost method m(k: int)
      modifies this
      ensures c == k
      c := k;

    ghost method p() {
      var cc := new C;
      assert cc.c == 8;