Дафни, замени индекс на значение в последовательностях

Question

в учебном пособии по Дафни в rise4fun , s[i := v] определено для замены индекса i на v в последовательности s.но при использовании этого всегда происходит сбой с expected method call, found expression.

, например, в приведенном ниже коде для замены двух индексов

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

, как правильно использовать s[i := v] в случае, подобном обменудва индекса.

Answer 1

Вы могли бы написать

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

Более кратко, но, возможно, труднее читать

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