AMN и математическая логическая нотация
-
19-09-2019 - |
Вопрос
Я не уверен, что это подходит для stackoverflow, но я не знаю, где еще спросить.Я изучаю B-метод для доказательства соответствия спецификациям требований, и у меня возникла проблема с логико-математической нотацией при указании предварительных условий операций.
Упрощая исходную задачу, у меня есть переменная, которая является подмножеством полеты декартова произведения между FLIGHT_NO x TIME x TIME, где для каждого участника (no, td, ta) no означает номер рейса, td - время вылета и ta - время прибытия.Как я могу получить, используя математическую логическую нотацию, элемент полеты что имеет наибольшее значение для td?
Решение
Ты хочешь этого получить такой элемент, или к тест что имеющийся у вас элемент удовлетворяет этому свойству?Я спрашиваю, потому что второе кажется разумным предварительным условием для операции.Я не знаю конкретно B-Метод;Я просмотрел некоторые документы, но не могу найти краткую ссылку, так что это может быть неверно в некоторых деталях.
Второй должен выглядеть примерно так (prj2
используется для второй проекции):
HasGreatestTd(flight) = flight \in flights \and \forall flight' (flight' \in flights => prj2(flight) >= prj2(flight'))
Тогда первое - это:
flightWithGreatestTd = choice({flight | HasGreatestTd(flight)})
Другие советы
Простите мое невежество, я не знаком с B-Методом.Но не могли бы вы использовать квантификатор уникальности?Это выглядело бы примерно так:
существует время td такое, что для всех времен td', td > td'
и
для всех td, td', td", если td > td" и td' > td", то td == td'
Это, конечно, предполагает, что в наборе есть ровно один элемент.Я не могу точно сказать, допускает ли B-метод всю мощь логики первого порядка, но я предполагаю, что вы могли бы приблизиться к этому.
Можно определить функции в B.Функции имеют постоянные значения и должны быть перечислены в предложении ABSTRACT_CONSTANTS и определены в предложении PROPERTIES.Я пытаюсь объяснить, как вы можете использовать эту конструкцию для решения вашей проблемы.
Далее следует небольшой отрывок , где
- введено сокращение для декартова произведения, предоставляющего информацию о рейсе;
DEFINITIONS FLIGHT_INFO == FLIGHT_NO * TIME * TIME
- объявляются четыре константы, первые три являются "аксессуарами", а последняя сопоставляет непустой набор информации о рейсе с информацией о рейсе с наибольшим временем вылета.
CONSTANTS flight_no, flight_departure, flight_arrival, last_flight
- Затем эти константы типизируются и определяются как полные функции.Обратите внимание, что последняя функция должна принимать в качестве входных данных непустое множество.Здесь я использовал разные подходы для определения этих функций.Один из них является определяющим (с равенством), а другой - аксиоматичным.
PROPERTIES // typing flight_no: FLIGHT_INFO --> FLIGHT_NO & flight_departure: FLIGHT_INFO --> TIME & flight_arrival: FLIGHT_INFO --> TIME & last_flight : POW1(FLIGHT_INFO) --> FLIGHT_INFO & // value flight_no = %(no, dt, at).(no |-> dt |-> at : FLIGHT_INFO | no) & flight_departure = %(no, dt, at).(no |-> dt |-> at : FLIGHT_INFO | dt) & flight_arrival = %(no, dt, at).(no |-> dt |-> at : FLIGHT_INFO | at) & !fs.(fs : POW1(FLIGHT_INFO) => last_flight(fs) : fs & !(fi).(fi : FLIGHT_INFO & fi : fs => flight_departure(fi) <= flight_departure(last_flight(fs)))