Сравнение элементов анализатора сплавов из набора - PullRequest
Новая
       86

Сравнение элементов анализатора сплавов из набора

0 голосов
/ 18 марта 2020

Краткая справка: мой проект заключается в создании компилятора, который компилирует из c -подобного языка в Alloy. Язык ввода, имеющий синтаксис, подобный c, должен поддерживать контракты . Сейчас я пытаюсь реализовать операторы if, поддерживающие операторы pre и post условие , подобные следующим: 

int x=2
if_preCondition(x>0)
if(x == 2){
   x = x + 1
}
if_postCondtion(x>0)

Проблема в том, что я немного запутался с результатами Alloy. 

sig  Number{
    arg1: Int,
}

fun addOneConditional (x : Int) : Number{
    { v : Number | 
            v.arg1 = ((x = 2 ) => x.add[1] else x)
    }
}

assert conditionalSome {
    all n: Number|  (n.arg1 = 2 ) => (some field: addOneConditional[n.arg1] | { field.arg1 = n.arg1.add[1] }) 
}

assert conditionalAll {
    all n: Number|  (n.arg1 = 2 ) => (all field: addOneConditional[n.arg1] | { field.arg1 = n.arg1.add[1] }) 
}

check conditionalSome
check conditionalAll

В приведенном выше примере conditionalAll не генерирует никаких Counterexample. Однако conditionalSome генерирует Counterexamples. Если я правильно понимаю квантификаторы all и some, то это ошибка. Потому что из математических логик c мы имеем expx expr (x) => ∃x expr (x) (т.е. Если выражение expr (x) истинно для всех значений из х тогда существует единственный х, для которого expr (x) истинно )

1 Ответ

0 голосов
/ 20 марта 2020

Во-первых, вам нужно модель ваших до, после и операций. Функции ужасны для этого, потому что они не могут , а не возвращать что-то, что указывает на сбой. Поэтому вам необходимо смоделировать операцию как предикат . Значение предиката указывает, удовлетворены ли pre / post, аргументы и возвращаемые значения могут быть смоделированы как параметры.

Насколько я понимаю, ваша операция: 

pred add[ x : Int, x' : Int ] {
  x > 0             -- pre condition
  x = 2 => 
    x'=x.plus[1] 
  else 
    x'=x
  x' > 0            -- post condition
}

В сплаве нет записываемых переменных (в Electrum), поэтому вам нужно смоделировать состояние до и после с помощью символа prime (').

Теперь мы можем использовать этот предикат для вычисления множества из решений вашей проблемы: 

fun solutions : set Int {
  { x' : Int | some x : Int | add[ x,x' ] }
}

Мы создаем множество с целыми числами, для которого у нас есть результат . Главный герой не является чем-то особенным в Alloy, это всего лишь соглашение для пост-государства. Я немного злоупотребляю здесь.

Это более чем достаточно, чтобы источник Alloy допустил ошибки, поэтому давайте проверим это. 

run { some solutions }

Если вы запустите это, вы увидите в Txt view: 

skolem $solutions={1, 3, 4, 5, 6, 7}

Это как и ожидалось. Операция add работает только для положительных чисел. Проверка . Если вход равен 2, результат равен 3. Er go, 2 никогда не может быть решением. Отметьте .

Признаюсь, меня немного смущает то, что вы делаете в своих утверждениях. Я старался точно их воспроизвести, хотя я удалил ненужные вещи, по крайней мере, я думаю, что мы ненужны. Сначала ваш some случай. Ваш код выполнял all, но затем выбирал 2. Таким образом, удалили внешнюю квантификацию и жестко закодировали 2. 

check  somen {
    some x' : solutions | 2.plus[1] = x'
}

Это действительно не дает нам никакого контрпримера. Поскольку solutions было {1, 3, 4, 5, 6, 7}, 2 + 1 = 3 находится в наборе, то есть выполняется условие some. 

check  alln {
    all x' : solutions  | 2.plus[1] = x'
}

Однако не все решения имеют 3 в качестве ответа. Если вы проверите это, я получу следующий контрпример: 

skolem $alln_x'={7}
skolem $solutions={1, 3, 4, 5, 6, 7}

Заключение . Дэниел Джексон советует не изучать Alloy с Ints. Глядя на свой класс Number, вы поняли его буквально: все еще основываете свою проблему на Ints Он имел в виду не использовать Int, не скрывать их под ковром в поле. Я понимаю, откуда приходит Даниэль, но Интсы очень привлекательны, так как мы с ними знакомы. Однако, если вы используете Ints, пусть они хотя бы используют всю свою славу и не скрывают их.

Надеюсь, это поможет.

И вся модель: 

pred add[ x : Int, x' : Int ] {
    x > 0               -- pre condition
    x = 2 => 
        x'=x.plus[1] 
    else 
        x'=x
    x' > 0              -- post condition
}   
fun solutions : set Int { { x' : Int | some x : Int | add[ x,x' ] } }

run { some solutions }
check  somen { some x' : solutions | x' = 3 }   
check  alln { all x' : solutions  | x' = 3 }
...