ارسل ملاحظاتك

ارسل ملاحظاتك لنا







منطق هور ودوره في برامج الحاسوب

العنوان بلغة أخرى: Hoare Logic and its Role in Computer Programs
المصدر: مجلة بحوث
الناشر: جامعة عين شمس - كلية البنات للآداب والعلوم والتربية
المؤلف الرئيسي: محمد، هبه ممدوح مختار (مؤلف)
المؤلف الرئيسي (الإنجليزية): Mohamed, Heba Mamdoh Mukhtar
مؤلفين آخرين: النويهي، سهام محمود (م. مشارك) , السيد، مايسة عبده علي (م. مشارك)
المجلد/العدد: مج4, ع5
محكمة: نعم
الدولة: مصر
التاريخ الميلادي: 2024
الشهر: مايو
الصفحات: 163 - 197
ISSN: 2735-4814
رقم MD: 1503164
نوع المحتوى: بحوث ومقالات
اللغة: العربية
قواعد المعلومات: EduSearch, HumanIndex
مواضيع:
كلمات المؤلف المفتاحية:
منطق هور | ثلاثية هور | التحقق الصوري | التقريرات | المواصفات | التحقق من البرنامج | Hoare Logic | Hoare Triple | Formal Verification | Assertions | Specification | Program Verification
رابط المحتوى:
صورة الغلاف QR قانون

عدد مرات التحميل

1

حفظ في:
المستخلص: يُعد تصميم وتطوير أنظمة عالية الجودة تلبي متطلباتها أمرًا في غاية الأهمية؛ خاصة مع التعقيد المتزايد باستمرار لأنظمة الحاسوب، فمن الممكن أن يتسبَّب فشل النظام في مهمته أو سلامته إلى مشكلات عديدة؛ مثل: تجاوز التكلفة، وفقدان في الأرواح أو خسائر اقتصادية وخيمة؛ لذلك وجَّه العديد من العلماء اهتمامهم للكشف عن أخطاء تلك البرامج ومعالجتها، استنادًا إلى أسس منطقية سليمة، ويُعتبر منطق هور أول منطق قدَّم نسقًا صوريًّا لتطبيقه في مجال التحقُّق الصوري من صحة البرنامج؛ لذا يهدف هذا البحث إلى توضيح وبيان دور منطق هور في ذلك؛ من خلال الوقوف على أسباب ظهوره، ومراحل تطوره، ومفهومه، وعرض وتحليل مكونات نسقه الصوري، وبيان كيفية تطبيقه، وقد اتبعت الباحثة في ذلك المنهج التاريخي، والمنهج التحليلي النقدي المقارَن. ليتبيَّن لنا أن المنطق لا ينفصل عن الواقع، بل يسايره في ظل التقدم العلمي والتكنولوجي. بالإضافة إلى أن دارسي علوم الحاسوب لا يمكنهم الاستغناء عن دراسة المنطق؛ فهو يوفِّر لهم الأساس لفهم كيفية عمل أجهزة الحاسوب، وكيفية التعامل معها، فإذا أراد المبرمج أن يتجنَّب الأخطاء في الكود البرمجي، ينبغي أن يتحقَّق من صحة برنامجه، باستخدام أسس وقواعد منطق هور؛ لذا حاز منطق هور على اهتمام علماء المنطق، وعلماء الحاسوب، فظهرت العديد من الإسهامات التي سعت لتطويره في ظل التقدم العلمي المستمر؛ من أجل التحقُّق وإثبات صحة البرامج بكافة أنواعها، بل وتطويرها أيضًا؛ لذلك تُوصي الباحثة بتوجيه المزيد من الاهتمام في عالمنا العربي بالأبحاث العلمية، حول الأنواع الجديدة للمنطق وتطبيقاتها في مجالات علوم الحاسوب.

Designing and developing high-quality systems that meet their requirements is extremely important. Especially with the ever-increasing complexity of computer systems, failure of the system in its mission or safety can cause many problems such as: cost overruns, loss of life or severe economic losses; Therefore, many scientists have directed their attention to detecting errors in these programs and treating them, based on sound logical foundations. Hoare’s logic is considered the first logic that presented a formal format for application in the field of formal verification of the verification of the program. Therefore, this research aims to clarify and explain the role of Hoare’s logic in verifying the program. By identifying the reasons for its appearance, the stages of its development, its concept, presenting and analyzing the components of its formal format, and explaining how to apply it in verifying the validity of the program. The researcher followed the historical approach and the comparative critical analytical approach. It becomes clear to us that logic is not separated from reality, but rather keeps pace with it considering scientific and technological progress. In addition, computer science students cannot do without studying logic; It provides them with the basis for understanding how computers work, and how to deal with them. If the programmer wants to avoid errors in the code and verify the validity of his program, he must apply the foundations and rules of Hoare's logic. Therefore, Hoare's logic gained the attention of logicians and computer scientists, and many contributions appeared that sought to develop it considering the continuous scientific progress. To verify and prove the validity of programs of all kinds, and even develop them; Therefore, the researcher recommends directing more attention in the Arab world to scientific research on new types of logic and their applications in the fields of computer science.

ISSN: 2735-4814

عناصر مشابهة