♾ نمونه‌ای از اثبات ریاضی (منطق هوار)

🧐 فرض کنید برنامه‌ای داریم که دو عدد x و y را با هم جمع می‌کند و نتیجه را در z ذخیره می‌کند.


💬 ما می‌خواهیم صحت این برنامه را اثبات کنیم:


1⃣ برنامه:

z := x + y

2⃣ سه‌تایی هوار:

{True} z := x + y {z = x + y}

پیش‌شرط: برای شروع کار، هیچ فرضیه خاصی در پیش‌شرط نداریم، بنابراین می‌گوییم True...

دستور: دستور ما z := x + y است که مقدار x + y را به متغیر z تخصیص می‌دهد...

پس‌شرط: پس از اجرای دستور، پس‌شرط ما این است که z باید برابر با x + y باشد...


3⃣ اثبات:

💬 برای اثبات اینکه این سه‌تایی هوار صحیح است، از قانون تخصیص در منطق هوار استفاده می‌کنیم.

✨ این قانون بیان می‌کند که اگر بتوانیم نشان دهیم که پس از اجرای دستور، پس‌شرط برقرار است، می‌توانیم نتیجه بگیریم که برنامه به درستی عمل می‌کند ✨

☝️🏼 مرحله اول: {استفاده از قانون تخصیص}:

📐 طبق قانون تخصیص، ما می‌نویسیم:

{P[x := E]} x := E {P}

💬 که به معنای این است که اگر پیش‌شرط با مقدار جدید x جایگزین شود، پس‌شرط نیز باید درست باشد...

در اینجا:
● P = z = x + y
● E = x + y

📏 بنابراین، با توجه به قانون تخصیص، می‌توانیم بنویسیم:

{z = x + y} z := x + y {z = x + y}

✌️🏼 مرحله دوم: {اثبات}

🎗 پیش‌شرط: True، به این معنا که هیچ فرضی قبل از اجرای دستور لازم نیست.

🎯 اجرا: در حال اجرای دستور z := x + y، مقدار جدیدی به z تخصیص می‌دهیم.

🧩 پس‌شرط: اکنون می‌خواهیم ثابت کنیم که
z = x + y

✨ از آنجایی که ما مقدار z را با x + y برابر می‌گذاریم، بنابراین نتیجه می‌گیریم که پس از اجرای دستور، z برابر با مجموع x و y است...


🔥 نتیجه‌گیری:

💬 به این ترتیب، با استفاده از قانون تخصیص، می‌توانیم نتیجه بگیریم که:

👾 اگر پیش‌شرط True باشد و دستور z := x + y اجرا شود، پس‌شرط z = x + y نیز برقرار خواهد بود.

✅ در نهایت، ما می‌توانیم نتیجه بگیریم که برنامه به درستی عمل می‌کند و مقدار صحیح را به متغیر z تخصیص می‌دهد...


👑 جمع‌بندی:

👌🏼 ما از سه‌تایی هوار و قانون تخصیص برای اثبات این که برنامه به درستی عمل می‌کند استفاده کردیم...

💫 به همین دلیل، این نتیجه به وضوح نشان می‌دهد که چگونه با استفاده از روش‌های منطقی و اثباتی، می‌توانیم درستی برنامه‌های پیچیده‌تر را نیز اثبات کنیم...

🦾 این رویکرد، به ما این امکان را می‌دهد که در مرحله طراحی و پیاده‌سازی، اطمینان حاصل کنیم که برنامه‌ها به درستی و مطابق با انتظار ما عمل می‌کنند...



🔗 پیوندهای مرتبط:

🦦 سرعتی یا تنبلی؟

📌 روش ثبت مغازه یا لوکیشن محل کار در گوگل مپ

💣 بمباران ترفندهای آیفونی 💥🤪



#Article
#Computer_Science
#FormalVerification
#ProgrammingTheory
#Rare_knowledge
#Professional
#Good_2_Know
#SoftwareCorrectness
#MathematicalProof
#AlgorithmVerification
#ComputerProgramming
#SoftwareEngineering



🤩Want more?
🛜Check our ↙️channel...↙️
🦾💻@Computer3cks