Ghost unary function initialized()

[MikaelMayer]

Summary

We would like to offer ours users access to a ghost construct that indicates if a local variable was initialized or not.

Background and Motivation

Loop invariants with initialization

Consider the following function:

method findSmallestIfExists(lst: seq<int>, p: int -> bool)
{
  var i := 0;
  var result : int;
  var found := false;
  while i < |lst|
    // invariant: found ==> result is initialized
  {
    if p(lst[i]) {
      if (!found || lst[i] < result) {
        found := true;
        result := lst[i];
      }
    }
    i := i + 1;
  }
  if (found) {
    print(result);
  }
}

If one could maintain the invariant that found ==> result is initialized, then this function would verify.
In Boogie, this is easy, one just need to add the invariant:

while ...
   invariant !found#0 || defass#result#0;

because the fact that result is initialized is encoded in a regular boolean variable. If only we could expose this boolean as a ghost variable in Dafny code, we would be able to solve the problem above without having to resort to option types.

Make assertion explicit

If someone writes:

method Test() {
  var a: int;
  while ... {
  }
  print a;
}

they'll get "cannot prove that a was initialized here". Normally, most assertions can be made explicit in Dafny; i.e. converted to assert statements, so that they can be lifted in invariants for examples.
Here we don't have any such mechanism so the user is left "guessing" what to do, and possibly needing to put a default value when they don't want to.

Proposed Feature

I suggest one the following unary construct, similar to allocated(x) or old(x):

• initialized(x)
• assigned(x)

Such an expression would be a ghost expressions, can be applied on local variables names only (and possibly constants in constructors?), and would be translated to their respective boolean assignment variables in Boogie.

Alternatives

Alternatively, one would be forced to initialized variables to avoid this error (which someone might want to avoid for memory issues, especially if a typical inhabitant of the type would consume a lot of memory), or use datatypes like Option to record the initialization state of a value, which would consume memory and not be as practical.

[keyboardDrummer]

The motivating example doesn't seem right to me. Can't you assign to * to result, like this?

method findSmallestIfExists(lst: seq<int>, p: int -> bool)
{
  var i := 0;
  var result : int := *;
  var found := false;
  while i < |lst|
  {
    if p(lst[i]) {
      if (!found || lst[i] < result) {
        found := true;
        result := lst[i];
      }
    }
    i := i + 1;
  }
  if (found) {
    print(result);
  }
}

Dafny accepts this program.

[MikaelMayer]

That's because it was an example with integers. Dafny does not accept this example:

method findSmallestIfExists<T>(lst: seq<T>, p: T -> bool, c: (T, T) -> bool)
{
  var i := 0;
  var result : T := *;
  var found := false;
  while i < |lst|
  {
    if p(lst[i]) {
      if (!found || c(lst[i], result)) {
        found := true;
        result := lst[i];
      }
    }
    i := i + 1;
  }
  if (found) {
    print(result);
  }
}

One way to accept this example is to define T(0), but again, as explained in Alternatives:

one would be forced to initialized variables to avoid this error (which someone might want to avoid for memory issues, especially if a typical inhabitant of the type would consume a lot of memory),

[keyboardDrummer]

One way to accept this example is to define T(0), but again, as explained in Alternatives:

one would be forced to initialized variables to avoid this error (which someone might want to avoid for memory issues, especially if a typical inhabitant of the type would consume a lot of memory),

Makes sense! Thanks