В сплаве считают
sig Очередь { ссылка : Очередь, элемент: Int }
Учтите, что у меня есть некоторый предикат predicate-1. Как мне определить область действия, когда я запускаю предикат-1 для Queue ‹=1 , int = {-3,-2,0,2}. Я не указал предикат здесь
запустить предикат-1 для 1 очереди, здесь int scope
не знаю, какой будет синтаксис для области int
Синтаксис
run predicate1 for 1 Queue, 3 Int
Областью действия целых чисел всегда является битовая ширина, поэтому вы не можете указать, что набор Int содержит ровно {-3. -2. 0,2}; вы можете указать только битовую ширину, и будут использоваться все целые числа в пределах этой битовой ширины. В моем примере выше набор Int будет содержать все целые числа от -4 до 3.
predicate1 (или напишите дополнительный предикат и выполните run {predicate1 and intLimit} for 1 Queue, 3 Int, используя модуль util/integer, чтобы ограничить используемые целые числа.
- person afsantos; 21.02.2013
