Why3 is a platform for deductive program verification. It provides rich language for specification and programming called WhyML. WhyML is also used as an intermediate language for the verification of C, Java or Ada programs
0 ответов

Ошибка синтаксиса плагина frama-c wp при использовании средства проверки CVC4

С примером файла find.c я могу без проблем доказать это, используя alt-ergo по умолчанию. Но при переходе на cvc4 выдается предупреждение и синтаксическая ошибка. Вот код: /*@ requires 0 <= n && \valid(a+(0..n-1)); assigns \nothing; ensur…
01 ноя '18 в 23:51
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 ответ

Почему я не могу использовать Why3 API в своем коде OCaml?

Я скачал tar3 Why3 и установил с помощью make и make install-lib как указано в документации для Why3 API. Но все же, когда я делаю open Why3, ocamlc и утоп пожаловаться unbound module Why3, Может кто-нибудь, пожалуйста, помогите мне, как использоват…
08 мар '18 в 08:21
1 ответ

Сообщение "Неизвестный логический символ map.Map.const" в Why3

Я экспериментирую с Why3, следуя их руководству, но я получаю сообщение Unknown logical symbol map.Map.const для нескольких пруверов. Вот содержание теории, которую я пытаюсь доказать: theory List type list 'a = Nil | Cons 'a (list 'a) predicate mem…
08 мар '17 в 16:39
0 ответов

Как запустить чат-бота, когда я использую LogicAdpater

Почему, когда я использую логический адаптер, я не могу обучить своего чат-бота (из Python3.6)? Примеры bot = Chatbot("gol", logic_adapter=['chatterbot.logic.TimeLogicAdapter']) bot.set_trainer(ListTrainer) bot.train("hey", "how are you")}
22 авг '18 в 19:16
1 ответ

Как позвонить Why3 из командной строки, чтобы получить доступ к проверщику с альтернативами?

Мой конфигурационный файл содержит альтернативные записи для разных пруверов. Когда я выполняю подтверждение Why3 с этим проверяющим устройством, выводом Why3 является сообщение о том, что у меня в файле конфигурации более одного проверяющего с зада…
08 июн '17 в 14:50
1 ответ

Логическое сопоставление с образцом в Why3ML

В других ML-вариантах (таких как SML) можно сделать что-то вроде этого: case l of (true, _) => false | (false,true) => false | (false,false) => true Тем не менее, делая аналогичные вещи, используя Why3ML match объявление вызывает синтаксиче…
17 ноя '17 в 17:13
1 ответ

z3 4.3.2 не удается найти модель для генерируемых Why3 (выполнимых) целей

Я пытаюсь использовать внутреннюю часть Why3 Z3 для извлечения моделей, которые затем могут быть использованы для получения тестовых случаев с ошибками в программах. Тем не менее, Z3 версии 4.3.2, кажется, не может ответить sat для любой цели Why3. …
23 фев '15 в 16:54
0 ответов

Нужна помощь в определении целого числа машины

Я использую mach.int библиотека в спецификации (см. также этот вопрос), и я пытаюсь определить константу, которая имеет тип int32: let constant_out1: int32 = 1 in … Тем не менее, при анализе этого, Why3 возвращает сообщение: This term has type int, …
27 июл '17 в 23:20
0 ответов

Ошибки OCaml во время использования Why3

Я пытаюсь скомпилировать why3ide (why3-0.81) с krakatoa & jessie (why-2.33) для Windows (Cygwin). Все прошло хорошо, за исключением того, что я не могу сделать правое нижнее текстовое поле для отображения обозначений (оно всегда пустое), более того,…
02 ноя '13 в 16:07
2 ответа

Как использовать Why3 доказательства в GUI Frama-C?

Это похоже на глупый вопрос, но я в тупике. Я пытаюсь использовать Frama-C Sodium и Why3 0.86.1 (оба установлены через OPAM), чтобы доказать некоторые простые свойства. Рассмотрим эту программу (toy.c): int main(void) { char *hello = "hello world!";…
17 сен '15 в 08:57
1 ответ

Является ли библиотека mach.int частью по умолчанию для Why3?

Я пытаюсь использовать 32-разрядные целые числа в спецификации Why3 модели Simulink для Why3, и я нашел библиотеку mach.int, которая, по крайней мере, в одном месте, описана как часть стандартной библиотеки. Однако, когда я пытаюсь использовать его …
12 апр '17 в 18:50
1 ответ

Доказательство простого свойства функции над массивом

Предположим, у нас есть следующий аннотированный C-код: int a[3] = {0}; /*@ requires \valid(a+(0..2)); assigns a[0..2]; ensures \forall int j; 0 <= j < 3 ==> (a[j] == j); */ int main() { int i = 0; /*@ loop assigns i, a[0..(i-1)]; loop inva…
16 июл '15 в 09:33
2 ответа

Coq индуктивные рассуждения о ACSL индуктивных предикатов?

Можно ли использовать индукцию для индуктивных предикатов, определенных в ACSL? Рассмотрим следующий пример из руководства ACSL: struct List { int value; struct List* next; }; /*@ inductive reachable{L}(struct List* root, struct List* to) { @ case e…
08 сен '15 в 09:58
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
1 ответ

Что означает [<-] в почему?

Я использую Frama-C, Alt-Ergo и Why3 для проверки системы. Одно доказательство обязательства, сгенерированное в Frama-C и отправленное в Why3, показано ниже (это версия Why3): (p_StableRemove t_1[a_5 &lt;- x] a_1 x_1 a i_2) Я хотел бы знать, что t_1…
15 июл '15 в 19:18
1 ответ

Запуск Frama-c Neon с Джесси

Я установил Frama-C и Why3, но когда я пытаюсь запустить Frama-C, я получаю сообщение об ошибке с Jessie3. frama-c -verbose 2 [kernel] warning: cannot load plug-in `Jessie3' (incompatible with Neon-20140301). The exact failure is: error loading shar…
29 окт '14 в 10:11
0 ответов

Как правильно приостановить инвариантную проверку в Why3?

Предположим, у меня есть следующий тип: type example { mutable a : int mutable b : int } invariant { a = b } Как я могу приостановить проверку инварианта, чтобы я мог выполнить операцию, которая нарушает инвариант? Такие как: let add (t : example)(n…
23 янв '19 в 19:37
0 ответов

Сбой компиляции FromInt.v на MacOS (попытка использовать плагин wp с Coq)

Если я попробую: frama-c -val -wp -wp-rte -wp-prover coq acsl-case-study.c тогда я получаю следующую ошибку: File "/var/folders/m5/pq77jvw12md76t51_6t51vfwhptwwy/T/wp7149b4.dir/coqwp/real/FromInt.v", line 22, characters 15-32: Error: The reference R…
18 янв '18 в 15:28
1 ответ

Научиться доказывать цели предварительных условий Frama-C

У меня есть следующий пример кода: typedef struct { BYTE fs_type; /* FAT sub-type (0:Not mounted) */ BYTE drv; /* Physical drive number */ } FATFS_temp; FATFS_temp *FatFs_temp[1]; /* Pointer to the file system objects (logical drives) */ /*@ @ requi…
30 авг '14 в 08:15