Описание тега b-method

Вопросы с тегом
3 ответа

AMN и математическая логика

Я не уверен, что это подходит для stackru, но я не знаю, где еще спросить. Я изучаю B-метод для проверки согласованности в спецификациях требований, и у меня есть проблема с нотацией логической математики при указании предварительных условий операци…
12 дек '09 в 13:46
2 ответа

Является ли B-метод альтернативой традиционным языкам программирования?

Я слышал о B-методе, который изобретен во Франции. Является ли это альтернативой традиционным языкам программирования, таким как C++ и java, или это совершенно другая вещь с разными целями?
23 фев '10 в 11:20
1 ответ

Уточнение спецификации B

Считайте, что у меня есть следующее в спецификации B: flower <: FLOWER age <: AGE owner <: OWNER Type <: flower * age Buyer : owner <-> flower Могу ли я создать уточнение следующим образом: flower <: FLOWER age <: AGE owner &…
19 июл '17 в 03:58
2 ответа

Протестируйте программу на языке b

Я не уверен, что это подходит для stackru, но я не знаю, где еще спросить. Для программы, написанной на языке b(не на языке B, предшественнике C и C++), и я хотел бы знать, хорошо ли она написана, есть ли компиляция или тест, который я могу выполнит…
01 ноя '12 в 15:37
2 ответа

Выражение правил в B-методе

Я пишу некоторые спецификации системы в B-метод. У меня есть следующие переменные, которые являются подмножествами общего набора: Первая запись: a:={x,y,z,v} b:={x,y,z} Я хочу сформулировать правило, что всякий раз, когда что-то существует в наборе …
11 июл '16 в 20:06
0 ответов

Бросок кубиков для b-метода в Ателье B

Домашнее задание требует, чтобы я разработал спецификацию B настольной игры Snakes & Ladders с помощью Atelier B. Цель игры - бросить один кубик и продвинуться вверх по доске. Цель состоит в том, чтобы завершить игру, приземлившись на последнюю …
04 янв '22 в 06:13
1 ответ

Формальная системная спецификация в AtelierB - Lhs бинарного оператора должна быть последовательностью (заданный тип POW(POW(INTEGERS * ORDERs)))

Я пытаюсь разработать спецификацию B для небольшой системы управления запасами, и я борюсь с ошибкой: Левая часть бинарного оператора должна быть последовательностью (данный тип POW(POW(INTEGERS * ORDERs))) Это моя абстрактная машина: MACHINE stock(…
11 ноя '22 в 18:42
0 ответов

Atelier B - Доказательство обязательств формата «H => vv$1 = vv$2» для vv, используемого в замене WHILE.

Я пытаюсь понять Proof Obligations этого формата:H => vv$1 = vv$2vv — это переменная, используемая в реализации в подстановке WHILE. Что означает это ЗП и как это доказать? Спасибо Вот структура проекта B: головка машин, утилиты, главная реализац…
06 янв '23 в 13:57
0 ответов

Atelier B - Доказательство простого PO в контексте цикла

Как я могу доказать, что в контексте замены WHILE выполняется следующий инвариант: INIT = FALSE => size(vv)>0? похоже, он генерирует блокирующий PO, относящийся к петле. Вот структура проекта B: голов.мч MACHINE head SETS ELEMENTS = {element0,…
08 янв '23 в 13:23
1 ответ

Использование B-метода для проверки структурированных данных

Я пытаюсь использовать B-метод как механизм формального указания структурированных данных. Как в функции, которая анализирует блок байтов, представляющий некоторые данные. Все примеры, которые я могу найти, представляют собой некоторую форму последо…
02 июн '23 в 20:34