Notation logique AMN et mathématique

Je ne suis pas sûr que ce soit approprié pour stackoverflow, mais je ne sais pas où demander d'autre. J'étudie la méthode B pour prouver la cohérence dans les spécifications des exigences, et j'ai un problème avec la notation mathématique logique lorsque je spécifie les pré-conditions des opérations.Notation logique AMN et mathématique

Simplifier le problème initial, j'ai une variable qui est un sous-ensemble vols du produit cartésien entre FLIGHT_NO x TEMPS x temps, où chaque membre (non, td, ta), des moyens non le numéro du vol , le jour du départ et le moment de l'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?

Source

2009-12-12 webdreamer

Stackoverflow ** est ** un forum approprié pour cette question, mais les questions de méthodes formelles (autres que subjectives où ses détracteurs pourraient exprimer leur dégoût pour eux) n'ont pas toujours reçu des réponses en temps opportun le passé. Bonne chance ... –

Voulez-vous obtenir un tel élément, ou à essai qu'un élément que vous avez satisfait à cette propriété? Je demande parce que la seconde semble une condition préalable raisonnable à une opération. Je ne connais pas la méthode B spécifiquement; J'ai regardé quelques documents, mais je ne trouve pas de référence rapide, donc cela peut être faux 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'))

Ensuite, la première est:

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

Source

2009-12-12 17:10:10

Eh bien, je suis venu avec une solution qui ressemble à vos réponses. Mais je ne trouve pas de fonction de projection dans AMN qui, étant donné que le vol réel est un sous-ensemble du jeu de huit cartésiens (et non trois), il est très difficile d'écrire ... – webdreamer

I J'ai trouvé une projection dans le logiciel que j'utilise (Atelier B), mais ce n'est que pour les relations. Dois-je faire prj2 (prj2 (vols prj2) si je veux accéder au 4ème champ de vols par exemple? Est-ce que ça marche comme des listes en Lisp? Il devrait y avoir un moyen plus simple de faire ça xD Je peux jeter un oeil dans les tableaux – webdreamer

, Je pense que vous devriez chercher à utiliser des enregistrements plutôt que des tableaux –

Pardonnez mon ignorance, je ne suis pas au courant du B-Méthode. Mais ne pourriez-vous pas utiliser le quantificateur d'unicité? Il avait l'air quelque chose comme:

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

pour tous 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 dans l'ensemble. Je ne peux pas vraiment dire si la méthode B permet la pleine puissance de la logique du premier ordre, mais je suppose que vous pourriez vous rapprocher de cela.

Source

2009-12-12 17:13:27

Note que vous ne mentionnez même pas la variable 'vols ' –

Ouais, une erreur facilement corrigeable, mais toujours une erreur, nous avons posté à peu près au même moment et quand j'ai vu le vôtre je l'ai upvoted car c'est probablement mieux que le mien. –

Il est possible de définir des fonctions dans B. Les fonctions ont des valeurs constantes et doivent être listées dans la clause ABSTRACT_CONSTANTS, et définies 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ù

un raccourci pour le produit cartésien donnant des informations de vol est introduite;

DEFINITIONS 
    FLIGHT_INFO == FLIGHT_NO * TIME * TIME

quatre constantes sont déclarées, les trois premiers sont "accesseurs", et le dernier Mappe un jeu non vide d'informations de vol pour le vol informations avec le plus grand temps de départ.

CONSTANTS 
    flight_no, flight_departure, flight_arrival, last_flight

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, j'ai utilisé différentes approches pour spécifier ces fonctions. L'un est définitionnel (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)))

Source

2017-06-29 11:47:17 dde

Notation logique AMN et mathématique

Répondre

Questions connexes