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

Question

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

Упрощая исходную задачу, у меня есть переменная, которая представляет собой подмножество полетов декартового произведения между FLIGHT_NO x TIME x TIME, где для каждого члена (нет, тд, та) нет номера рейса, т. Д. Время вылета и время прибытия. Как я могу получить с помощью математической логики элемент полетов, который имеет наибольшее значение td?

Answer 1

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

Второй должен выглядеть так (prj2 используется для второй проекции):

HasGreatestTd(flight) = flight \in flights \and \forall flight' (flight' \in flights => prj2(flight) >= prj2(flight'))

Тогда первое:

flightWithGreatestTd = choice({flight | HasGreatestTd(flight)})

Answer 2

Прости мое невежество, я не знаком с B-методом. Но не могли бы вы использовать квантификатор уникальности? Это будет выглядеть примерно так:

существует время td такое, что для всех времен td', td > td'

а также

для всех td, td ', td' ', если td > td''и td' > td'', то td == td'

Это, конечно, предполагает, что в наборе есть ровно один элемент. Я не могу точно сказать, допускает ли B-метод всю мощь логики первого порядка, но я предполагаю, что вы могли бы приблизиться к этому.

Answer 3

Можно определить функции в B. Функции имеют постоянные значения и должны быть перечислены в предложении ABSTRACT_CONSTANTS и определены в предложении PROPERTIES. Я пытаюсь объяснить, как вы можете использовать эту конструкцию для решения вашей проблемы.

Следует небольшой отрывок, где

1. введен ярлык для декартового произведения, дающего информацию о полете;

DEFINITIONS
    FLIGHT_INFO == FLIGHT_NO * TIME * TIME

2. объявляются четыре константы, первые три являются "аксессорами", а последняя отображает непустой набор информации о рейсе в информацию о рейсе с наибольшим временем вылета.

CONSTANTS
    flight_no, flight_departure, flight_arrival, last_flight

3. Затем эти константы печатаются и определяются как суммарные функции. Обратите внимание, что последняя функция должна принимать в качестве входных данных непустой набор. Здесь я использовал разные подходы для определения этих функций. Один из них является определением (с равенством), а другой является аксиоматическим.

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)))