مقدمة في التحقق من البرمجيات باستخدام لغة Dafny - تأليف Boro Sitnikovski (غلاف ورقي)

ملخص الكتاب تعرّف على أساسيات التحقق من البرمجيات وإثبات صحتها باستخدام لغة البرمجة Dafny المدعومة من Microsoft Research. وبينما تتسم بعض الكتب الأخرى حول هذا الموضوع بالصرامة الرياضية الشديدة، سيعتمد هذا الكتاب على أقل قدر ممكن من الرموز والصرامة الرياضية، وسيشرح كل مفهوم بلغة بسيطة وواضحة. يُعد هذا الكتاب المرجع المثالي لمبرمجي البرمجيات والمطورين الذين يمتلكون مهارات في لغة C# ولغات البرمجة الأخرى. نظرًا لأن كتابة برمجيات صحيحة قد تكون أمرًا صعبًا، ستتعلم من خلال هذا الكتاب مفهوم الحوسبة والتحقق من البرمجيات. بعد ذلك، قم بتطبيق هذه المفاهيم والتقنيات لكتابة كود برمجي خالٍ من الأخطاء وبثقة تامة، بحيث يكون من السهل فهمه. ستكون الشفرة المصدرية متاحة طوال الكتاب، كما يمكن الوصول إليها مجانًا عبر GitHub. بعد قراءة هذا الكتاب واستخدامه، ستتمكن من كتابة شفرة مصدرية صحيحة وخالية من الأخطاء البرمجية، وهي قابلة للتطبيق بغض النظر عن المنصة ولغة البرمجة التي تستخدمها. ما ستتعلمه: اكتشف لغة البرمجة Dafny المدعومة من Microsoft Research.

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

لمن هذا الكتاب لمطوري البرمجيات والمبرمجين الذين لديهم خبرة برمجية أساسية سابقة. لا تتطلب معرفة لغة برمجة محددة. كما أنه مناسب لمن لديهم خبرة رياضية بسيطة جداً (الدوال والمتغيرات).

من الغلاف الخلفي تعرّف على التحقق من البرمجيات وإثبات صحتها باستخدام لغة البرمجة Dafny المدعومة من Microsoft Research. وبينما تتسم بعض الكتب الأخرى حول هذا الموضوع بالصرامة الرياضية الشديدة، سيعتمد هذا الكتاب على أقل قدر ممكن من الرموز والصرامة الرياضية، وسيشرح كل مفهوم بلغة بسيطة وسهلة. يُعد هذا الكتاب المرجع المثالي لمبرمجي ومطوري البرمجيات الذين يمتلكون مهارات في لغة C# ولغات البرمجة الأخرى. نظرًا لصعوبة كتابة برمجيات خالية من الأخطاء، ستتعلم من خلال هذا الكتاب مفاهيم الحوسبة والتحقق من البرمجيات، ومن ثم ستتمكن من تطبيق هذه المفاهيم والتقنيات لكتابة كود برمجي خالٍ من الأخطاء وسهل الفهم بكل ثقة. ستكون الأكواد المصدرية متاحة طوال الكتاب، كما يمكن الوصول إليها مجانًا عبر GitHub. وبعد قراءة هذا الكتاب واستخدامه، ستصبح قادرًا على كتابة أكواد مصدرية صحيحة للبرمجيات الحرة والضخمة، بحيث تكون قابلة للتطبيق بغض النظر عن المنصة أو لغة البرمجة التي تستخدمها. ستكتشف لغة البرمجة Dafny المدعومة من Microsoft Research

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

نبذة عن المؤلف يتمتع Boro Sitnikovski بخبرة تزيد عن عشر سنوات من العمل الاحترافي كمهندس برمجيات. بدأ البرمجة باستخدام لغة assembly على معالج Intel x86 في سن العاشرة. وخلال مرحلة المدرسة الثانوية، فاز بعدة جوائز في البرمجة التنافسية، تراوحت بين المركز 4 و3 و1. وهو خريج معلوماتية - وكانت أطروحة البكالوريوس الخاصة به بعنوان "Programming in Haskell using algebraic data structures"، بينما كانت أطروحة الماجستير بعنوان "Formal verification of Instruction Sets in Virtual Machines". كما قام بنشر بعض الأوراق البحثية حول التحقق من البرمجيات. تشمل اهتماماته البحثية الأخرى لغات البرمجة، والرياضيات، والمنطق، والخوارزميات، وكتابة برمجيات صحيحة. وهو مؤمن بشدة بفلسفة المصادر المفتوحة ويساهم في مشاريع متنوعة مفتوحة المصدر. وفي أوقات فراغه، يستمتع بقضاء بعض الوقت مع عائلته.