Во-первых, возможно ли это только на алгоритмах, не имеющих побочных эффектов? Во-вторых, где я могу узнать об этом процессе, какие-нибудь хорошие книги, статьи и т. Д.?

Я написал этот небольшой фрагмент кода на Haskell, чтобы выяснить, как GHC доказывает, что для натуральных чисел можно разделить только четные числа пополам: {-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeFamilies #-} module Nat where data...

Для изучения зависимых типов я переписываю свою старую игру на Haskell в Idris. В настоящее время «движок» игры использует встроенные целочисленные типы, такие как Word8 . Я хотел бы доказать некоторые леммы, касающиеся числовых свойств этих чисел...

Мне интересно, что мне нужно добавить к следующему, чтобы он прошел дафни? function mapper (input: seq<int>) : seq<(int, int)> ensures |mapper(input)| == |input| { if |input| == 0 then [] else [(0,input[0])] + mapper(input[1..])...

Здесь http://spinroot.com/spin/Man/Manual.html , написано что: В Promela есть еще один способ избежать проблемы проверки и установки: атомарные последовательности. Добавляя префикс ключевого слова atomic к последовательности операторов,...

В настоящее время я пытаюсь немного понять официальную проверку с помощью KeY инструмент для Java-программ. Вот мой код Java с ключевыми аннотациями: public class Test { public int[] a; /*@ public normal_behavior @ ensures...

seL4 — официально верифицированная операционная система. В этом pdf говорится, что "нет арифметических или других исключений" . Как это проверить? Является ли реализация перебором всех допустимых входных данных?

Не уверен, что делаю неправильно, но я думал, что reflexivity должен работать ниже, но это не так. a, b : nat H : (1 <=? a - b - 3) = true ______________________________________(1/7) is_true (0 < a - b - 3) Я также пробовал apply...

Я новичок в формальной верификации и начал формальную верификацию с SymbiYosys. Я написал некоторый код в System Verilog для изучения формальной проверки, я смог пройти BMC и прикрыть код, но он не работает (НЕИЗВЕСТНО) для индукции. У меня нет...