A Formal Executable Semantics of Orc using the K Framework
No Thumbnail Available
Date
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Saudi Digital Library
Abstract
أٝرخ لغة تعبير رياضية تمكّن من وصف عمليات حوسبة متوازية (كما في الحوسبة متعددة المهام)، و هي اختصار كلمة أرخصطرة (أٝوركۧسترا)، سُمّيت بذلك تنويها عن عمل قائد الأرخصطرة في تنظيم و توزيع المهام على عازفيه و التنسيق بينهم. تخفي لغة التعبير هذه تفاصيل عمليات الحوسبة المعروفة في لغات البرمجة خلف ستار أنيق لا يحتوي إلا على أدوات بسيطة هي القدرة على نداء الدوالّ و الجمع بينها بأربع منسقات أرخصطرية بسيطة و جامعة. هدفنا من هذا البحث تمكين التأكّد الآليّ من صحة البرامج المكتوبة بلغة أٝرخ، فوجب لذلك كتابة وصف رياضيّ (دلاليّ) كامل للغة أٝرخ، و لعمل ذلك اخترنا محيط عمل يسمى K يمكّن من تعريف لغات ثم تشغيل برامج بتلك اللغات، و يمكّن كذلك من تأكّدٍ من صحتها. يعرض هذا البحث بدقّة كيف استخدمنا مُختلف مميزات K لنصل إلى وصف رياضيّ بسيط و أنيق للغة أٝرخ، و كيف يُقارَن وصفُنا بما سبقه، و كيف يمكّننا هذا من تشغيل برامج بلغة أٝرخ و التأكدِ من صحّتها من خلال عدّة أمثلة مشروحة.