reverse breaking change to array spec

This commit is contained in:
Ken McMillan 2018-06-29 12:25:00 -07:00
Родитель 44fcbe0025
Коммит ebb0917b1f
1 изменённых файлов: 2 добавлений и 2 удалений

Просмотреть файл

@ -95,8 +95,8 @@ module array(domain,range) = {
assert end(old a) <= X & X < s -> value(a,X) = v
}
after append {
# assert end(a) > end(old a) & ~(end(old a) < X & X < end(a));
assert domain.succ(end(old a),end(a));
assert end(a) > end(old a) & ~(end(old a) < X & X < end(a));
# assert domain.succ(end(old a),end(a));
assert 0 <= X & X < end(old a) -> value(a,X) = value(old a,X);
assert value(a,end(old a)) = v
}