ALZUHAIBI OMAR ZUHAIR2022-05-182022-05-183088https://drepo.sdl.edu.sa/handle/20.500.14154/2721أٝرخ لغة تعبير رياضية تمكّن من وصف عمليات حوسبة متوازية (كما في الحوسبة متعددة المهام)، و هي اختصار كلمة أرخصطرة (أٝوركۧسترا)، سُمّيت بذلك تنويها عن عمل قائد الأرخصطرة في تنظيم و توزيع المهام على عازفيه و التنسيق بينهم. تخفي لغة التعبير هذه تفاصيل عمليات الحوسبة المعروفة في لغات البرمجة خلف ستار أنيق لا يحتوي إلا على أدوات بسيطة هي القدرة على نداء الدوالّ و الجمع بينها بأربع منسقات أرخصطرية بسيطة و جامعة. هدفنا من هذا البحث تمكين التأكّد الآليّ من صحة البرامج المكتوبة بلغة أٝرخ، فوجب لذلك كتابة وصف رياضيّ (دلاليّ) كامل للغة أٝرخ، و لعمل ذلك اخترنا محيط عمل يسمى K يمكّن من تعريف لغات ثم تشغيل برامج بتلك اللغات، و يمكّن كذلك من تأكّدٍ من صحتها. يعرض هذا البحث بدقّة كيف استخدمنا مُختلف مميزات K لنصل إلى وصف رياضيّ بسيط و أنيق للغة أٝرخ، و كيف يُقارَن وصفُنا بما سبقه، و كيف يمكّننا هذا من تشغيل برامج بلغة أٝرخ و التأكدِ من صحّتها من خلال عدّة أمثلة مشروحة.enA Formal Executable Semantics of Orc using the K FrameworkThesis