Modifies seq<object>

[dreamqin68]

Hi,

I'm facing an error when attempting to modify a sequence (seq<object>). Specifically, I aim to append an item to the sequence q within the Push method.

method Push(item: object, q:seq<object>)
      modifies q
{
      q := q+[item];           
}

The error message is,

LHS of assignment must denote a mutable variable

While I understand the error, I'm unsure how to correct it. Thank you in advance!

[racko]

I assume that you want to learn about methods modifying something, so I'll not suggest that you use a function instead.

Sequences cannot be modified, but you can modify an object containing a sequence, e.g.

class Seq { var q: seq<object> }

method Push(item: object, s: Seq)
  modifies s
{
  s.q := s.q+[item];
}

or

class Seq {
  method Push(item: object)
    modifies this
  {
    q := q+[item];
  }

  var q: seq<object>
}

I'm not saying that this is good code. I'm just suggesting "minimal" modifications to make it work.

Sequences are values like integers - you cannot modify "5" either. But you can change an object with an integer field by assigning a new integer to that field. You are not changing the integer value. You are changing the object.

[dreamqin68]

Thanks a lot!