২৩ সেপ, ২০২৫·8 মিনিট
টনি হোয়ার-এর শুদ্ধতা ধারণা: লজিক থেকে নিরাপদ কোড
টনি হোয়ার-এর Hoare লজিক, কুইকসোর্ট ও সেফটি মাইন্ডসেট কীভাবে ব্যবহারিক কৌশলে রূপ নেয়—কোড রিভিউ, ইনভারিয়েন্ট ও স্পেসিফিকেশন থেকে নিরাপদ সফটওয়্যার পর্যন্ত শেখা।
টনি হোয়ার-এর Hoare লজিক, কুইকসোর্ট ও সেফটি মাইন্ডসেট কীভাবে ব্যবহারিক কৌশলে রূপ নেয়—কোড রিভিউ, ইনভারিয়েন্ট ও স্পেসিফিকেশন থেকে নিরাপদ সফটওয়্যার পর্যন্ত শেখা।
যখন মানুষ বলে কোনো প্রোগ্রাম “শুদ্ধ” তাতে তারা প্রায়শই বোঝায়: “আমি এটা কয়েকবার চালিয়েছি এবং আউটপুট ঠিক দেখাচ্ছে।” এটা একটা উপযোগী সংকেত—কিন্তু এটা শুদ্ধতা নয়। সরলভাবে, শুদ্ধতা মানে প্রোগ্রাম তার স্পেসিফিকেশন মেনে চলে: প্রত্যেক অনুমোদিত ইনপুটের জন্য এটি প্রয়োজনীয় ফলাফল তৈরি করে এবং স্টেট পরিবর্তন, সময়সীমা এবং ত্রুটির সম্পর্কে যেসব নিয়ম আছে সেগুলো রক্ষা করে।
কিন্তু ধাঁধাটি হল “স্পেসিফিকেশন মেনে চলে” শোনায় সহজ—কিন্তু করা কঠিন।
প্রথমত, স্পেসিফিকেশনগুলো প্রায়ই অস্পষ্ট হয়। একটি প্রোডাক্ট রিকোয়ারমেন্ট বলতে পারে “তালিকাটি সাজাও”, কিন্তু এটা কি স্থিতিশীল সাজানো (stable sorting) মানে? ডুপ্লিকেট মান, খালি তালিকা, বা অ-সংখ্যাতত্ত্ব উপাদানগুলো কীভাবে হবে? স্পেসিফিকেশনে যদি না বলা থাকে, আলাদা মানুষ আলাদা অনুমান করবে।
দ্বিতীয়ত, এজ কেসগুলো বিরল নয়—তবে তারা কম ঘন ঘন পরীক্ষা করা হয়। Null মান, ওভারফ্লো, অফ-বাই-ওয়ান সীমা, অস্বাভাবিক ব্যবহারকারী ক্রম এবং অননুজ্ঞেয় বাহ্যিক ব্যর্থতা “এটা কাজ করে” থেকে “প্রোডাকশনে ব্যর্থ” এ পরিণত করতে পারে।
তৃতীয়ত, চাহিদা পরিবর্তন হয়। একটি প্রোগ্রাম গতকালের স্পেসিফিকেশনের প্রশ্নে শুদ্ধ হতে পারে এবং আজকের স্পেসিফিকেশনের তুলনায় ভুল হতে পারে।
টনি হোয়ার-এর বড় অবদান ছিল সবকিছুই সবসময় প্রমাণ করা উচিত—এই দাবি নয়। বরং তিনি বলেছিলেন যে আমরা কোড কোন কাজ করবে তা আরও সুনির্দিষ্ট ভাবে ব্যাখ্যা করতে পারি—এবং তা শৃঙ্খলাবদ্ধভাবে বিশ্লেষণ করতে পারি।
এই পোস্টে আমরা তিনটি সংযুক্ত থ্রেড অনুসরণ করব:
অধিকাংশ দল সম্পূর্ণ ফর্মাল প্রমাণ লিখবে না। কিন্তু আংশিক, “প্রমাণ-স্টাইল” চিন্তা তবুও বাগ ধরতে সহজ করে, রিভিউ আরও ধারালো করে, এবং কোড শিপ করার আগে আচরণ স্পষ্ট করে।
টনি হোয়ার এমন বিরল কম্পিউটার বিজ্ঞানীদের একজন যাদের গবেষণা কেবল পেপার বা ক্লাসরুমে আটকে থাকে না। তিনি একাডেমিয়া ও ইন্ডাস্ট্রির মধ্যে চলাফেরা করেছেন, এবং তিনি প্রত্যেক দলের সম্মুখীন হওয়া ব্যবহারিক প্রশ্ন নিয়ে চিন্তা করেছেন: বিশেষ করে উচ্চ স্টেকস থাকলে কিভাবে আমরা নিশ্চিত হবো যে প্রোগ্রামটি আমরা যা ভাবি তা করে?
এই লেখাটি কিছু হোয়ার ধারণার উপর কেন্দ্রিত যা বাস্তব কোডবেজে প্রায়ই দেখা যায়:
{P} C {Q} ব্যবহার করে প্রোগ্রাম আচরণ বর্ণনা করার উপায়।এখানে আপনি গভীর গাণিতিক ফর্মালিজম পাবেন না, এবং আমরা কুইকসোর্টের সম্পূর্ণ, মেশিন-চেকযোগ্য প্রমাণ দেওয়ার চেষ্টা করব না। লক্ষ্য হলো ধারণাগুলো অ্যাক্সেসযোগ্য রাখা: আপনার যুক্তি পরিষ্কার করতে যথেষ্ট কাঠামো, কিন্তু কোড রিভিউকে গ্র্যাজুয়েট সেমিনারে পরিণত না করেই।
হোয়ার-এর ধারণাগুলো দৈনন্দিন সিদ্ধান্তে অনুবাদিত হয়: একটি ফাংশন কোন অনুমানগুলোর উপর নির্ভর করে, কলারকে কী গ্যারান্টি দেয়, লুপের মাঝখানে কী বজায় থাকতে হবে, এবং রিভিউতে “প্রায়ঠিক” পরিবর্তনগুলো কীভাবে শনাক্ত করবেন। এমনকি আপনি যদি স্পষ্টভাবে {P} C {Q} না লেখেন, সেই আকৃতির চিন্তা API, টেস্ট এবং জটিল কোড নিয়ে কথোপকথন উন্নত করে।
হোয়ার-এর দৃষ্টিভঙ্গি হলো “কয়েকটি উদাহরণে ঠিক ছিল” এর চেয়েও কঠোর: শুদ্ধতা হল সম্মত প্রতিশ্রুতি পূরণ—না যে ছোট নমুনায় ঠিক দেখাচ্ছে।
বাগ প্রায়ই ঘটে যখন দল মাঝের ধাপটি এড়িয়ে সরাসরি requirements থেকে কোডে লাফায়, ফলে “প্রতিশ্রুতি” অস্পষ্ট থাকে।
দুইটি দাবি প্রায়ই একসাথে মিশে যায়:
বাস্তব সিস্টেমে, “কখনও শেষ না হওয়া” ঠিক না হওয়ার মতোই ক্ষতিকর হতে পারে।
শুদ্ধতার বিবৃতিগুলো সার্বজনীন নয়; সেগুলো নির্ভর করে অনুমানগুলোর উপর, যেমন:
অনুমানগুলো স্পষ্ট করা “আমার মেশিনে কাজ করে” কে অন্যদের বোঝার যোগ্য অঙ্গীকারে পরিণত করে।
ধরা যাক একটি ফাংশন sortedCopy(xs) আছে।
একটি দরকারী স্পেসিফিকেশন হতে পারে: “নতুন তালিকা ys রিটার্ন করবে, যেখানে (1) ys ঊর্ধ্বক্রমে সাজানো, এবং (2) ys-এ xs-এর উপাদানসমূহ ঠিক সমান গণনায় আছে, এবং (3) xs অপরিবর্তিত আছে।”
এখন “সঠিক” মানে হলো কোডটি উক্ত তিনটি পয়েন্ট উল্লিখিত অনুমানগুলোর অধীনে পূরণ করছে—শুধু যে আউটপুটটি দ্রুত পরীক্ষা করে সাজানো মনে হচ্ছে তা নয়।
হোয়ার লজিক কোড নিয়ে এমনভাবে আলোচনা করার উপায় দেয় যেটা আপনি চুক্তি বলেই ভাববেন: যদি আপনি এমন একটি স্টেটে শুরু করেন যা নির্দিষ্ট শর্তগুলো পূরণ করে, এবং আপনি এই কোডটি চালান, আপনি এমন একটি স্টেটে শেষ করবেন যা নির্দিষ্ট গ্যারান্টি পূরণ করে।
কোর নোটেশন হলো হোয়ার ট্রিপল:
{precondition} program {postcondition}
প্রিকন্ডিশন জানায় কোড অংশ চালানোর আগে কী সত্য হতে হবে। এটি আপনি আশা করছেন এমন কিছু নয়; এটি কোডটির চলার জন্য যা প্রয়োজন।
উদাহরণ: ধরা যাক একটি ফাংশন দুটি সংখ্যার গড় রিটার্ন করে বিনা ওভারফ্লো চেকের।
a + b ইন্টিজার টাইপে ফিট করেavg = (a + b) / 2avg হল a ও b-র গাণিতিক গড়যদি প্রিকন্ডিশন বজায় না থাকে (ওভারফ্লো সম্ভব), পোস্টকন্ডিশন আর প্রযোজ্য নাও হতে পারে। ট্রিপলটি আপনাকে তা জাহির করতে বাধ্য করে।
পোস্টকন্ডিশন জানায় কোডটি চালানোর পরে কী সত্য হবে—ধরা যাক প্রিকন্ডিশন মেনে চলেছে। ভালো পোস্টকন্ডিশনগুলো স্পষ্ট ও চেকযোগ্য হওয়া উচিত। “রেজাল্ট ভ্যালিড” বলার বদলে বলুন “ভ্যালিড” মানে কী: সাজানো, অ-নেগেটিভ, নির্দিষ্ট সীমার মধ্যে, নির্দিষ্ট ফিল্ড ছাড়া অপরিবর্তিত ইত্যাদি।
হোয়ার লজিক ক্ষুদ্র বিবৃতিগুলো থেকে বহু ধাপের কোড পর্যন্ত স্কেল করে:
x = x + 1-এর পরে x সম্পর্কে কোন কোন সত্যতা প্রযোজ্য?মুখ্য উদ্দেশ্য হলো প্রত্যাশা পাঠযোগ্য করা: স্পষ্ট অনুমান, স্পষ্ট ফলাফল, এবং রিভিউতে “এটা কাজ করে” কথোপকথনগুলো কমানো।
লুপ ইনভারিয়েন্ট এমন একটি বক্তব্য যা লুপ শুরুর আগে সত্য, প্রতিটি ইটারেশনের পরে সত্য থাকে, এবং লুপ শেষের সময়ে সত্য থাকে। এটি একটি সাধারণ ধারণা কিন্তু বড় সুবিধা দেয়: এটি “কাজ করছে” কথাকে এমন এক দাবিতে পরিণত করে যা আপনি প্রতিটি ধাপেই চেক করতে পারেন।
ইনভারিয়েন্ট না থাকলে রিভিউতে প্রায়শই শোনা যায়: “আমরা তালিকাটি ইটারেট করি এবং ধীরে ধীরে জিনিস ঠিক করি।” একটি ইনভারিয়েন্ট নির্দিষ্ট করে দেয়: এই মুহূর্তে ঠিক কীই ঠিক করা হয়েছে, যদিও লুপ শেষ হয়নি। একবার আপনি সেটা স্পষ্টভাবে বলতে পারেন, অফ-বাই-ওয়ান ত্রুটি ও মিসিং কেসগুলো শনাক্ত করা সহজ হয়, কারণ সেগুলো এমন মুহূর্ত হিসেবে দেখা যায় যেখানে ইনভারিয়েন্ট ভাঙবে।
দৈনন্দিন কোডের অধিকাংশই কিছু নির্ভরযোগ্য টেমপ্লেট ব্যবহার করতে পারে।
1) বাউন্ডস / ইনডেক্স সেফটি
ইনডেক্সগুলো নিরাপদ রেঞ্জে রাখুন।
0 <= i <= nlow <= left <= right <= highএই ধরনের ইনভারিয়েন্ট আউট-অফ-রেঞ্জ অ্যাক্সেস প্রতিরোধে এবং অ্যারে যুক্তি কনক্রিট করতে উপকারী।
2) প্রসেস করা বনাম অপ্রসেস করা আইটেম
ডেটাকে “করা হয়ে গেছে” অঞ্চলে এবং “এখনও করা হয়নি” অঞ্চলে ভাগ করুন।
a[0..i)-এর সমস্ত উপাদান পরীক্ষা করা হয়েছে।”result-এ স্থানান্তরিত প্রতিটি আইটেম ফিল্টার প্রেডিকেট সন্তুষ্ট করে।”এটি অনিশ্চিত অগ্রগতি কে স্পষ্ট শব্দে “প্রক্রিয়াজাত” কী বোঝায় তা বলে দেয়।
3) সাজানো প্রিফিক্স (বা পার্টিশন করা প্রিফিক্স)
সাজানো, মার্জিং এবং পার্টিশনিং-এ সাধারণ।
a[0..i) সাজানো।”a[0..i)-এর সব উপাদান <= pivot, এবং a[j..n)-এর সব উপাদান >= pivot।”পূর্ণ অ্যারে এখনো সাজানো না হলেও, আপনি ঠিক জানেন কোন অংশটি পিন করা আছে।
শুদ্ধতা কেবল সঠিক হওয়া নয়; লুপটিকে সম্পন্নও হতে হবে। একটি সহজ উপায় হলো একটি মাপ (প্রায়ই variant বলা হয়) নামকরণ করা যা প্রতিটি ইটারেশনে হ্রাস পায় এবং চিরতরে হ্রাস পেতে পারে না।
উদাহরণ:
n - i প্রতি পদে 1 করে কমে।”যদি আপনি হ্রাসমান একটি মাপ না পান, আপনি হয়ত একটি বাস্তব ঝুঁকি আবিষ্কার করেছেন: কিছু ইনপুটে অসীম লুপ।
কুইকসোর্টের সহজ প্রতিশ্রুতি হলো: একটি স্লাইস (অথবা অ্যারে সেগমেন্ট) দেওয়া হলে তার উপাদানগুলো এমনভাবে পুনর্বিন্যস্ত করা যে তারা অর্ধ-অবনমিত (non-decreasing) ক্রমে আসে, এবং কোনো মান হারায় না বা নতুন মান গঠন করা হয় না। অ্যালগরিদমের উচ্চ-স্তরের রূপটি সহজ:
এটি একটি চমৎকার শিক্ষণ উদাহরণ কারণ এটি মাথায় ধারণ করার জন্য ছোট কিন্তু অপ্রচুরতা দেখায় যেখানে অনানুষ্ঠানিক যুক্তি ব্যর্থ হয়। কয়েকটি র্যান্ডম টেস্টে কাজ করে দেখানো কুইকসোর্টের তবুও কিছু ইনপুট বা বাউন্ডারি কন্ডিশনে ভুল থাকতে পারে।
কিছু সমস্যা সাধারণত বেশিরভাগ বাগের কারণ:
হোয়ার-স্টাইল যুক্তিতে, প্রমাণ সাধারণত দুটি অংশে ভাগ করা হয়:
এই বিভাজন যুক্তি পরিচালনাযোগ্য রাখে: পার্টিশন ঠিক করে নিন, তারপর এর উপরে সটিং শুদ্ধতা গঠন করুন।
কুইকসোর্টের গতি একটি ধূর্ত ছোট রুটিনের ওপর নির্ভর করে: পার্টিশন। যদি পার্টিশন সামান্য ভুল হয়, কুইকসোর্ট ভুল সাজাতে পারে, চিরান্তন রিকার্শনে পড়ে যেতে পারে, বা এজ কেসে ক্র্যাশ দিতে পারে।
আমরা ক্লাসিক হোয়ার পার্টিশন স্কিম ব্যবহার করব (দুটি পয়েন্টার ভিতরে দিকে চলে)।
ইনপুট: একটি অ্যারে স্লাইস A[lo..hi] এবং একটি pivot মান (প্রায়শই A[lo])।
আউটপুট: একটি ইনডেক্স p যাতে:
A[lo..p]-এর প্রতিটি উপাদান হলো <= pivotA[p+1..hi]-এর প্রতিটি উপাদান হলো >= pivotমনোযোগ দিন কী প্রতিশ্রুত নয়: pivot অবশ্যই p অবস্থানে শেষ হবে এমন বাধ্যবাধকতা নেই, এবং pivot-এর সমান উপাদানগুলো দুই পাশেই থাকতে পারে। সেটা ঠিক আছে—কুইকসোর্টকে কেবল একটি সঠিক বিভাজনই লাগে।
অ্যালগরিদম i বাম দিক থেকে এবং j ডান দিক থেকে এগোচ্ছে—ভাল যুক্তি তখনই কাজ করে যখন আপনি জানেন কী “লক ইন” হয়ে গেছে। বাস্তবসম্মত ইনভারিয়েন্টগুলো হতে পারে:
A[lo..i-1]-এর সব আইটেম <= pivot (বাম সাইড ক্লিন)A[j+1..hi]-এর সব আইটেম >= pivot (ডান সাইড ক্লিন)A[i..j]-এর সব কিছু অনশ্রেণীকৃত (এখনো চেক করা হচ্ছে)যখন আমরা পাই A[i] >= pivot এবং A[j] <= pivot, সেগুলো সোয়াপ করলে ইনভারিয়েন্টগুলো বজায় থাকে এবং অনশ্রেণীকৃত মধ্যম অংশ ছোট হয়ে আসে।
i ডান দিকে চলে যাবে; পার্টিশনকে তবুও টার্মিনেট করে এবং যৌক্তিক p রিটার্ন করতে হবে।j বাম দিকে চলে যাবে; একই টার্মিনেশন উদ্বেগ আছে।< বনাম <=), পয়েন্টার আটকে যেতে পারে। হোয়ার স্কিম কনসিস্টেন্ট নিয়মের ওপর নির্ভর করে যাতে অগ্রগতি চালু থাকে।বিভিন্ন পার্টিশন স্কিম আছে (Lomuto, Hoare, তিন-ভাবে পার্টিশনিং)। মূল কথা হলো একটি স্কিম বাছুন, তার কন্ট্রাক্ট স্পষ্টভাবে বলুন, এবং একই কন্ট্রাক্টের বিরুদ্ধে কোড রিভিউ করুন।
রিকার্শন সবচেয়ে সহজে বিশ্বাসযোগ্য হয় যখন আপনি দুইটি প্রশ্নের স্পষ্ট উত্তর দিতে পারেন: কখন বন্ধ হয়? এবং প্রতিটি ধাপ কেন বৈধ? হোয়ার-স্টাইল চিন্তা সাহায্য করে কারণ এটি আপনাকে বলতেই বাধ্য করে যে কোন শর্ত একটি কলের আগে সত্য এবং কল ফিরে এলে কী সত্য থাকবে।
একটি রিকারসিভ ফাংশনের অন্তত একটি বেস কেস থাকা উচিত যেখানে আর কোনো রিকার্সিভ কল হবে না এবং তবুও প্রতিশ্রুত ফলাফল বজায় থাকবে।
স্যর্টিং-এ একটি প্রচলিত বেস কেস হল “লম্বাই 0 বা 1”—এগুলো ইতিমধ্যেই সাজানো। এখানে “সাজানো” পরিষ্কারভাবে বলা উচিত: ≤ অর্ডারিং সম্পর্কের জন্য আউটপুট অ্যারেটি সাজানো যদি প্রতিটি i < j-এর জন্য a[i] ≤ a[j] হয়। (ইকুয়াল উপাদানের অরিজিনাল অর্ডার রাখার বিষয়টি আলাদা প্রপার্টি, stability; কুইকসোর্ট সাধারণত স্টেবল নয় যদি আপনি এটিকে স্টেবল করতে না ডিজাইন করেন)।
প্রতিটি রিকার্সিভ ধাপে ফাংশনকে কঠোরভাবে ছোট ইনপুটে কল করা উচিত। এই “ছোট হওয়া” আপনার টার্মিনেশন যুক্তি: সাইজ কমে এবং 0-এর নিচে নামতে পারে না, তাই আপনি অনন্ত রিকার্সনে পড়তে পারবেন না।
ছোট হওয়া স্ট্যাক সেফটির জন্যও গুরুত্বপূর্ণ। সঠিক কোডও স্ট্যাক গভীরতা অত্যধিক হলে ক্র্যাশ করতে পারে। কুইকসোর্টে অসমভাবে বিভাজন করলে গভীর রিকার্সন হতে পারে—এটি টার্মিনেশন প্রমাণের পাশাপাশি বাস্তব একস্মৃতি সতর্কতা।
কুইকসোর্টের ওয়ার্সট-কেস সময় জটিলতা O(n²) তে নেমে আসতে পারে যখন পার্টিশন খুবই অসমান হয়, কিন্তু সেটা পারফরম্যান্সের বিষয়—শুদ্ধতার ব্যর্থতা নয়। যুক্তির লক্ষ্য হলো: ধরে নিন পার্টিশন উপাদান রক্ষা করে এবং pivot অনুসারে ভাগ করে, সাবরেঞ্জগুলো সঠিকভাবে সাজালে পুরো রেঞ্জটি সিম্পল ডেফিনিশন অনুযায়ী সাজানো হবে।
টেস্টিং ও প্রমাণ-স্টাইল যুক্তি একই লক্ষ্য—আত্মবিশ্বাস—প্রাপ্তির বিভিন্ন পথ।
টেস্টগুলো কংক্রিট ভুল ধরতে দুর্দান্ত: একটি অফ-বাই-ওয়ান, একটি মিসিং এজ কেস, একটি রিগ্রেশন। কিন্তু একটি টেস্ট সুইট ইনপুট স্পেসের মাত্র নমুনা নিতে পারে। এমনকি “100% কভারেজ”ও মানে সেই নয় যে “সব আচরণ পরীক্ষা করা হয়েছে”; বেশিরভাগ সময় মানে “সব লাইন চালানো হয়েছে।”
প্রমাণ-স্টাইল যুক্তি (বিশেষত হোয়ার-স্টাইল) একটি স্পেসিফিকেশন থেকে শুরু করে প্রশ্ন করে: যদি এই প্রিকন্ডিশনগুলো সত্য থাকে, তাহলে কোড কি সর্বদা পোস্টকন্ডিশান প্রতিষ্ঠা করবে? যখন আপনি এটি ভালভাবে করেন, আপনি কেবল একটি বাগ খুঁজে পান না—প্রায়শই পুরো একটি বাগ শ্রেণীকে (যেমন “অ্যারে অ্যাক্সেস রেঞ্জের বাইরে যায়” বা “লুপ পার্টিশন প্রপার্টি ভাঙে”) দূর করতে পারেন।
একটি পরিষ্কার স্পেক একটি টেস্ট জেনারেটর।
যদি আপনার পোস্টকন্ডিশন বলে “আউটপুট সাজানো এবং ইনপুটের permutation,” আপনি স্বয়ংক্রিয়ভাবে টেস্ট আইডিয়া পেয়ে যাবেন:
স্পেক আপনাকে বলে “সঠিক” কী, এবং টেস্টগুলো তা বাস্তবে মেলে কি না তা চেক করে।
প্রপার্টি-ভিত্তিক টেস্টিং প্রুফ এবং উদাহরণগত টেস্টিং-এর মধ্যে মাঝপথে আছে। হাত দিয়ে কয়েকটি কেস বাছাই করার বদলে, আপনি প্রপার্টি বর্ণনা করেন এবং একটি টুল অসংখ্য ইনপুট জেনারেট করে।
সাজানোর জন্য দুটি সহজ প্রপার্টি অনেকদূর যায়:
এই প্রপার্টিগুলো আসলে executable পোস্টকন্ডিশন।
একটি হালকা ওজন রুটিন যা স্কেলে করে:
আপনি যদি এটিকে প্রতিষ্ঠা করতে চান, “স্পেক + যুক্তি নোট + টেস্ট” কে আপনার PR টেমপ্লেট বা কোড রিভিউ চেকলিস্টে রাখুন (দেখুন /blog/code-review-checklist)।
যদি আপনি একটি ভিব-কোডিং ওয়ার্কফ্লো ব্যবহার করেন (চ্যাট-ভিত্তিক ইন্টারফেস থেকে কোড জেনারেট করা), একই শৃঙ্খলা প্রয়োগযোগ্য—এবং সম্ভবত আরও প্রয়োজনীয়। উদাহরণস্বরূপ Koder.ai-তে আপনি Planning Mode-এ শুরু করে preconditions/postconditions পিন করতে পারেন, তারপর property-based টেস্ট যোগ করার সময় স্ন্যাপশট ও রোলব্যাক ব্যবহার করে ইটারেট করতে পারেন। টুলটি ইমপ্লিমেন্টেশন দ্রুত করে, কিন্তু স্পেকই রাখে “দ্রুত” কে “শীতল” থেকে “ভঙ্গুর” হওয়া থেকে রক্ষা করে।
শুদ্ধতা কেবল “প্রোগ্রাম সঠিক মান রিটার্ন করে” ব্যাপার নয়। সেফটি মাইন্ডসেট একটি ভিন্ন প্রশ্ন করে: কোন ফলাফলগুলি অগ্রহণযোগ্য, এবং কিভাবে আমরা সেগুলো প্রতিরোধ করব—এমনকি কোড চাপলে, ভুলভাবে ব্যবহার করলে বা আংশিকভাবে ব্যর্থ হলেও? বাস্তবে, সেফটি হল শুদ্ধতা একটি অগ্রাধিকারের তালিকা: কিছু ব্যর্থতা অশান্তিকর, আর কিছু আর্থিক ক্ষতি, প্রাইভেসি লঙ্ঘন বা শারীরিক ক্ষতি করতে পারে।
বাগ হল কোড বা ডিজাইনের ত্রুটি। হ্যাজার্ড হল এমন একটি পরিস্থিতি যা অগ্রহণযোগ্য ফলাফল ঘটাতে পারে। একটি বাগ এক প্রেক্ষাপটে নিরীহ হতে পারে এবং অন্য প্রেক্ষাপটে বিপজ্জনক।
উদাহরণ: একটি ফটোগ্যালারি-তে অফ-বাই-ওয়ান ত্রুটি একটি ছবিকে ভুলভাবে লেবেল করতে পারে; একই ত্রুটি একটি মেডিসিন ডোজ ক্যালকুলেটরে রোগীকে ক্ষতিগ্রস্ত করতে পারে। সেফটি চিন্তা আপনাকে কোড আচরণকে ফলাফলের সঙ্গে যুক্ত করতে বাধ্য করে—শুধু স্পেক কমপ্লায়েন্স নয়।
ধারণা ভারী ফরমাল মেথড লাগবে না যত তাড়াতাড়ি আপনি কিছু রুটিন অভ্যাস মানেন তা সঙ্গে সঙ্গে সেফটি বাড়ায়:
এই কৌশলগুলো হোয়ার-স্টাইল যুক্তির সাথে ভালোভাবে জোড়া যায়: আপনি প্রিকন্ডিশন স্পষ্ট করেন (কোন ইনপুট গ্রহণযোগ্য) এবং পোস্টকন্ডিশনে সেফটি প্রপার্টি রাখেন (কী কখনও ঘটবে না)।
সেফটি-উপযোগী চেকগুলোর কিছু খরচ থাকে—CPU, জটিলতা, বা মাঝে মাঝে ভুল প্রত্যাখ্যান।
সেফটি চিন্তা সৌন্দর্যের প্রমাণ দেখানো নয়—এটি সেই ব্যর্থ মোডগুলো প্রতিরোধ করবে যেগুলো আপনি সহ্য করতে পারেন না।
কোড রিভিউই হলো যেখানে শুদ্ধতা চিন্তা দ্রুত ফল দেয়, কারণ আপনি বিজ্ঞদের চেয়ে বহু আগে অনুপস্থিত অনুমানগুলি ধরতে পারেন। হোয়ার-র মূল কৌশল—"এখানে কী সত্য হতে হবে" এবং "এখানে কী সত্য থাকবে"—রিভিউ প্রশ্নে সহজে অনুবাদ করা যায়।
একটি চেঞ্জ পড়ার সময় প্রতিটি গুরুত্বপূর্ণ ফাংশনকে একটি ছোট প্রতিশ্রুতি হিসেবে ফ্রেম করুন:
একটি সহজ রিভিউ অভ্যাস: আপনি যদি এক বাক্যে প্রি/পোস্ট কন্ডিশন বলতে না পান, কোডটি সম্ভবত স্পষ্ট কাঠামো প্রয়োজন।
ঝুঁকিপূর্ণ বা কেন্দ্রীয় ফাংশনের উপরে একটি ছোট কন্ট্রাক্ট কমেন্ট যোগ করুন। এটি কনক্রিট রাখুন: ইনপুট, আউটপুট, সাইড-ইফেক্ট এবং ত্রুটি।
def withdraw(account, amount):
"""Contract:
Pre: amount is an integer > 0; account is active.
Post (success): returns new_balance; account.balance decreased by amount.
Post (failure): raises InsufficientFunds; account.balance unchanged.
"""
...
এই মন্তব্যগুলো ফর্মাল প্রমাণ নয়, কিন্তু রিভিউয়ারের কাছে কী চেক করতে হবে তা পরিষ্কার করে।
নিরাপত্তা বা ঝুঁকিপূর্ণ কোড রিভিউ করার সময় বেশি স্পষ্ট হন—বিশেষত যখন কোড হ্যান্ডেল করে:
যদি চেঞ্জ এগুলোকে স্পর্শ করে, জিজ্ঞেস করুন: “প্রিকন্ডিশন কোথায়, এবং সেগুলো কোথায় প্রয়োগ হচ্ছে?” এবং “ত্রুটি হলে আমরা কি গ্যারান্টি দিই যে সিস্টেম নিরাপদ থাকবে?”
ফর্মাল যুক্তি মানে আপনার পুরো কোডবেসকে একটি গাণিতিক পেপারে পরিণত করা নয়। লক্ষ্য হলো সেই জায়গাগুলোতে অতিরিক্ত নিশ্চয়তা ব্যয় করা যেখানে লাভ বেশি: জায়গাগুলো যেখানে “টেস্টে ঠিক আছে” যথেষ্ট নয়।
সেগুলো ভালো কাজ করে যখন আপনার একটি ছোট, ক্রিটিক্যাল মডিউল থাকে যাকে সবকিছু নির্ভর করে (অথেনটিকেশন, পেমেন্ট রুল, পারমিশন, সেফটি ইন্টারলক), বা একটি জটিল অ্যালগরিদম যেখানে অফ-বাই-ওয়ান ভুল দীর্ঘ সময় লুকিয়ে থাকে (পার্সার, শিডিউলার, ক্যাশিং/এভিকশন, কনকারেন্সি প্রিমিটিভ, পার্টিশন-শৈলীর কোড)।
একটি দরকারী নিয়ম: যদি একটি বাগ বাস্তব ক্ষতি, বড় আর্থিক ক্ষতি, বা চুপচাপ ডেটা করাপশন ঘটাতে পারে, আপনি সাধারণ রিভিউ + টেস্টের বাইরে আরও চান।
আপনি "হালকা" থেকে "ভারী" পর্যন্ত বেছে নিতে পারেন, এবং প্রায়ই ভাল ফলাফল আসে যখন আপনি এগুলো একত্রে ব্যবহার করেন:
ফর্মালিটির গভীরতা নির্ধারণ করুন:
অবশ্যই, আপনি ধাপে ধাপে "ফর্মালিটি" বাড়াতে পারেন: প্রথমে স্পষ্ট কন্ট্রাক্ট ও ইনভারিয়েন্ট, তারপর অটোমেশন দিয়ে সেগুলো বজায় রাখুন। Koder.ai-র মতো টিমে দ্রুত UI, ব্যাকএন্ড ও স্কিমা জেনারেশন হলেও আপনি স্ন্যাপশট/রোলব্যাক ও CI-তে কন্ট্রাক্টের টেস্ট রেখে দ্রুততার সঙ্গে নিশ্চয়তা বজায় রাখতে পারেন।
পরিকল্পনা বা কোড রিভিউতে “আর কি ফর্মাল করা উচিত?” গেট হিসেবে ব্যবহার করুন:
আরও পড়ার জন্য: design-by-contract, property-based testing, স্টেট মেশিনে model checking, আপনার ভাষার জন্য স্ট্যাটিক অ্যানালাইজার, এবং প্রুফ অ্যাসিস্ট্যান্ট ও ফরমাল স্পেসিফিকেশনের প্রারম্ভিক বিষয়বস্তু।
শুদ্ধতা মানে প্রোগ্রামটি একটি সম্মত স্পেসিফিকেশন মেনে চলে: নির্ধারিত ইনপুট ও প্রাসঙ্গিক সিস্টেম স্টেটের জন্য এটি প্রত্যাশিত আউটপুট ও সাইড-ইফেক্ট তৈরি করে এবং ত্রুটি হলে প্রতিশ্রুত ভেবে আচরণ করে। “চেক করে দেখেছি, কাজ করেছে” সাধারণত বোঝায় আপনি মাত্র কয়েকটি উদাহরণ পরীক্ষা করেছেন, পুরো ইনপুট স্পেস বা জটিল বাউন্ডারি কন্ডিশন নয়।
Requirements হল ব্যবসায়িক লক্ষ্য (যেমন “তালিকাটি ডিসপ্লের জন্য সাজাও”)। স্পেসিফিকেশন হল সেই লক্ষ্যটির সুনির্দিষ্ট, যাচাইযোগ্য প্রতিশ্রুতি (যেমন “নতুন তালিকা রিটার্ন করবে, ঊর্ধ্বক্রমে সাজানো, ইনপুট একই সংখ্যার উপাদান বহন করবে”)। Implementation হল আপনার লেখা কোড। ভুল প্রায়ই তখন ঘটে যখন দল requirements থেকে সরাসরি কোডে লাফ দেয় এবং মাঝের যাচাইযোগ্য প্রতিশ্রুটিটা লেখে না।
Partial correctness: যদি কোড রিটার্ন করে, ফলাফল ঠিক।
Total correctness: কোডটি অবশ্যই রিটার্ন করবে এবং ফলাফল ঠিক হবে—অর্থাৎ টারমিনেশনও দাবির অংশ।
প্র্যাকটিক্যালি, total correctness গুরুত্বপূর্ণ যখন “অন্তহীনভাবে অপেক্ষা করা” ব্যবহারকারীর কাছে ব্যর্থতা, রিসোর্স লিক বা সেফটি রিস্ক তৈরি করে।
একটি Hoare triple {P} C {Q} এমন একটি চুক্তির মতো পড়ে:
P (precondition): C চালানোর আগে কী সত্য হতে হবেC: কোডের অংশপ্রিকন্ডিশন হল সেই জিনিসগুলো যা কোড চালানোর আগে হতে হবে (যেমন “ইনডেক্সগুলি রেঞ্জে আছে”, “উপাদানগুলো তুলনাযোগ্য”, “লক ধরে আছে”)। যদি কলাররা এগুলো ভঙ্গ করতে পারে, তাহলে বিকল্প হিসাবে:
অন্যথায় আপনার পোস্টকন্ডিশন কেবল কামনাই থেকে যাবে।
একটি লুপ ইনভারিয়েন্ট হল এমন একটি বক্তব্য যা লুপ শুরু হওয়ার আগেই সত্য, প্রতিটি ইটারেশনের পরে সত্য থাকে, এবং লুপ শেষ হওয়ার সময়ও সত্য থাকে। কিছু পুনঃব্যবহারযোগ্য টেমপ্লেট:
0 <= i <= n)আপনি যদি ইনভারিয়েন্ট ব্যাখ্যা করতে না পারেন, লুপটি সম্ভবত একসাথে অনেক কাজ করছে বা বাউন্ডারি অস্পষ্ট।
সাধারণত একটি মেজার (variant) নামকরণ করা হয় যা প্রতিটি ইটারেশনে ছোট হয় এবং চিরতরে ছোট হতে পারে না, যেমন:
n - i প্রতি ইটারেশনে 1 করে ছোটানোযদি আপনি কোনো হ্রাসমান মেজার না খুঁজে পান, তাহলে এটি একটি বাস্তব নন-টার্মিনেশন ঝুঁকি নির্দেশ করতে পারে—বিশেষত ডুপ্লিকেট বা আটকে থাকা পয়েন্টারের ক্ষেত্রে।
Quicksort-এ partition হলো ছোট কিন্তু অত্যন্ত গুরুত্বপূর্ণ রুটিন। যদি partition সামান্যও ভুল হয়, ফলাফল হতে পারে:
এজন্য partition-এর কন্ট্রাক্ট স্পষ্টভাবে বলুন: বাম দিকে কী সত্য, ডান দিকে কী সত্য, এবং উপাদানগুলো কেবল পুনর্বিন্যাস হয়েছে (permutation)।
ডুপ্লিকেট এবং pivot-এর সমান উপাদানগুলো সঠিকভাবে হ্যান্ডল না করলে সমস্যায় পড়া স্বাভাবিক:
i/j আটকে থাকতে পারে যদি == বা <= ব্যাবহার অসঙ্গত হয়ব্যবহারিক নিয়ম: একটি partition স্কিম (Hoare, Lomuto, তিন-ভাবে) বেছে নিন এবং তুলনা নিয়ম কনসিস্টেন্ট রাখুন; প্রয়োজন হলে তিন-ভাবে পার্টিশন ব্যবহার করুন, যা ডুপ্লিকেটের ক্ষেত্রে এবং রিকার্শন গভীরতা উভয়ের জন্য উপকারী।
টেস্টিং কনক্রিট ভুলগুলো ধরতে চমৎকার; reasoning (প্রমাণধাঁচ) পুরো শ্রেণীর বাগ বাতিল করতে সাহায্য করে (যেমন বাউন্ডস সেফটি, ইনভারিয়েন্ট রক্ষা, টার্মিনেশন)। একটি ব্যবহারিক হাইব্রিড ওয়ার্কফ্লো:
সাজানোর জন্য দুইটি উচ্চ-মূল্যের প্রপার্টি:
Q (postcondition): C সম্পন্ন হওয়ার পরে কী সত্য হবে, যদি P সত্য ছিলনোট: আপনাকে বাস্তবে এই নোটেশন কোডে লিখতেই হবে না—রিভিউ ও ডিজাইনে “কী শর্তে চালানো হচ্ছে” ও “চালানোর পরে কী গ্যারান্টি” ভাবাটা যথেষ্ট ব্যবহারিক সুবিধা দেয়।