la notation et de la logique de AMN mathématiques

Question

Je ne suis pas sûr que cela est approprié pour stackoverflow, mais je ne sais pas où demander. J'étudie la méthode B pour prouver cohérence dans cahier des charges, et j'ai un problème avec la notation mathématique logique en spécifiant les conditions préalables des opérations.

Simplifier le problème d'origine, j'ai une variable qui est un sous-ensemble Vols du produit cartésien entre FLIGHT_NO x TIME x TIME, où pour chaque membre (non, td, ta), signifie pas la numéro du vol, td l'heure de départ et ta TME d'arrivée. Comment puis-je obtenir, en utilisant la notation logique mathématique, l'élément vols qui a la plus grande valeur de td?

Answer 1

Voulez-vous get un tel élément, ou test qu'un élément que vous avez satisfait à cette propriété? Je demande parce que la seconde semble une condition préalable à une opération raisonnable. Je ne sais pas la méthode B spécifique; Je l'ai regardé certains documents, mais ne peut pas trouver une référence rapide, donc cela peut se tromper dans certains détails.

La seconde devrait ressembler à ceci (prj2 est utilisé pour la deuxième projection):

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

Alors la première est:

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

Answer 2

Pardonnez mon ignorance, je ne suis pas familier avec le B-Méthode. Mais vous ne pourriez pas utiliser le quantificateur unique? Il avait l'air quelque chose comme:

il existe un temps td tel que pour tout temps td 'td> td'

et

pour tout td, td 'td '', si td> td '' et td'> td '' alors td == td '

Ceci, bien sûr, suppose qu'il y a exactement un élément de l'ensemble. Je ne peux pas vraiment dire si la méthode B-permet la pleine puissance de logique de premier ordre, mais je suppose que vous pourriez se rapprocher de cela.

Answer 3

Il est possible de définir des fonctions dans B. Les fonctions ont des valeurs constantes et doivent figurer dans la clause ABSTRACT_CONSTANTS et définie dans la clause PROPERTIES. J'essaie d'expliquer comment vous pouvez utiliser cette construction pour résoudre votre problème.

Suit un petit extrait où

1. un raccourci pour le produit cartésien donnant des informations de vol est introduit;

DEFINITIONS
    FLIGHT_INFO == FLIGHT_NO * TIME * TIME

2. quatre constantes sont déclarées, les trois premiers sont « accesseurs », et le dernier Mappe un jeu non vide d'informations de vol à l'information de vol avec la plus grande heure de départ.

CONSTANTS
    flight_no, flight_departure, flight_arrival, last_flight

3. Ensuite, ces constantes sont tapés et définies comme des fonctions au total. Notez que la dernière fonction doit prendre en entrée un ensemble non vide. Ici, je l'habitude d'approches différentes pour spécifier ces fonctions. L'un est définitionnelle (avec une égalité), et l'autre est axiomatique.

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