টনি হোয়ার-এর শুদ্ধতা ধারণা: লজিক থেকে নিরাপদ কোড

কেন “শুদ্ধতা” মানে শুধু “এটা কাজ করেছে” নয়

যখন মানুষ বলে কোনো প্রোগ্রাম “শুদ্ধ” তাতে তারা প্রায়শই বোঝায়: “আমি এটা কয়েকবার চালিয়েছি এবং আউটপুট ঠিক দেখাচ্ছে।” এটা একটা উপযোগী সংকেত—কিন্তু এটা শুদ্ধতা নয়। সরলভাবে, শুদ্ধতা মানে প্রোগ্রাম তার স্পেসিফিকেশন মেনে চলে: প্রত্যেক অনুমোদিত ইনপুটের জন্য এটি প্রয়োজনীয় ফলাফল তৈরি করে এবং স্টেট পরিবর্তন, সময়সীমা এবং ত্রুটির সম্পর্কে যেসব নিয়ম আছে সেগুলো রক্ষা করে।

কিন্তু ধাঁধাটি হল “স্পেসিফিকেশন মেনে চলে” শোনায় সহজ—কিন্তু করা কঠিন।

কেন শুদ্ধতা সত্যিই কঠিন

প্রথমত, স্পেসিফিকেশনগুলো প্রায়ই অস্পষ্ট হয়। একটি প্রোডাক্ট রিকোয়ারমেন্ট বলতে পারে “তালিকাটি সাজাও”, কিন্তু এটা কি স্থিতিশীল সাজানো (stable sorting) মানে? ডুপ্লিকেট মান, খালি তালিকা, বা অ-সংখ্যাতত্ত্ব উপাদানগুলো কীভাবে হবে? স্পেসিফিকেশনে যদি না বলা থাকে, আলাদা মানুষ আলাদা অনুমান করবে।

দ্বিতীয়ত, এজ কেসগুলো বিরল নয়—তবে তারা কম ঘন ঘন পরীক্ষা করা হয়। Null মান, ওভারফ্লো, অফ-বাই-ওয়ান সীমা, অস্বাভাবিক ব্যবহারকারী ক্রম এবং অননুজ্ঞেয় বাহ্যিক ব্যর্থতা “এটা কাজ করে” থেকে “প্রোডাকশনে ব্যর্থ” এ পরিণত করতে পারে।

তৃতীয়ত, চাহিদা পরিবর্তন হয়। একটি প্রোগ্রাম গতকালের স্পেসিফিকেশনের প্রশ্নে শুদ্ধ হতে পারে এবং আজকের স্পেসিফিকেশনের তুলনায় ভুল হতে পারে।

এই পোস্টের বাকি অংশ থেকে কী আশা করবেন

টনি হোয়ার-এর বড় অবদান ছিল সবকিছুই সবসময় প্রমাণ করা উচিত—এই দাবি নয়। বরং তিনি বলেছিলেন যে আমরা কোড কোন কাজ করবে তা আরও সুনির্দিষ্ট ভাবে ব্যাখ্যা করতে পারি—এবং তা শৃঙ্খলাবদ্ধভাবে বিশ্লেষণ করতে পারি।

এই পোস্টে আমরা তিনটি সংযুক্ত থ্রেড অনুসরণ করব:

• হোয়ার লজিক: প্রি-ফলাফল এবং পোস্টকন্ডিশন ব্যবহার করে হালকা, গঠিত যুক্তি।
• কুইকসোর্ট: একটি পরিচিত অ্যালগরিদম যা দেখায় কীভাবে ছোট “স্বচ্ছ” ধাপগুলো (যেমন পার্টিশন) সতর্ক চিন্তা দরকার।
• সেফটি মাইন্ডসেট: নির্মম ফলাফল ঘটতে পারে এমন পরিস্থিতিতে শুদ্ধতাকে ব্যবহারিক দায়িত্ব হিসেবে দেখা।

অধিকাংশ দল সম্পূর্ণ ফর্মাল প্রমাণ লিখবে না। কিন্তু আংশিক, “প্রমাণ-স্টাইল” চিন্তা তবুও বাগ ধরতে সহজ করে, রিভিউ আরও ধারালো করে, এবং কোড শিপ করার আগে আচরণ স্পষ্ট করে।

টনি হোয়ার সংক্ষেপে: এমন ধারণা যা প্রতিদিনের কোডে পৌঁছে গেছে

টনি হোয়ার এমন বিরল কম্পিউটার বিজ্ঞানীদের একজন যাদের গবেষণা কেবল পেপার বা ক্লাসরুমে আটকে থাকে না। তিনি একাডেমিয়া ও ইন্ডাস্ট্রির মধ্যে চলাফেরা করেছেন, এবং তিনি প্রত্যেক দলের সম্মুখীন হওয়া ব্যবহারিক প্রশ্ন নিয়ে চিন্তা করেছেন: বিশেষ করে উচ্চ স্টেকস থাকলে কিভাবে আমরা নিশ্চিত হবো যে প্রোগ্রামটি আমরা যা ভাবি তা করে?

এই পোস্টের জন্য গুরুত্বপূর্ণ অবদানগুলো

এই লেখাটি কিছু হোয়ার ধারণার উপর কেন্দ্রিত যা বাস্তব কোডবেজে প্রায়ই দেখা যায়:

• হোয়ার লজিক: preconditions, postconditions এবং পরিচিত হোয়ার ট্রিপল {P} C {Q} ব্যবহার করে প্রোগ্রাম আচরণ বর্ণনা করার উপায়।
• লুপ ইনভারিয়েন্ট: লুপগুলোর বিষয়ে ডায়াগনস্টিক প্রথা, “আমার মেশিনে কাজ করেছে” ধরণের যুক্তি ছাড়িয়ে যেতে সহায়ক।
• কুইকসোর্ট (বিশেষ করে এর পার্টিশন ধাপ): একটি বিখ্যাত উদাহরণ যেখানে ছোট, সুনির্দিষ্ট শুদ্ধতার বিবৃতি অনেক কিছু স্পষ্ট করে।
• সেফটি চিন্তা: শুদ্ধতা কোনো বিলাসিতা নয়; তা হয় অনিচ্ছাকৃত অস্বস্তি বনাম ক্ষতির মধ্যে পার্থক্য।

এই পোস্টে আমরা যা করব না

এখানে আপনি গভীর গাণিতিক ফর্মালিজম পাবেন না, এবং আমরা কুইকসোর্টের সম্পূর্ণ, মেশিন-চেকযোগ্য প্রমাণ দেওয়ার চেষ্টা করব না। লক্ষ্য হলো ধারণাগুলো অ্যাক্সেসযোগ্য রাখা: আপনার যুক্তি পরিষ্কার করতে যথেষ্ট কাঠামো, কিন্তু কোড রিভিউকে গ্র্যাজুয়েট সেমিনারে পরিণত না করেই।

কেন তার কাজ সাধারণ প্রোগ্রামিংকে প্রভাবিত করে

হোয়ার-এর ধারণাগুলো দৈনন্দিন সিদ্ধান্তে অনুবাদিত হয়: একটি ফাংশন কোন অনুমানগুলোর উপর নির্ভর করে, কলারকে কী গ্যারান্টি দেয়, লুপের মাঝখানে কী বজায় থাকতে হবে, এবং রিভিউতে “প্রায়ঠিক” পরিবর্তনগুলো কীভাবে শনাক্ত করবেন। এমনকি আপনি যদি স্পষ্টভাবে {P} C {Q} না লেখেন, সেই আকৃতির চিন্তা API, টেস্ট এবং জটিল কোড নিয়ে কথোপকথন উন্নত করে।

বাস্তবে “শুদ্ধতা” কী মানে

হোয়ার-এর দৃষ্টিভঙ্গি হলো “কয়েকটি উদাহরণে ঠিক ছিল” এর চেয়েও কঠোর: শুদ্ধতা হল সম্মত প্রতিশ্রুতি পূরণ—না যে ছোট নমুনায় ঠিক দেখাচ্ছে।

Requirements vs. specification vs. implementation

• Requirements: স্টেকহোল্ডারের চাহিদা সাধারণ ভাষায় (কি চায়)।
• Specification: সেই চাহিদার সুনির্দিষ্ট, যাচাইযোগ্য রূপ (ফাংশনকে কী করতে হবে)।
• Implementation: আপনি যে কোড লিখেছেন (কীভাবে করে)।

বাগ প্রায়ই ঘটে যখন দল মাঝের ধাপটি এড়িয়ে সরাসরি requirements থেকে কোডে লাফায়, ফলে “প্রতিশ্রুতি” অস্পষ্ট থাকে।

আংশিক শুদ্ধতা বনাম সম্পূর্ণ শুদ্ধতা

দুইটি দাবি প্রায়ই একসাথে মিশে যায়:

• আংশিক শুদ্ধতা: যদি কোড রিটার্ন করে, ফলাফল সঠিক।
• সম্পূর্ণ শুদ্ধতা: কোড রিটার্ন করবে এবং ফলাফল সঠিক—অর্থাৎ টার্মিনেশন দাবির অংশ।

বাস্তব সিস্টেমে, “কখনও শেষ না হওয়া” ঠিক না হওয়ার মতোই ক্ষতিকর হতে পারে।

শুদ্ধতা সবসময় অনুমানগুলোর উপর নির্ভর করে

শুদ্ধতার বিবৃতিগুলো সার্বজনীন নয়; সেগুলো নির্ভর করে অনুমানগুলোর উপর, যেমন:

• ইনপুট (উদাহরণ: তালিকা মেমরিতে ফিট করে, উপাদান তুলনাযোগ্য)
• নিয়মাবলী (উদাহরণ: সময়সীমা, ইন্টিজারের রেঞ্জ)
• পরিবেশ (উদাহরণ: কনকারেন্সি, I/O ব্যর্থতা, কনফিগারেশন)

অনুমানগুলো স্পষ্ট করা “আমার মেশিনে কাজ করে” কে অন্যদের বোঝার যোগ্য অঙ্গীকারে পরিণত করে।

একটি ক্ষুদ্র স্পেসিফিকেশন উদাহরণ

ধরা যাক একটি ফাংশন sortedCopy(xs) আছে।

একটি দরকারী স্পেসিফিকেশন হতে পারে: “নতুন তালিকা ys রিটার্ন করবে, যেখানে (1) ys ঊর্ধ্বক্রমে সাজানো, এবং (2) ys-এ xs-এর উপাদানসমূহ ঠিক সমান গণনায় আছে, এবং (3) xs অপরিবর্তিত আছে।”

এখন “সঠিক” মানে হলো কোডটি উক্ত তিনটি পয়েন্ট উল্লিখিত অনুমানগুলোর অধীনে পূরণ করছে—শুধু যে আউটপুটটি দ্রুত পরীক্ষা করে সাজানো মনে হচ্ছে তা নয়।

হোয়ার লজিক বেসিক: প্রিকন্ডিশন, পোস্টকন্ডিশন, ট্রিপল

হোয়ার লজিক কোড নিয়ে এমনভাবে আলোচনা করার উপায় দেয় যেটা আপনি চুক্তি বলেই ভাববেন: যদি আপনি এমন একটি স্টেটে শুরু করেন যা নির্দিষ্ট শর্তগুলো পূরণ করে, এবং আপনি এই কোডটি চালান, আপনি এমন একটি স্টেটে শেষ করবেন যা নির্দিষ্ট গ্যারান্টি পূরণ করে।

কোর নোটেশন হলো হোয়ার ট্রিপল:

{precondition} program {postcondition}

Preconditions: আপনি কী অনুমান করেন

প্রিকন্ডিশন জানায় কোড অংশ চালানোর আগে কী সত্য হতে হবে। এটি আপনি আশা করছেন এমন কিছু নয়; এটি কোডটির চলার জন্য যা প্রয়োজন।

উদাহরণ: ধরা যাক একটি ফাংশন দুটি সংখ্যার গড় রিটার্ন করে বিনা ওভারফ্লো চেকের।

• Precondition: a + b ইন্টিজার টাইপে ফিট করে
• Program: avg = (a + b) / 2
• Postcondition: avg হল a ও b-র গাণিতিক গড়

যদি প্রিকন্ডিশন বজায় না থাকে (ওভারফ্লো সম্ভব), পোস্টকন্ডিশন আর প্রযোজ্য নাও হতে পারে। ট্রিপলটি আপনাকে তা জাহির করতে বাধ্য করে।

Postconditions: আপনি কী গ্যারান্টি দেন

পোস্টকন্ডিশন জানায় কোডটি চালানোর পরে কী সত্য হবে—ধরা যাক প্রিকন্ডিশন মেনে চলেছে। ভালো পোস্টকন্ডিশনগুলো স্পষ্ট ও চেকযোগ্য হওয়া উচিত। “রেজাল্ট ভ্যালিড” বলার বদলে বলুন “ভ্যালিড” মানে কী: সাজানো, অ-নেগেটিভ, নির্দিষ্ট সীমার মধ্যে, নির্দিষ্ট ফিল্ড ছাড়া অপরিবর্তিত ইত্যাদি।

অ্যাসাইনমেন্ট ও সিকোয়েন্সিং (চিহ্নলোচনার ওভারলোড ছাড়া)

হোয়ার লজিক ক্ষুদ্র বিবৃতিগুলো থেকে বহু ধাপের কোড পর্যন্ত স্কেল করে:

• অ্যাসাইনমেন্ট স্পষ্টভাবে স্টেট পরিবর্তন করে। যুক্তি করা হয়: x = x + 1-এর পরে x সম্পর্কে কোন কোন সত্যতা প্রযোজ্য?
• সিকোয়েন্সিং (“এটা করো, তারপর ওটা”) গ্যারান্টিগুলো চেইন করে: যদি ধাপ 1 ধাপ 2-এর প্রিকন্ডিশন প্রতিষ্ঠা করে, তবে পুরো ব্লককে বিশ্বাস করা সহজ হয়।

মুখ্য উদ্দেশ্য হলো প্রত্যাশা পাঠযোগ্য করা: স্পষ্ট অনুমান, স্পষ্ট ফলাফল, এবং রিভিউতে “এটা কাজ করে” কথোপকথনগুলো কমানো।

বাস্তব দলগুলোর জন্য লুপ ইনভারিয়েন্ট লিখতে পারা

লুপ ইনভারিয়েন্ট এমন একটি বক্তব্য যা লুপ শুরুর আগে সত্য, প্রতিটি ইটারেশনের পরে সত্য থাকে, এবং লুপ শেষের সময়ে সত্য থাকে। এটি একটি সাধারণ ধারণা কিন্তু বড় সুবিধা দেয়: এটি “কাজ করছে” কথাকে এমন এক দাবিতে পরিণত করে যা আপনি প্রতিটি ধাপেই চেক করতে পারেন।

কেন ইনভারিয়েন্ট হাত-ধানাপাওয়া যুক্তি বন্ধ করে দেয়

ইনভারিয়েন্ট না থাকলে রিভিউতে প্রায়শই শোনা যায়: “আমরা তালিকাটি ইটারেট করি এবং ধীরে ধীরে জিনিস ঠিক করি।” একটি ইনভারিয়েন্ট নির্দিষ্ট করে দেয়: এই মুহূর্তে ঠিক কীই ঠিক করা হয়েছে, যদিও লুপ শেষ হয়নি। একবার আপনি সেটা স্পষ্টভাবে বলতে পারেন, অফ-বাই-ওয়ান ত্রুটি ও মিসিং কেসগুলো শনাক্ত করা সহজ হয়, কারণ সেগুলো এমন মুহূর্ত হিসেবে দেখা যায় যেখানে ইনভারিয়েন্ট ভাঙবে।

পুনঃব্যবহারযোগ্য ইনভারিয়েন্ট টেমপ্লেট

দৈনন্দিন কোডের অধিকাংশই কিছু নির্ভরযোগ্য টেমপ্লেট ব্যবহার করতে পারে।

1) বাউন্ডস / ইনডেক্স সেফটি

ইনডেক্সগুলো নিরাপদ রেঞ্জে রাখুন।

• 0 <= i <= n
• low <= 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) ক্রমে আসে, এবং কোনো মান হারায় না বা নতুন মান গঠন করা হয় না। অ্যালগরিদমের উচ্চ-স্তরের রূপটি সহজ:

1. একটি pivot মান বাছুন।
2. রেঞ্জটি পার্টিশন করুন যাতে “pivot-এর চেয়ে ছোট” উপাদান এক পাশে চলে যায় এবং “বড়” অন্য পাশে (সমানগুলোর জন্য কিছু নিয়ম)।
3. বাম ও ডান সাবরেঞ্জে রিকার্স করুন।

এটি একটি চমৎকার শিক্ষণ উদাহরণ কারণ এটি মাথায় ধারণ করার জন্য ছোট কিন্তু অপ্রচুরতা দেখায় যেখানে অনানুষ্ঠানিক যুক্তি ব্যর্থ হয়। কয়েকটি র‌্যান্ডম টেস্টে কাজ করে দেখানো কুইকসোর্টের তবুও কিছু ইনপুট বা বাউন্ডারি কন্ডিশনে ভুল থাকতে পারে।

কোন জিনিসগুলো “স্বচ্ছ” ইমপ্লিমেন্টেশনকে ভাঙে

কিছু সমস্যা সাধারণত বেশিরভাগ বাগের কারণ:

• ডুপ্লিকেটস: আপনার পার্টিশন যদি “pivot-র সমান” উপাদানগুলিকে অসামঞ্জস্যভাবে হ্যান্ডল করে, তাহলে আপনি অনন্ত রিকার্সনে পড়তে পারেন (সাবরেঞ্জ ছোট হচ্ছে না) বা পার্টিশন নিজেই নিজস্ব নিয়ম ভাঙবে।
• খালি বা এক-উপাদান রেঞ্জ: বেস কেস সঠিক না হলে আউট-অফ-বাউন্ডস বা অনন্ত রিকার্সন হতে পারে।
• অফ-বাই-ওয়ান ইনডেক্স: পার্টিশন অ্যালগরিদম প্রায়শই দুইটি পয়েন্টার ব্যবহার করে; একটি ভুল তুলনা বা ইনক্রিমেন্ট একটি উপাদান ফেলে দিতে পারে বা রেঞ্জের বাইরে সোয়াপ করতে পারে।

আসলে কী প্রমাণ করতে হয়

হোয়ার-স্টাইল যুক্তিতে, প্রমাণ সাধারণত দুটি অংশে ভাগ করা হয়:

• পার্টিশন শুদ্ধতা: পার্টিশনের পরে বাম পাশে প্রতিটি উপাদান pivot-র সাথে নির্ধারিত সম্পর্ক মেনে চলে, ডান পাশে বিপরীত সম্পর্ক মেনে চলে, এবং ফলাফল মূল উপাদানগুলোর একটি permutation।
• রিকার্শন শুদ্ধতা: রিকার্সিভ কলগুলো নিশ্চিতভাবে ছোট রেঞ্জে চলে (টার্মিনেশন) এবং যদি সেগুলো তাদের সাবরেঞ্জ সাজায়, সর্বোপরি পুরো রেঞ্জ সাজানো হবে।

এই বিভাজন যুক্তি পরিচালনাযোগ্য রাখে: পার্টিশন ঠিক করে নিন, তারপর এর উপরে সটিং শুদ্ধতা গঠন করুন।

পার্টিশন শুদ্ধতা: কুইকসোর্টের মূল

কুইকসোর্টের গতি একটি ধূর্ত ছোট রুটিনের ওপর নির্ভর করে: পার্টিশন। যদি পার্টিশন সামান্য ভুল হয়, কুইকসোর্ট ভুল সাজাতে পারে, চিরান্তন রিকার্শনে পড়ে যেতে পারে, বা এজ কেসে ক্র্যাশ দিতে পারে।

পার্টিশনের চুক্তি (কী গ্যারান্টি দিতে হবে)

আমরা ক্লাসিক হোয়ার পার্টিশন স্কিম ব্যবহার করব (দুটি পয়েন্টার ভিতরে দিকে চলে)।

ইনপুট: একটি অ্যারে স্লাইস A[lo..hi] এবং একটি pivot মান (প্রায়শই A[lo])।

আউটপুট: একটি ইনডেক্স p যাতে:

• A[lo..p]-এর প্রতিটি উপাদান হলো <= pivot
• A[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, সেগুলো সোয়াপ করলে ইনভারিয়েন্টগুলো বজায় থাকে এবং অনশ্রেণীকৃত মধ্যম অংশ ছোট হয়ে আসে।

বাউন্ডারি কেসগুলো যা শুদ্ধতাকে কভার করতে হবে

• সবই pivot-র চেয়ে ছোট: i ডান দিকে চলে যাবে; পার্টিশনকে তবুও টার্মিনেট করে এবং যৌক্তিক p রিটার্ন করতে হবে।
• সবই pivot-র চেয়ে বড়: j বাম দিকে চলে যাবে; একই টার্মিনেশন উদ্বেগ আছে।
• অনেকগুলো সমান: যদি তুলনা অসঙ্গত হয় (< বনাম <=), পয়েন্টার আটকে যেতে পারে। হোয়ার স্কিম কনসিস্টেন্ট নিয়মের ওপর নির্ভর করে যাতে অগ্রগতি চালু থাকে।
• ইতিমধ্যেই সাজানো / উল্টোদিকে সাজানো: পারফর্ম্যান্স খারাপ হতে পারে, কিন্তু চুক্তি ভাঙা উচিত নয়।

বিভিন্ন পার্টিশন স্কিম আছে (Lomuto, Hoare, তিন-ভাবে পার্টিশনিং)। মূল কথা হলো একটি স্কিম বাছুন, তার কন্ট্রাক্ট স্পষ্টভাবে বলুন, এবং একই কন্ট্রাক্টের বিরুদ্ধে কোড রিভিউ করুন।

রিকার্শন নিয়ে যুক্তি: বেস কেস ও টার্মিনেশন

রিকার্শন সবচেয়ে সহজে বিশ্বাসযোগ্য হয় যখন আপনি দুইটি প্রশ্নের স্পষ্ট উত্তর দিতে পারেন: কখন বন্ধ হয়? এবং প্রতিটি ধাপ কেন বৈধ? হোয়ার-স্টাইল চিন্তা সাহায্য করে কারণ এটি আপনাকে বলতেই বাধ্য করে যে কোন শর্ত একটি কলের আগে সত্য এবং কল ফিরে এলে কী সত্য থাকবে।

বেস কেস সঠিক হতে হবে

একটি রিকারসিভ ফাংশনের অন্তত একটি বেস কেস থাকা উচিত যেখানে আর কোনো রিকার্সিভ কল হবে না এবং তবুও প্রতিশ্রুত ফলাফল বজায় থাকবে।

স্যর্টিং-এ একটি প্রচলিত বেস কেস হল “লম্বাই 0 বা 1”—এগুলো ইতিমধ্যেই সাজানো। এখানে “সাজানো” পরিষ্কারভাবে বলা উচিত: ≤ অর্ডারিং সম্পর্কের জন্য আউটপুট অ্যারেটি সাজানো যদি প্রতিটি i < j-এর জন্য a[i] ≤ a[j] হয়। (ইকুয়াল উপাদানের অরিজিনাল অর্ডার রাখার বিষয়টি আলাদা প্রপার্টি, stability; কুইকসোর্ট সাধারণত স্টেবল নয় যদি আপনি এটিকে স্টেবল করতে না ডিজাইন করেন)।

সাবপ্রবলেমটি অবশ্যই ছোট হতে হবে

প্রতিটি রিকার্সিভ ধাপে ফাংশনকে কঠোরভাবে ছোট ইনপুটে কল করা উচিত। এই “ছোট হওয়া” আপনার টার্মিনেশন যুক্তি: সাইজ কমে এবং 0-এর নিচে নামতে পারে না, তাই আপনি অনন্ত রিকার্সনে পড়তে পারবেন না।

ছোট হওয়া স্ট্যাক সেফটির জন্যও গুরুত্বপূর্ণ। সঠিক কোডও স্ট্যাক গভীরতা অত্যধিক হলে ক্র্যাশ করতে পারে। কুইকসোর্টে অসমভাবে বিভাজন করলে গভীর রিকার্সন হতে পারে—এটি টার্মিনেশন প্রমাণের পাশাপাশি বাস্তব একস্মৃতি সতর্কতা।

শুদ্ধতা প্রথমে, পারফর্ম্যান্স পরে

কুইকসোর্টের ওয়ার্সট-কেস সময় জটিলতা O(n²) তে নেমে আসতে পারে যখন পার্টিশন খুবই অসমান হয়, কিন্তু সেটা পারফরম্যান্সের বিষয়—শুদ্ধতার ব্যর্থতা নয়। যুক্তির লক্ষ্য হলো: ধরে নিন পার্টিশন উপাদান রক্ষা করে এবং pivot অনুসারে ভাগ করে, সাবরেঞ্জগুলো সঠিকভাবে সাজালে পুরো রেঞ্জটি সিম্পল ডেফিনিশন অনুযায়ী সাজানো হবে।

প্রমাণ-স্টাইল চিন্তা ও টেস্টিং: কিভাবে তারা মিলে কাজ করে

টেস্টিং ও প্রমাণ-স্টাইল যুক্তি একই লক্ষ্য—আত্মবিশ্বাস—প্রাপ্তির বিভিন্ন পথ।

টেস্টিং বাগ পায়; যুক্তি বাগের শ্রেণী বাতিল করে

টেস্টগুলো কংক্রিট ভুল ধরতে দুর্দান্ত: একটি অফ-বাই-ওয়ান, একটি মিসিং এজ কেস, একটি রিগ্রেশন। কিন্তু একটি টেস্ট সুইট ইনপুট স্পেসের মাত্র নমুনা নিতে পারে। এমনকি “100% কভারেজ”ও মানে সেই নয় যে “সব আচরণ পরীক্ষা করা হয়েছে”; বেশিরভাগ সময় মানে “সব লাইন চালানো হয়েছে।”

প্রমাণ-স্টাইল যুক্তি (বিশেষত হোয়ার-স্টাইল) একটি স্পেসিফিকেশন থেকে শুরু করে প্রশ্ন করে: যদি এই প্রিকন্ডিশনগুলো সত্য থাকে, তাহলে কোড কি সর্বদা পোস্টকন্ডিশান প্রতিষ্ঠা করবে? যখন আপনি এটি ভালভাবে করেন, আপনি কেবল একটি বাগ খুঁজে পান না—প্রায়শই পুরো একটি বাগ শ্রেণীকে (যেমন “অ্যারে অ্যাক্সেস রেঞ্জের বাইরে যায়” বা “লুপ পার্টিশন প্রপার্টি ভাঙে”) দূর করতে পারেন।

স্পেসিফিকেশন আরও ভাল টেস্ট কেস তৈরি করে

একটি পরিষ্কার স্পেক একটি টেস্ট জেনারেটর।

যদি আপনার পোস্টকন্ডিশন বলে “আউটপুট সাজানো এবং ইনপুটের permutation,” আপনি স্বয়ংক্রিয়ভাবে টেস্ট আইডিয়া পেয়ে যাবেন:

• বাউন্ডারি: খালি তালিকা, এক উপাদান, ইতিমধ্যেই সাজানো, উল্টোদিকে সাজানো।
• ইনভারিয়েন্ট: মধ্যবর্তী বৈশিষ্ট্য (যেমন পার্টিশন ইনভারিয়েন্ট ধরে আছে কিনা)।
• অবৈধ ইনপুট: null, NaN, সীমাবদ্ধতার বাইরের ইনডেক্স, অসঙ্গত তুলনাকারী।

স্পেক আপনাকে বলে “সঠিক” কী, এবং টেস্টগুলো তা বাস্তবে মেলে কি না তা চেক করে।

প্রপার্টি-ভিত্তিক টেস্টিং বাস্তব সেতু

প্রপার্টি-ভিত্তিক টেস্টিং প্রুফ এবং উদাহরণগত টেস্টিং-এর মধ্যে মাঝপথে আছে। হাত দিয়ে কয়েকটি কেস বাছাই করার বদলে, আপনি প্রপার্টি বর্ণনা করেন এবং একটি টুল অসংখ্য ইনপুট জেনারেট করে।

সাজানোর জন্য দুটি সহজ প্রপার্টি অনেকদূর যায়:

• Sortedness: ফলাফল অ-ঘাটতি ক্রমে আছে।
• Permutation: ফলাফল ইনপুটের সাথে একই উপাদানগুলো একই গণনায় রয়েছে।

এই প্রপার্টিগুলো আসলে executable পোস্টকন্ডিশন।

একটি দল বাস্তবে ব্যবহার করতে পারবে এমন ওয়ার্কফ্লো

একটি হালকা ওজন রুটিন যা স্কেলে করে:

1. প্রথমে স্পেক লিখুন (preconditions, postconditions, মূল ইনভারিয়েন্ট)।
2. জটিল অংশগুলো নিয়ে যুক্তি করুন (লুপ, পার্টিশনিং, রিকার্শন বাউন্ডারি)।
3. স্পেককে টেস্টে রূপান্তর করুন (বাউন্ডারি কেস + প্রপার্টি-ভিত্তিক চেক)।
4. এগুলো একসাথে রাখুন কোড এবং রিভিউতে, যাতে ভবিষ্যৎ পরিবর্তন চুপচাপ মূল উদ্দেশ্য লঙ্ঘন না করে।

আপনি যদি এটিকে প্রতিষ্ঠা করতে চান, “স্পেক + যুক্তি নোট + টেস্ট” কে আপনার PR টেমপ্লেট বা কোড রিভিউ চেকলিস্টে রাখুন (দেখুন /blog/code-review-checklist)।

যদি আপনি একটি ভিব-কোডিং ওয়ার্কফ্লো ব্যবহার করেন (চ্যাট-ভিত্তিক ইন্টারফেস থেকে কোড জেনারেট করা), একই শৃঙ্খলা প্রয়োগযোগ্য—এবং সম্ভবত আরও প্রয়োজনীয়। উদাহরণস্বরূপ Koder.ai-তে আপনি Planning Mode-এ শুরু করে preconditions/postconditions পিন করতে পারেন, তারপর property-based টেস্ট যোগ করার সময় স্ন্যাপশট ও রোলব্যাক ব্যবহার করে ইটারেট করতে পারেন। টুলটি ইমপ্লিমেন্টেশন দ্রুত করে, কিন্তু স্পেকই রাখে “দ্রুত” কে “শীতল” থেকে “ভঙ্গুর” হওয়া থেকে রক্ষা করে।

সেফটি চিন্তা: বাস্তব-জগতের পরিণতি সহ শুদ্ধতা

শুদ্ধতা কেবল “প্রোগ্রাম সঠিক মান রিটার্ন করে” ব্যাপার নয়। সেফটি মাইন্ডসেট একটি ভিন্ন প্রশ্ন করে: কোন ফলাফলগুলি অগ্রহণযোগ্য, এবং কিভাবে আমরা সেগুলো প্রতিরোধ করব—এমনকি কোড চাপলে, ভুলভাবে ব্যবহার করলে বা আংশিকভাবে ব্যর্থ হলেও? বাস্তবে, সেফটি হল শুদ্ধতা একটি অগ্রাধিকারের তালিকা: কিছু ব্যর্থতা অশান্তিকর, আর কিছু আর্থিক ক্ষতি, প্রাইভেসি লঙ্ঘন বা শারীরিক ক্ষতি করতে পারে।

ঝুঁকি বনাম বাগ: কেন প্রভাব গুরুত্বপূর্ণ

বাগ হল কোড বা ডিজাইনের ত্রুটি। হ্যাজার্ড হল এমন একটি পরিস্থিতি যা অগ্রহণযোগ্য ফলাফল ঘটাতে পারে। একটি বাগ এক প্রেক্ষাপটে নিরীহ হতে পারে এবং অন্য প্রেক্ষাপটে বিপজ্জনক।

উদাহরণ: একটি ফটোগ্যালারি-তে অফ-বাই-ওয়ান ত্রুটি একটি ছবিকে ভুলভাবে লেবেল করতে পারে; একই ত্রুটি একটি মেডিসিন ডোজ ক্যালকুলেটরে রোগীকে ক্ষতিগ্রস্ত করতে পারে। সেফটি চিন্তা আপনাকে কোড আচরণকে ফলাফলের সঙ্গে যুক্ত করতে বাধ্য করে—শুধু স্পেক কমপ্লায়েন্স নয়।

সবচেয়ে খারাপ ফলাফল প্রতিরোধের সহজ কৌশল

ধারণা ভারী ফরমাল মেথড লাগবে না যত তাড়াতাড়ি আপনি কিছু রুটিন অভ্যাস মানেন তা সঙ্গে সঙ্গে সেফটি বাড়ায়:

• Fail-safe defaults: সিস্টেম নিশ্চিত হতে না পারলে নিরাপদ আচরণ বেছে নিন। উদাহরণ: অথরাইজেশন চেক ব্যর্থ হলে অনুমতি না দিয়ে দিন, অনুমতি দিয়ে নয়।
• বাউন্ডারিতে ইনপুট ভ্যালিডেশন: ব্যবহারকারী ইনপুট, ফাইল কন্টেন্ট ও নেটওয়ার্ক ডেটাকে অনবিশ্বাসযোগ্য ধরা। টাইপ, রেঞ্জ, ফর্ম্যাট এবং ইনভারিয়েন্টগুলো প্রথমেই যাচাই করুন।
• লিমিট ও টাইমআউট: মেমরি ব্যবহার, অনুরোধের আকার, রিকার্শন গভীরতা, রিট্রাই ও এক্সিকিউশনের সময় সীমা দেয়া। অনেক ঘটনার কারণ হচ্ছে “সঠিক” কোড অযৌক্তিক ইনপুটে চালানো।

এই কৌশলগুলো হোয়ার-স্টাইল যুক্তির সাথে ভালোভাবে জোড়া যায়: আপনি প্রিকন্ডিশন স্পষ্ট করেন (কোন ইনপুট গ্রহণযোগ্য) এবং পোস্টকন্ডিশনে সেফটি প্রপার্টি রাখেন (কী কখনও ঘটবে না)।

ট্রেড-অফ: চেক বিনামূল্যে আসে না

সেফটি-উপযোগী চেকগুলোর কিছু খরচ থাকে—CPU, জটিলতা, বা মাঝে মাঝে ভুল প্রত্যাখ্যান।

• পারফরম্যান্স বনাম চেক: দ্রুত পথ কদরযোগ্য, কিন্তু গুরুত্বপূর্ণ সীমায় ভ্যালিডেশন, রেট লিমিট এবং টাইমআউট থাকা উচিত।
• কঠোরতা বনাম ব্যবহারযোগ্যতা: সব অসম্পূর্ণ ইনপুট প্রত্যাখ্যান করলে ব্যবহারকারী বিরক্ত হতে পারে; সব কিছু গ্রহণ করলে বিভ্রান্তি ও শোষণ বাড়ে। ব্যবহারিক সমাধান: “কোরে কঠোর, প্রান্তে নম্র” এবং লজিং ও মাপজোক রাখুন কতবার এজ-কেস আসে।

সেফটি চিন্তা সৌন্দর্যের প্রমাণ দেখানো নয়—এটি সেই ব্যর্থ মোডগুলো প্রতিরোধ করবে যেগুলো আপনি সহ্য করতে পারেন না।

হোয়ার-স্টাইল যুক্তি কোড রিভিউতে প্রয়োগ করা

কোড রিভিউই হলো যেখানে শুদ্ধতা চিন্তা দ্রুত ফল দেয়, কারণ আপনি বিজ্ঞদের চেয়ে বহু আগে অনুপস্থিত অনুমানগুলি ধরতে পারেন। হোয়ার-র মূল কৌশল—"এখানে কী সত্য হতে হবে" এবং "এখানে কী সত্য থাকবে"—রিভিউ প্রশ্নে সহজে অনুবাদ করা যায়।

হোয়ার ধারণাগুলোকে রিভিউ প্রশ্নে রূপান্তর করুন

একটি চেঞ্জ পড়ার সময় প্রতিটি গুরুত্বপূর্ণ ফাংশনকে একটি ছোট প্রতিশ্রুতি হিসেবে ফ্রেম করুন:

• Assumptions (preconditions): ইনপুট, স্টেট এবং পরিবেশ সম্পর্কে কী সত্য হতে হবে? (উদাহরণ: “তালিকা শূন্য নয়”, “ইউজার অথেনটিকেটেড”, “লক ধরা আছে”)।
• Guarantees (postconditions): পরে কী সত্য—রিটার্ন মান ও সাইড-ইফেক্টসহ? (উদাহরণ: “ব্যালান্স amount দ্বারা কমেছে”, “রেকর্ড ঠিক একবার ঢোকানো হয়েছে”)।
• Invariants: লুপ, রিট্রাই বা বহু-পদক্ষেপ ওয়ার্কফ্লোর সময় কী বজায় থাকতে হবে? (উদাহরণ: “processed_count ≤ total”, “এখন পর্যন্ত ডেবিটের যোগফল ক্রেডিটের যোগফলের সমান”)।
• Failure behavior: ত্রুটি হলে কী হয়—সিস্টেম কি নিরাপদ অবস্থায় আছে? আংশিক আপডেট রোলব্যাক করা হয়েছে কি?

একটি সহজ রিভিউ অভ্যাস: আপনি যদি এক বাক্যে প্রি/পোস্ট কন্ডিশন বলতে না পান, কোডটি সম্ভবত স্পষ্ট কাঠামো প্রয়োজন।

গুরুত্বপূর্ণ ফাংশনের জন্য “কন্ট্রাক্ট কমেন্ট”

ঝুঁকিপূর্ণ বা কেন্দ্রীয় ফাংশনের উপরে একটি ছোট কন্ট্রাক্ট কমেন্ট যোগ করুন। এটি কনক্রিট রাখুন: ইনপুট, আউটপুট, সাইড-ইফেক্ট এবং ত্রুটি।

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.
    """
    ...

এই মন্তব্যগুলো ফর্মাল প্রমাণ নয়, কিন্তু রিভিউয়ারের কাছে কী চেক করতে হবে তা পরিষ্কার করে।

ঝুঁকিপূর্ণ কোডের জন্য হালকা চেকলিস্ট

নিরাপত্তা বা ঝুঁকিপূর্ণ কোড রিভিউ করার সময় বেশি স্পষ্ট হন—বিশেষত যখন কোড হ্যান্ডেল করে:

• পার্সিং/ভ্যালিডেশন (ম্যালফর্মড ইনপুট পাথ, বাউন্ডারি কেস)
• কনক্যারেন্সি (লক, রেস, idempotency, রিট্রাই)
• টাকা/কোটা (রাউন্ডিং, ডবল-চার্জিং, ওভারফ্লো)
• পারমিশন (কারা কি করতে পারে, এবং কেন)

যদি চেঞ্জ এগুলোকে স্পর্শ করে, জিজ্ঞেস করুন: “প্রিকন্ডিশন কোথায়, এবং সেগুলো কোথায় প্রয়োগ হচ্ছে?” এবং “ত্রুটি হলে আমরা কি গ্যারান্টি দিই যে সিস্টেম নিরাপদ থাকবে?”

কখন ফর্মাল টুল ব্যবহার করবেন—এবং একটি ব্যবহারিক চেকলিস্ট

ফর্মাল যুক্তি মানে আপনার পুরো কোডবেসকে একটি গাণিতিক পেপারে পরিণত করা নয়। লক্ষ্য হলো সেই জায়গাগুলোতে অতিরিক্ত নিশ্চয়তা ব্যয় করা যেখানে লাভ বেশি: জায়গাগুলো যেখানে “টেস্টে ঠিক আছে” যথেষ্ট নয়।

ফর্মাল মেথডগুলো সবচেয়ে বেশি সাহায্য করে কোথায়

সেগুলো ভালো কাজ করে যখন আপনার একটি ছোট, ক্রিটিক্যাল মডিউল থাকে যাকে সবকিছু নির্ভর করে (অথেনটিকেশন, পেমেন্ট রুল, পারমিশন, সেফটি ইন্টারলক), বা একটি জটিল অ্যালগরিদম যেখানে অফ-বাই-ওয়ান ভুল দীর্ঘ সময় লুকিয়ে থাকে (পার্সার, শিডিউলার, ক্যাশিং/এভিকশন, কনকারেন্সি প্রিমিটিভ, পার্টিশন-শৈলীর কোড)।

একটি দরকারী নিয়ম: যদি একটি বাগ বাস্তব ক্ষতি, বড় আর্থিক ক্ষতি, বা চুপচাপ ডেটা করাপশন ঘটাতে পারে, আপনি সাধারণ রিভিউ + টেস্টের বাইরে আরও চান।

বিবেচনা করার টুলসমূহ (উচ্চস্তরে)

আপনি "হালকা" থেকে "ভারী" পর্যন্ত বেছে নিতে পারেন, এবং প্রায়ই ভাল ফলাফল আসে যখন আপনি এগুলো একত্রে ব্যবহার করেন:

• টাইপস (মজবুত টাইপ সিস্টেম, non-null, units/quantities): অবৈধ স্টেটের পুরো শ্রেণি প্রতিরোধ করে।
• স্টাটিক অ্যানালাইসিস: সন্দেহজনক পথ, API ব্যবহার ভুল, ডেটা রেস, টেইন্টেড ইনপুট ফ্লো খুঁজে পায়।
• কন্ট্রাক্টস (preconditions/postconditions, assertions): আপনার হোয়ার-স্টাইল বিবৃতিগুলোর executable সংস্করণ।
• মডেল চেকিং: স্টেট মেশিনগুলো অন্বেষণ করে (প্রোটোকল, কনকারেন্সি, “what if” সিকুয়েন্সের জন্য চমৎকার)।
• ফর্মাল ভেরিফিকেশন: সর্বোচ্চ নিশ্চয়তার অংশগুলোর জন্য মেশিন-চেকড প্রমাণ।

কতটা গভীর হওয়া উচিত?

ফর্মালিটির গভীরতা নির্ধারণ করুন:

• ঝুঁকি: প্রভাব × সম্ভাবনা। উচ্চ ঝুঁকি শক্ত গ্যারান্টি ন্যায্য করে।
• খরচ: স্পেসিফাই, প্রুফ ও রক্ষণাবেক্ষণের সময়।
• চেঞ্জ রেট: দ্রুত পরিবর্তিত কোডকে ফর্মালি ধরে রাখা কঠিন; প্রথমে ইন্টারফেস স্থিতিশীল করুন।
• টিম দক্ষতা: যদি প্রমাণ প্রয়োগ ধীর করে দেয়, তবে শুরু করুন কন্ট্রাক্ট ও স্ট্যাটিক অ্যানালাইসিস দিয়ে।

অবশ্যই, আপনি ধাপে ধাপে "ফর্মালিটি" বাড়াতে পারেন: প্রথমে স্পষ্ট কন্ট্রাক্ট ও ইনভারিয়েন্ট, তারপর অটোমেশন দিয়ে সেগুলো বজায় রাখুন। Koder.ai-র মতো টিমে দ্রুত UI, ব্যাকএন্ড ও স্কিমা জেনারেশন হলেও আপনি স্ন্যাপশট/রোলব্যাক ও CI-তে কন্ট্রাক্টের টেস্ট রেখে দ্রুততার সঙ্গে নিশ্চয়তা বজায় রাখতে পারেন।

একটি ব্যবহারিক চেকলিস্ট

পরিকল্পনা বা কোড রিভিউতে “আর কি ফর্মাল করা উচিত?” গেট হিসেবে ব্যবহার করুন:

1. সবচেয়ে খারাপ বিশ্বাসযোগ্য ফলাফল কী, এবং কারা ক্ষতিগ্রস্ত হবে (ইউজার, অপস, রেগুলেটর)?
2. টেস্ট দিয়ে কি গুরুত্বপূর্ণ এজ-কেস এবং স্টেটগুলো কভার করা সম্ভব?
3. লজিক কি স্টেটফুল, কনকারেন্ট, না কি ইনভারিয়েন্ট/বাউন্ডারি-ভারী?
4. পাবলিক এন্ট্রি পয়েন্টগুলোর জন্য আমরা কি স্পষ্ট preconditions/postconditions লিখতে পারি?
5. কি একটি ছোট কোর আছে যাকে আমরা আলাদা করে আরও গভীরে ভেরিফাই করতে পারি?
6. কোন টুল সবচেয়ে ভালো রিটার্ন দেবে: শক্ত টাইপস, স্ট্যাটিক অ্যানালাইসিস, কন্ট্রাক্ট, মডেল চেকিং, না কি প্রমাণ?
7. পরবর্তী ত্রৈমাসিকে কী পরিবর্তন হবে, এবং কিভাবে আমরা গ্যারান্টিগুলো বজায় রাখব?

আরও পড়ার জন্য: design-by-contract, property-based testing, স্টেট মেশিনে model checking, আপনার ভাষার জন্য স্ট্যাটিক অ্যানালাইজার, এবং প্রুফ অ্যাসিস্ট্যান্ট ও ফরমাল স্পেসিফিকেশনের প্রারম্ভিক বিষয়বস্তু।