Продолжая идеи в: Существуют ли какие-либо доказуемые языки реального мира? Не знаю, как вы, но мне надоело писать код, который я не могу гарантировать . Задав вышеуказанный вопрос и получив феноменальный ответ (всем спасибо!), Я решил...

Я столкнулся с терминами «конкретное и символическое исполнение», когда рассматривал концепцию конколическое тестирование . (Упомянутая там статья "CUTE: Concolic модульного тестирования для C" использует этот термин в своем абстрактном разделе.)...

Я хочу написать простую функцию, которая находит наибольшее число в данном массиве целых чисел. Вот спецификация: package Maximum with SPARK_Mode is type Vector is array(Integer range <>) of Integer; function Maximum (A : in Vector)...

это доказательство дает бесконечный цикл в верификаторе Дафниса: // Status: verifier infinite loop // rotates a region of the array by one place forward method displace(arr: array<int>, start: nat, len: nat) returns (r: array<int>)...

ОБНОВЛЕНО Задачи на решение некоторых дафных задач, описанных ниже с заданным классом и соответствующими методами. Если вам нужно что-то еще, пожалуйста, скажите мне, спасибо заранее. Также обновлена ​​ссылка со всем этим кодом вrise4fun....

Можно ли выполнить формальную проверку с помощью языка HDL Chisel3? Если да, есть ли для этого программное обеспечение с открытым исходным кодом? Я знаю, что мы можем сделать формальную проверку Verilog с Yosys, но с chisel?

В последней версии 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, символы...

В Dafny lemma реализован как ghost method , поэтому он полезен только для спецификации. Однако вы не можете вызвать лемму из ghost field , например: class A { var i: int; lemma sum_is_commutative(i: int, j: int) ensures i +...

Этот код основан на статье Википедии о красно-черных деревьях. а в части о красно-черных деревьях в книге CLRS "Введение в алгоритмы". Эта программа отображает ожидаемые результаты, если я ее запускаю. Теперь я хотел бы убедиться, что это хорошо....

Как записать какие-то данные в файл в виде лога или какую-то статистику в Uppaal? Есть ли какая-то функция fprintf или какая-то FILE* , такая как у нас в C , или нет? Тот же вопрос и по чтению из файла.