Dafny中s[i := v]语法报错，如何正确实现序列元素交换？

Ah, I see the issue here! Let's break this down clearly.

The core problem is that Dafny sequences are immutable, and the s[i := v] syntax is an expression—not a statement. It doesn't modify the original sequence in-place; instead, it returns a brand new sequence where the element at index i is replaced with v. Your code is trying to use this expression like a method call that alters the original sequence, which is why you're hitting that error.

Correct Usage for Swapping Elements #

To make your swap work, you need to assign the result of s[i := v] back to your input variable (since each "modification" creates a new sequence). Here's how to adjust your code:

var a:int := input[j];
var b:int := input[j-1];
// Assign the new sequence back to input to update its value
input := input[j := b];
input := input[j-1 := a];

You can also do this in a single line for brevity (since each sequence operation returns a new sequence, you can chain them):

input := input[j-1 := a][j := b];

Why This Works #

Dafny's immutable sequences are designed to make formal verification easier—since sequences can't be changed after creation, the prover can reason about their properties more reliably. Every time you use s[i := v], you're creating a copy of the original sequence with one element updated, not altering the original.

Full Example Method #

Here's a complete method that swaps two elements in a sequence, with preconditions to ensure valid indices:

method SwapElements(input: seq<int>, j: int) returns (output: seq<int>)
  requires 1 <= j < |input|  // Ensure j and j-1 are valid, non-out-of-bounds indices
{
  var a := input[j];
  var b := input[j-1];
  output := input[j := b][j-1 := a];
}

method TestSwap() {
  var mySeq := [1, 2, 3, 4];
  var swapped := SwapElements(mySeq, 2);
  assert swapped == [1, 3, 2, 4];  // Verify the swap worked as expected
}

Key Takeaways #

• s[i := v] is an expression, not a statement—always assign its result to a variable to use the updated sequence.
• Dafny sequences are immutable; there's no way to modify them in-place.
• Chaining sequence operations (s[i := x][j := y]) is a clean way to perform multiple updates in one step.

内容的提问来源于stack exchange，提问作者Amir-Mousavi