method IndexOf(a: array<int>, x: int) returns (i: int)
    ensures if i == -1 
      then x !in a[..]
      else 0 <= i < a.Length && a[i] == x
{
    i := 0;
    while i < a.Length 
        invariant 0 <= i <= a.Length
        invariant x !in a[..i]
    {
        if a[i] == x { return; }
        i := i + 1;
    }
    return -1;
}

method PrintArray(a: array<int>) 
{
    print "[";
    for k := 0 to a.Length
    { 
        if k > 0 
        { 
            print ", ";
        }
        print a[k]; 
    }
    print "]\n";
}
method Main() {
    var my_nums := new int[10](i => i*i);
    PrintArray(my_nums);
    var j := IndexOf(my_nums, 7);
    assert j == -1;
    print j, "\n";
    j := IndexOf(my_nums, 25);
    assert my_nums[5] == 25;
    assert j == 5;
    print j, "\n";
}