Amn ورعاية الرياضيات

Question

لست متأكدا من أن هذا مناسب ل Stackoverflow، لكنني لا أعرف أين أسأله. أنا أدرس طريقة B لإثبات المواصفات في متطلبات المواصفات، ولدي مشكلة في تدوين الرياضيات المنطقية عند تحديد الشروط المسبقة للعمليات.

تبسيط المشكلة الأصلية، لدي متغير وهو مجموعة فرعية الرحلات الجوية من المنتج الديكارتي بين Trainer_NO X الوقت X X، حيث بالنسبة لكل عضو (لا، TD، TA)، لا يعني عدد الرحلة، TD وقت المغادرة و TME TME من الوصول. كيف يمكنني الحصول عليها، باستخدام تدوين منطق الرياضيات، عنصر الرحلات الجوية التي لديها أكبر قيمة 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. وظائف لها قيم ثابتة ويتم سردها في جملة Abstress_constants، ومع تحديدها في جملة الخصائص. أحاول شرح كيف يمكنك استخدام هذا البناء لحل مشكلتك.

يتبع مقتطفات صغيرة حيث

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