Search code examples
z3verificationdafny

Dafny, replace index by value in sequences

in the Dafny tutorial at rise4fun, s[i := v] is defined for replacing the index i by v in sequence s. but using this always fails with expected method call, found expression.

for instance in the code below for swapping two indexes

var a:int :=input[j];
var b:int :=input[j-1];
input[j := b]; //expected method call, found expression
input[j-1 := a]; //expected method call, found expression

what is the correct way of using s[i := v] in a case like swapping two indexes.

Solution

  • You could write

    var a:int :=input[j];
var b:int :=input[j-1];
input := input[j:=b] ;
input := input[j-i : a];

    More succinctly, but perhaps harder to read

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