التحقق رسميًا من صحة الخوارزمية

Question

بادئ ذي بدء ، هل هذا ممكن فقط على الخوارزميات التي ليس لها آثار جانبية؟

ثانياً ، أين يمكنني التعرف على هذه العملية ، أي كتب ومقالات جيدة وما إلى ذلك؟

Answer 1

coq هو مساعد دليل ينتج إخراج OCAML الصحيح. انها معقدة جدا رغم ذلك. لم أتجول أبدًا للنظر إليه ، لكن زميلي في العمل بدأ ثم توقف عن استخدامه بعد شهرين. كان ذلك في الغالب لأنه أراد إنجاز الأمور بشكل أسرع ، ولكن إذا كنت بحاجة إلى التحقق من خوارزمية ، فقد تكون هذه فكرة جيدة.

هنا دورة الذي يستخدم COQ ويتحدث عن إثبات الخوارزميات.
و هنا برنامج تعليمي حول كتابة الأوراق الأكاديمية في COQ.

Answer 2

1. عموما الكثير أسهل للتحقق/إثبات الصواب عندما لا يتم إشراك أي آثار جانبية ، لكنها ليست شرطًا مطلقًا.
2. قد ترغب في إلقاء نظرة على بعض الوثائق للحصول على لغة مواصفات رسمية مثل ض. المواصفات الرسمية ليست دليلًا على حد ذاتها ، ولكنها غالبًا ما تكون الأساس لواحد.

Answer 3

عادة ما تكون أدلة الصواب محددة للغاية للخوارزمية في متناول اليد.

ومع ذلك ، هناك العديد من الحيل المعروفة التي يتم استخدامها وإعادة استخدامها مرة أخرى. على سبيل المثال ، مع الخوارزميات العودية يمكنك استخدامها أحواض الحلقة.

هناك خدعة شائعة أخرى تتمثل في تقليل المشكلة الأصلية إلى مشكلة يكون إثبات الخوارزمية على الصواب أسهل من أجلها ، ثم تعميم المشكلة أسهل أو إظهار أن المشكلة الأسهل يمكن ترجمتها إلى حل للمشكلة الأصلية. هنا هو وصف.

إذا كان لديك خوارزمية معينة في الاعتبار ، فيمكنك أن تفعل أفضل في السؤال عن كيفية إنشاء دليل على هذه الخوارزمية بدلاً من إجابة عامة.

Answer 4

شراء هذه الكتب: http://www.amazon.com/science-programming-monographs-computer/dp/0387964800

كتاب غريس ، البرمجة العلمية هي أشياء رائعة. المريض ، شامل ، كاملة.

Answer 5

أعتقد أن التحقق من صحة الخوارزمية من شأنه أن يتحقق من صحة مطابقةها مع المواصفات. هناك فرع من علوم الكمبيوتر النظرية تسمى الطرق الرسمية قد يكون ما تبحث عنه إذا كنت بحاجة إلى الاقتراب من الإثبات قدر الإمكان. من ويكيبيديا ،

الطرق الرسمية هي نوع معين من التقنيات القائمة على الرياضيات لمواصفات وتطوير والتحقق من أنظمة البرمجيات والأجهزة

ستتمكن من العثور على العديد من موارد وأدوات التعلم من العديد من الروابط على صفحة Wikipedia المرتبطة ومن الطرق الرسمية ويكي.

Answer 6

يقدم منطق علوم الكمبيوتر ، من قبل Huth و Ryan ، نظرة عامة قابلة للقراءة بشكل معقول للأنظمة الحديثة للأنظمة. بمجرد أن تحدث الناس عن إثبات البرامج الصحيحة - مع لغات البرمجة التي قد يكون لها أو لا يكون لها آثار جانبية. الانطباع الذي أحصل عليه من هذا الكتاب وأماكن أخرى هو أن التطبيقات الحقيقية مختلفة - على سبيل المثال ، يثبت أن البروتوكول صحيح ، أو أن وحدة نقطة العائمة للرقاقة يمكن أن تقسم بشكل صحيح ، أو أن روتينًا خاليًا من القفل لمعالجة القوائم المرتبطة صحيح.

ACM Computing Surveys Vol 41 Issue 4 (أكتوبر 2009) هي مشكلة خاصة في التحقق من البرامج. يبدو أنه يمكنك الوصول إلى واحدة على الأقل من الأوراق بدون حساب ACM من خلال البحث عن "الطرق الرسمية: الممارسة والتجربة".

Answer 7

الأداة Frama-C, ، الذي يقترح Elazar مقطع فيديو تجريبي في التعليقات ، يمنحك لغة مواصفات ، ACSL, ، بالنسبة لكتابة عقود الوظائف والمحللات المختلفة للتحقق من أن وظيفة C تستوفي عقودها وسلامتها مثل عدم وجود أخطاء في وقت التشغيل.

برنامج تعليمي ممتد ، ACSL بالقدوة, ، تعرض أمثلة على خوارزميات C الفعلية التي يتم تحديدها والتحقق منها ، ويفصل الوظائف الخالية من التأثير الجانبي عن الوظائف الفعالة (تعتبر تلك الخالية من التأثير الجانبي أسهل وتأتي أولاً في البرنامج التعليمي). هذا المستند مثير للاهتمام أيضًا لأنه لم يكتبه مصممو الأدوات التي تصفها ، لذلك فهي تعطي نظرة أكثر تعليمية على هذه التقنيات.

Answer 8

إذا كنت على دراية بـ LISP ، فعليك بالتأكيد التحقق من ACL2: http://www.cs.utexas.edu/~moore/acl2/acl2-doc.html

Answer 9

ديجكسترا انضباط البرمجة ويضع EWDs أساس التحقق الرسمي كعلم في البرمجة. عمل أبسط هو Wirth's البرمجة المنهجية, ، والذي يبدأ بالنهج البسيط لاستخدام التحقق. يستخدم Wirth قبل Iso Pascal للغة ؛ يستخدم Dijkstra شكلاً يشبه Algol-68 يسمى Guarded (GCL). نضج التحقق الرسمي منذ Dijkstra و Hoare ، ولكن هذه النصوص القديمة قد لا تزال نقطة انطلاق جيدة.

Answer 10

أداة PVS التي طورتها Stanford Guys هي نظام المواصفات والتحقق. لقد عملت عليه ووجدته مفيدًا جدًا لـ Theoram Proving.

Answer 11

WRT (1) ، من المحتمل أن تضطر إلى إنشاء نموذج للخوارزمية بطريقة "تلتقط" الآثار الجانبية للخوارزمية في متغير البرنامج يهدف إلى تصميم مثل هذه الآثار الجانبية القائمة على الحالة.