AMN e notação lógica matemática

Question

Não tenho certeza se isso é apropriado para o StackOverflow, mas não sei mais onde perguntar. Estou estudando o método B para provar a consistência nas especificações de requisitos e tenho um problema com a notação matemática lógica ao especificar as condições pré das operações.

Simplificando o problema original, eu tenho uma variável que é um subconjunto voos Do produto cartesiano entre o Flight_no X Time x Time, onde para cada membro (não, TD, TA), não significa o número do voo, o tempo de partida e o TME da chegada. Como posso obter, usando a notação lógica matemática, o elemento de voos Esse tem o maior valor de TD?

Answer 1

Você quer pegue tal elemento, ou para teste que um elemento que você tem satisfaz essa propriedade? Estou perguntando porque o segundo parece uma pré -condição sensata para uma operação. Não conheço o método B especificamente; Eu olhei para alguns documentos, mas não consigo encontrar uma referência rápida, então isso pode estar errado em alguns detalhes.

O segundo deve ficar assim (prj2 é usado para a segunda projeção):

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

Então o primeiro é:

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

Answer 2

Perdoe minha ignorância, não estou familiarizado com o método B. Mas você não poderia usar o quantificador de exclusividade? Parece algo como:

Existe um tempo TD de tal forma que para todos os tempos td ', td> td'

e

Para todos os td, td ', td' ', se td> td' 'e td'> td '' então td == td '

É claro que isso assume que existe exatamente um elemento no conjunto. Não sei dizer se o método B permite todo o poder da lógica de primeira ordem, mas presumo que você possa chegar perto disso.

Answer 3

É possível definir funções em B. funções têm valores constantes e devem ser listados na cláusula abstract_constants e definidos na cláusula de propriedades. Eu tento explicar como você pode usar esse construto para resolver seu problema.

Segue um pequeno trecho onde

1. Um atalho para o produto cartesiano que fornece informações de voo é introduzido;

DEFINITIONS
    FLIGHT_INFO == FLIGHT_NO * TIME * TIME

2. Quatro constantes são declaradas, as três primeiras são "acessadores" e os últimos mapas um conjunto não vazio de informações de voo nas informações de voo com o maior horário de partida.

CONSTANTS
    flight_no, flight_departure, flight_arrival, last_flight

3. Em seguida, essas constantes são digitadas e definidas como funções totais. Observe que a última função deve tomar como entrada um conjunto não vazio. Aqui eu costumava usar diferentes abordagens para especificar essas funções. Um é definitivo (com igualdade) e o outro é axiomático.

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