AMN e notação lógica matemática
-
19-09-2019 - |
Pergunta
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?
Solução
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)})
Outras dicas
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.
É 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
- Um atalho para o produto cartesiano que fornece informações de voo é introduzido;
DEFINITIONS FLIGHT_INFO == FLIGHT_NO * TIME * TIME
- 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
- 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)))