formal-methods

1зной

1ответ

Невозможно заставить классы классов работать в Lean

У меня возникли проблемы с пониманием того, как запускать использование классов типов Lean. Вот попытка небольшой пример: section the_section structure toto [class] (A : Type) := (rel : A → A → Prop)

0зной

1ответ

Как правильно создать схему Z для этого сценария?

Все примеры, которые я нашел, имели только 2 объявления such as name and date OR members and telephone. Однако мой сценарий таков: Я хотел бы создать Z-схему под названием AppointmentDB. AppointmentDB

1зной

2ответ

Каким будет число достижимых состояний, если состояния модели Petri-Net находятся в цикле

Если у меня есть модель Петри-сетки из 8 мест и 8 транзакций. В этой модели нет мертвого состояния, потому что токен находится в цикле и пройдя все 8 мест в первом цикле. Во второй и оставшейся петлях

3зной

1ответ

Неравенство рассуждения в Isabelle

У меня есть следующее простое доказательство: 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_simp

0зной

2ответ

Как вы подтверждаете завершение рекурсивной длины списка?

Предположим, у нас есть список: List = nil | Cons(car cdr:List). Обратите внимание, что я говорю о модифицируемых списках! И тривиальная рекурсивная функция длины: recursive Length(List l) = match l

0зной

1ответ

Возврат высокий или самый низкий значение Z нотации, формальный метод

Я новичок в Z нотации, Допустим, у меня есть функция F определяется как X | -> Y, , где Х представляет собой строку и Y есть число. Как я могу получить наивысшее значение Y в этой функции? Существует