Dafny -在循环中调用时违反修改

method example() {
    var arr := new int[5];
    for i := 0 to 5 {
        arr[i] := i; // 这里会违反修改，因为i=5时超出了数组的边界
    }
}

method example() {
    var arr := new int[5];
    for i := 0 to 4 { // 修改为4，避免越界
        arr[i] := i;
    }
}

method example() {
    var arr := new int[5];
    var sum := 0;
    for i := 0 to 4 {
        arr[i] := i;
        sum := sum + arr[i];
    }
    assert sum == 10; // 这里可能会违反修改，如果sum的计算不正确
}

method example() {
    var arr := new int[5];
    var sum := 0;
    for i := 0 to 4 {
        arr[i] := i;
        sum := sum + arr[i];
    }
    assert sum == 10; // 确保sum的计算正确
}

method example() {
    var arr := new int[5];
    var done := false;
    while (!done) {
        for i := 0 to 4 {
            if (i == 2) {
                done := true;
            }
            arr[i] := i; // 这里可能会违反修改，因为done可能在循环中途变为true
        }
    }
}

method example() {
    var arr := new int[5];
    var done := false;
    while (!done) {
        for i := 0 to 4 {
            if (i == 2) {
                done := true;
            }
            if (!done) {
                arr[i] := i; // 确保在done为false时才修改
            }
        }
    }
}