استخدام المسندات في السبائك

Question

أحاول استخدام اثنين من المسندات (على سبيل المثال،methodsWiThSameParameters وmethodsWiThSameReturn) من واحد آخر (أي.checkOverriding) لكنني أتلقى الخطأ التالي:"لا توجد أوامر للتنفيذ".أي أدلة؟لقد حاولت أيضًا استخدام الوظائف ولكن دون جدوى، إما بسبب بناء الجملة أو لأن الوظائف لا تُرجع قيمًا منطقية.

إنها جزء من نموذج Java Metamodel المحدد في Alloy، كما علقت في بعض الأسئلة السابقة.

pred checkOverriding[]{
//check accessibility of methods involved in overriding
  no c1, c2: Class {
    c1=c2.^extend
    some m1, m2:Method |
          m1 in c1.methods && m2 in c2.methods && m1.id = m2.id 
          && methodsWiThSameParameters[m1, m2] && methodsWiThSameReturn[m1, m2] && 
               ( (m1.acc = protected && (m2.acc = private_ || #(m2.acc) = 0 )) ||
                 (m1.acc = public && (m2.acc != public || #(m2.acc) = 0 )) ||
                 (#(m1.acc) = 0 && m2.acc != private_ )
               )
      }
    }

pred methodsWiThSameParameters [first,second:Method]{
    m1.param=m2.param || (#(m1.param)=0 && #(m2.param)=0)  
}
pred methodsWiThSameReturn [first, second:Method]{
    m1.return=m2.return || (#(m1.return)=0 && #(m2.return)=0) 
}

---

شكرا لردك، السيد C.م.سبيربيرج ماكوين، ولكن أعتقد أنني لم أكن واضحًا بما فيه الكفاية في سؤالي.

يتم استدعاء المسند الخاص بي، على سبيل المثال checkOverriding، من حقيقة مثل هذه:

fact chackJavaWellFormednessRules{
    checkOverriding[]
}

وبالتالي، ما زلت لا أفهم الخطأ:"لا توجد أوامر للتنفيذ".

Answer 1

لقد حددت المسندات.لديهم دلالات تعريفية بحتة وستكون صحيحة في بعض المجموعات الفرعية من حالات النموذج وكاذبة في المجموعة الفرعية التكميلية.

إذا كنت تريد من المحلل أن يفعل أي شيء، فأنت بحاجة إلى إعطائه تعليمات؛تعليمات البحث عن مثيل للمسند هي run.لذلك سوف تريد أن تقول شيئا مثل

run methodsWithSameParameters for 3

أو

run methodsWithSameParameters for 5
run methodsWithSameReturn for 5

لاحظ أنه يمكن أن يكون لديك أكثر من تعليمات في نموذج Alloy؛يتيح لك المحلل إخباره بما يجب تنفيذه.

---

[إضافة]

محلل السبائك يتعلق بالكلمات الرئيسية run و check (و هم فقط) على أنها "أوامر".من الوصف الخاص بك، يبدو الأمر كما لو لم يكن لديك أي تكرارات لهذه الكلمات الرئيسية في النموذج.

إذا كان كل ما تريد فعله هو رؤية بعض أمثلة نموذج Alloy (للتحقق من أن النموذج ليس متناقضًا مع نفسه)، فإن أبسط طريقة هي إضافة شيء مثل ما يلي إلى النموذج:

pred show {}
run show for 3

أو، إذا كان لديك بالفعل مسند مسمى، فيمكنك ببساطة إضافة a run أمر لهذا المسند:

run checkOverriding 

ولكن بدون شرط في النموذج الذي يبدأ بأي منهما run أو check, ، ليس لديك "أمر" في النموذج.

أنت تقول أنك حددت المسند (checkOverriding) ثم تم تحديده في حقيقة أن هذا المسند راضٍ دائمًا.وهذا يرقى إلى القول بأن المسند checkOverriding دائمًا ما يكون صحيحًا (وربما يتم ذلك عن طريق صنع checkOverriding حقيقة بدلا من المسند)، ولكن لها معنى تصريحي بحت، ولا تعتبر "أمرا".إذا كنت تريد أن تتمكن Alloy من العثور على مثيلات للمسند، فيجب عليك استخدام الأمر run يأمر؛إذا كنت تريد أن تجد Alloy أمثلة مضادة لتأكيد ما، فيجب عليك استخدام التابع check يأمر.