original.name="ListAssign_Valid_5"
======
>>> main.whiley
type nint is null | int
function move(int from, int to, nint[][] list) -> nint[][]
requires from >= 0 && from < |list|
requires from + 1 < |list[from]|
requires to >= 0 && to < |list|
requires to + 1 < |list[to]|:
//
nint tmp = list[from][from + 1]
list[from][from + 1] = null
list[to][to + 1] = tmp
return list
public export method test() :
nint[][] ls = [[1, 2, 3], [4, 5, 6], [7, 8, 9]]
ls = move(0, 1, ls)
assume ls == [[1, null, 3], [4, 5, 2], [7, 8, 9]]
---