Описание тега formal-methods
Формальные методы - это особый вид математически обоснованных методов спецификации, разработки и проверки программных и аппаратных систем.
2
ответа
Использование forall в определении рекурсивной функции
Я пытаюсь использовать функцию, чтобы определить рекурсивное определение, используя меру, и я получаю ошибку: Error: find_call_occs : Prod Я публикую весь исходный код внизу, но моя функция Function kripke_sat (M : kripke) (s : U) (p : formula) {mea…
13 дек '10 в 19:37
0
ответов
Формализуйте следующее требование в логике высказываний, используя подходящие высказывания для компонентных утверждений.
Процесс a или процесс b входит в критическую секцию, но не одновременно. Если это произойдет (то есть они одновременно входят в критическую секцию), будет выполнено прерывание. р = обработать q = процесс б r = критическая секция оператор ∨ = или опе…
06 дек '15 в 15:31
11
ответов
Могут ли функции Haskell быть доказаны / проверены на модели / проверены со свойствами корректности?
Продолжая идеи: есть ли доказуемые языки реального мира? Я не знаю как вы, но мне надоело писать код, который я не могу гарантировать. Задав вышеупомянутый вопрос и получив феноменальный ответ (спасибо всем!), Я решил сузить свой поиск доказуемого, …
02 ноя '10 в 13:12
2
ответа
event-b: возможно ли сгенерировать последовательность из... в... простых чисел через лямбду в одном выражении?
Интересно, возможно ли сгенерировать последовательность простых чисел с одним лямбда- выражением в событии b? Это то, что я до сих пор: @axm1 primeSet = {x∣ x ∈ 1‥100 ∧ ¬(∃y·y < x ∧ y > 1 ∧ x mod y = 0)} ∧ finite(primeSet) @axm2 primeSeq ∈ 1‥c…
07 фев '14 в 10:31
1
ответ
Как показать "счет" заданного отношения?
У меня есть этот код: taking’ = taking ∪ {s? → m?} Как вы видете, taking это имя для отношения, где s карты для m, Выше отношение показывает процедуру добавления (объединение), где я добавляю новый маплет к этому отношению. Тем не менее, мне нужно п…
31 июл '13 в 04:56
1
ответ
Не могу заставить классы типа работать в Lean
У меня возникли проблемы с пониманием, как вызвать использование классов типов Лин. Вот попытка на небольшом примере: section the_section structure toto [class] (A : Type) := (rel : A → A → Prop) (Hall : ∀ a, rel a a) definition P A := exists (a : A…
18 июн '16 в 13:51
1
ответ
Анализ статических значений LLVM для оптимизации
Допустим, у меня есть такая функция: int foo(int a, int b, int d, int x){ if (c) {a = 1; b = 1; d = a;} else {a = 2; b = 2; d = 1;} if (a == b) {x = d;} else {x = 0;} return x; } Эта тривиальная функция всегда возвращает 1. Компиляция с помощью clan…
08 ноя '12 в 23:13
1
ответ
Почему Coq не может сам определить симметрию равенства?
Предположим, мы пытаемся формализовать некоторые (полу) теоретико-групповые свойства, например: Section Group. Variable A: Type. Variable op: A -> A -> A. Definition is_left_neutral (e: A) := forall x: A, (op e x) = x. Definition is_right_neut…
21 сен '17 в 23:01
1
ответ
Формальные методы в C++ для безопасного программного обеспечения
Глядя на C, C имеет хорошую поддержку формальных методов, которые могут использоваться в коде (frama-c, VCC, Verifiedast). Насколько я могу судить, в C++ нет ничего похожего. Какие формальные методы доступны для рассуждения о безопасности программно…
22 июл '14 в 23:54
1
ответ
Преобразование грамматики (написанной в ANTLR) языка в формальный язык / математические обозначения
В моем текущем проекте мой начальник назначил задание выразить грамматику (написанную на ANTLR) языка, специфичного для предметной области, в формальный язык / нотации. Например, ниже приведен небольшой фрагмент кода грамматики. vocabSpec : 'resourc…
13 апр '13 в 16:42
1
ответ
Могу ли я сказать, что пространство состояний является формальной спецификацией поведения некоторой системы?
Учитывая систему и ее полное пространство состояний, могу ли я сказать, что это пространство состояний является формальной спецификацией поведения этой системы?
29 июн '16 в 05:55
1
ответ
Рассуждения о неравенстве в Изабель
У меня есть следующее простое доказательство: lemma fixes a b n :: nat assumes a: "a > n" "b > n" shows "a*b > n*n" proof - from assms show "a*b > n*n" by(simp_all add: field_simps) ERROR qed В состоянии доказательства Изабель говорит: У…
16 ноя '16 в 02:55
2
ответа
Каково будет число достижимых состояний, если модельные состояния Petri-Net находятся в цикле
Если у меня есть модель сети Петри из 8 мест и 8 транзакций. В этой модели нет мертвых состояний, потому что токен находится в цикле и проходит все 8 мест в первом цикле. Во втором и оставшихся циклах он пройдет через 6 мест, потому что токен попаде…
06 авг '15 в 05:11
2
ответа
Формальные методы - Карта цен, относящая автомобили к цене с двумя наборами BL и Fiat
У меня есть вопрос из главы 5 "Практические формальные методы с VDM" Дерека Эндрюса и Даррела INCE, на который я не был уверен, как ответить, так что вот, спасибо за любую помощь! Если цена на карте соотносит автомобили с их ценой, в набор BL входят…
29 май '14 в 17:43
6
ответов
Как узнать о формальном нисходящем подходе к архитектуре программного обеспечения?
Я разработчик программного обеспечения, заинтересованный в поиске информации. В настоящее время я работаю над своим третьим проектом поисковой системы и ОЧЕНЬ разочарован количеством стандартного кода, который пишется снова и снова, с теми же ошибка…
25 ноя '09 в 11:56
2
ответа
Требуется инструмент для получения линейной спецификации временной логики из диаграммы последовательности UML 2.0
Я работаю над проверкой согласованности модели программного обеспечения. Для этого мне нужно написать линейную временную логику для диаграммы последовательности UML 2.0. если у какого-либо органа есть какой-либо другой инструмент для того же самого,…
18 май '10 в 11:54
1
ответ
Доказательство правильности в формальной логике
Мне было интересно, если кто-нибудь может помочь мне ответить на этот вопрос. Это из предыдущей экзаменационной работы, и я смог узнать ответ, готовый к экзамену этого года. Этот вопрос кажется настолько простым, что я полностью теряюсь, что именно …
24 май '12 в 21:37
1
ответ
Где взять данные аппаратной модели?
У меня есть задача, которая состоит из 3-х одновременных самоопределенных (рекурсивных друг другу) процессов. Мне нужно каким-то образом заставить его исполниться на компьютере, но любая попытка преобразовать требование в программный код только моим…
03 сен '17 в 19:29
2
ответа
Доказательство правильности алгоритма
Мне было интересно, если кто-нибудь может помочь мне ответить на этот вопрос. Это из предыдущей экзаменационной работы, и я смог узнать ответ, готовый к экзамену этого года. Этот вопрос кажется настолько простым, что я полностью теряюсь, что именно …
27 апр '14 в 11:23
1
ответ
Получение предмета по дате в Alloy
Я застрял в этой формальной проблеме домашней работы методов, и я не уверен, что я не получаю права. У меня есть две подписи, Item и ToDo, которые определены так: sig Item { due : Date lone -> Step, category : Category lone -> Step } one sig T…
01 ноя '10 в 06:23