Описание тега why3ml
1
ответ
Вызов моей собственной функции в предикате в Why3
В последней версии Why3 (1.0.0), когда я пытаюсь сделать что-то вроде следующего: let add_one (n: int) : int = n+1 predicate is_successor_of (n: int) (m: int) = m = add_one n Я получаю сообщение об ошибке в форме: файл "../something.why", строка x, …
09 июл '18 в 19:00
1
ответ
Логическое сопоставление с образцом в Why3ML
В других ML-вариантах (таких как SML) можно сделать что-то вроде этого: case l of (true, _) => false | (false,true) => false | (false,false) => true Тем не менее, делая аналогичные вещи, используя Why3ML match объявление вызывает синтаксиче…
17 ноя '17 в 17:13
0
ответов
Как правильно вводить лямбда-выражения в Why3ML?
Я хочу проверить функцию с помощью лямбды. Например: let map (t : array int) (f : array int -> array int) : array int = f t Однако это приводит к ошибке: Файл "map_reduce.mlw", строка 25, символы 4-7: это приложение создает переменную чистого тип…
23 янв '19 в 18:02
0
ответов
Как правильно приостановить инвариантную проверку в Why3?
Предположим, у меня есть следующий тип: type example { mutable a : int mutable b : int } invariant { a = b } Как я могу приостановить проверку инварианта, чтобы я мог выполнить операцию, которая нарушает инвариант? Такие как: let add (t : example)(n…
23 янв '19 в 19:37
0
ответов
Why3: имитация серверной части компилятора
Для школьного проекта мне нужно написать бэкэнд небольшого компилятора, который переводит арифметические выражения в инструкции стековой машины. Наша отправная точка - это синтаксическое дерево выражения, а не его текстовое представление (как вы мож…
12 июн '21 в 00:38
0
ответов
Why3: Как проверить список
У меня есть следующий тест, но я не уверен, как работает синтаксис why3 для списков goals, может кто поможет? goal Testexecute : (* execute (list int) (list instruction (SPush)) *) execute [(Econst 42),(Econst 21)] [SPush 2] = [(Econst 2),(Econst 42…
14 июн '21 в 01:53
0
ответов
Why3: Доказательство с индукцией
У меня есть следующие леммы: lemma compile_correct_aux : forall a : aexp, s: state, st : stack, p : prog. execute s st (compile a ++ p) = execute s (Cons (aeval s a) st) p lemma compile_correct: forall a : aexp, s: state. execute s Nil (compile a) =…
19 июн '21 в 00:28
0
ответов
Coq to Why3: с обозначениями
В Coq у меня есть следующий код: Fixpoint executeBool (state:M.t Z) (stack:list Z) (program:list insStBool) {struct program} : list Z := match program with ... | (SBSkip (S n))::l => executeBool_skip n state stack l end with executeBool_skip (n:n…
18 июн '21 в 22:14
0
ответов
Coq to Why3: Доказательство вспомогательной леммы о коррекции функций
У меня есть это доказательство в Coq: Lemma executeCompile : forall (state:M.t Z) (ins:aexp) (p:list insSt) (stack:list Z), execute state stack (compile ins ++ p) = execute state ((aeval ins state)::stack) p. Proof. intros state ins. induction ins;i…
20 июн '21 в 17:19