برتراند ماير وآخرون. : مفهوم الصنف الثابت في برمجة OO
الملخص: تعتبر ثوابت الفئة (قيود التناسق التي يتم الحفاظ عليها بواسطة كل عملية على كائنات من نوع معين) أساسية لبناء البرامج الموجهة للكائنات وفهمها والتحقق منها. لكن بالنسبة للتحقق ، فإنها تثير صعوبات لم تتلق بعد حلاً مقبولاً بشكل عام. يقدم هذا العمل قاعدة إثبات تهدف إلى حل هذه المشكلات والسماح لأدوات التحقق بالاستفادة من الثوابت. يوضح مفهوم الثابت ويحدد المشكلات الثلاثة المرتبطة بها: عمليات الاسترجاعات والوصول الخفي والتسرب المرجعي. على سبيل المثال ، نتج خطأ Ethereum DAO لعام 2016 ، الذي سُرقت فيه 50 مليون دولار ، عن رد اتصال يبطل ثابتًا. تبدأ المناقشة بنموذج حسابي مبسط وقاعدة إثبات مرتبطة به ، مما يدل على صحتها. ثم يقوم بحذف الفرضيات المبسطة الثلاث واحدة تلو الأخرى ، حيث يثير كل حذف إحدى المشكلات الثلاث ، ويؤدي إلى تكييف مماثل لقاعدة الإثبات. يمكن للنسخة النهائية من القاعدة معالجة الأمثلة الصعبة ، بما في ذلك "مشكلات التحدي" المدرجة في الأدبيات.
الملخص: تعتبر ثوابت الفئة (قيود التناسق التي يتم الحفاظ عليها بواسطة كل عملية على كائنات من نوع معين) أساسية لبناء البرامج الموجهة للكائنات وفهمها والتحقق منها. لكن بالنسبة للتحقق ، فإنها تثير صعوبات لم تتلق بعد حلاً مقبولاً بشكل عام. يقدم هذا العمل قاعدة إثبات تهدف إلى حل هذه المشكلات والسماح لأدوات التحقق بالاستفادة من الثوابت. يوضح مفهوم الثابت ويحدد المشكلات الثلاثة المرتبطة بها: عمليات الاسترجاعات والوصول الخفي والتسرب المرجعي. على سبيل المثال ، نتج خطأ Ethereum DAO لعام 2016 ، الذي سُرقت فيه 50 مليون دولار ، عن رد اتصال يبطل ثابتًا. تبدأ المناقشة بنموذج حسابي مبسط وقاعدة إثبات مرتبطة به ، مما يدل على صحتها. ثم يقوم بحذف الفرضيات المبسطة الثلاث واحدة تلو الأخرى ، حيث يثير كل حذف إحدى المشكلات الثلاث ، ويؤدي إلى تكييف مماثل لقاعدة الإثبات. يمكن للنسخة النهائية من القاعدة معالجة الأمثلة الصعبة ، بما في ذلك "مشكلات التحدي" المدرجة في الأدبيات.
What's Your Reaction?
