Formal specification
কম্পিউটার বিজ্ঞানে, আনুষ্ঠানিক নির্দিষ্টকরণ হল গাণিতিক ভিত্তিক কৌশল যার উদ্দেশ্য হল সিস্টেম এবং সফ্টওয়্যার বাস্তবায়নে সহায়তা করা। এগুলি একটি পদ্ধতি বর্ণনা করতে, তার আচরণ বিশ্লেষণ করতে এবং কঠোর এবং কার্যকর যুক্তি সরঞ্জামের মাধ্যমে আগ্রহের মূল বৈশিষ্ট্যগুলি যাচাই করে তার নকশায় সহায়তা করতে ব্যবহৃত হয়। এই নির্দিষ্টকরণগুলি এই অর্থে আনুষ্ঠানিক যে তাদের একটি বাক্য গঠন রয়েছে, তাদের শব্দার্থবিদ্যা একটি ডোমেনের মধ্যে পড়ে এবং এগুলি দরকারী তথ্য অনুমান করতে ব্যবহার করা যেতে পারে। অনুপ্রেরণা প্রতিটি উত্তীর্ণ দশকে কম্পিউটার ব্যবস্থা ক্রমবর্ধমানভাবে আরও শক্তিশালী হয়ে উঠেছে এবং ফলস্বরূপ, তারা সমাজের জন্য আরও প্রভাবশালী হয়ে উঠেছে। এই কারণে, নির্ভরযোগ্য সফ্টওয়্যারের নকশা এবং বাস্তবায়নে সহায়তা করার জন্য আরও ভাল কৌশল প্রয়োজন। প্রতিষ্ঠিত প্রকৌশল শাখাগুলি গাণিতিক বিশ্লেষণকে পণ্য নকশা তৈরি এবং বৈধ করার ভিত্তি হিসাবে ব্যবহার করে। সফ্টওয়্যার ইঞ্জিনিয়ারিংয়ের নির্ভরযোগ্যতার ক্ষেত্রে এটি অর্জনের জন্য আনুষ্ঠানিক নির্দিষ্টকরণগুলি এমন একটি উপায় যা একবার পূর্বাভাস দেওয়া হয়েছিল। পরীক্ষার মতো অন্যান্য পদ্ধতিগুলি সাধারণত কোডের গুণমান বাড়ানোর জন্য ব্যবহার করা হয়। ব্যবহার এই ধরনের নির্দিষ্টকরণের পরিপ্রেক্ষিতে, একটি সিস্টেমের নকশা তার নির্দিষ্টকরণের ক্ষেত্রে সঠিক কিনা তা প্রদর্শনের জন্য আনুষ্ঠানিক যাচাইকরণ কৌশল ব্যবহার করা সম্ভব। এটি প্রকৃত বাস্তবায়নে কোনও বড় বিনিয়োগ করার আগে ভুল সিস্টেম ডিজাইনগুলি সংশোধন করার অনুমতি দেয়। আরেকটি পদ্ধতি হল একটি নির্দিষ্টকরণকে একটি নকশায় রূপান্তরিত করার জন্য সম্ভবত সঠিক পরিশোধন পদক্ষেপগুলি ব্যবহার করা, যা শেষ পর্যন্ত একটি বাস্তবায়নে রূপান্তরিত হয় যা নির্মাণের মাধ্যমে সঠিক। এটি লক্ষ করা গুরুত্বপূর্ণ যে একটি আনুষ্ঠানিক নির্দিষ্টকরণ একটি বাস্তবায়ন নয়, বরং এটি একটি বাস্তবায়ন বিকাশের জন্য ব্যবহার করা যেতে পারে। আনুষ্ঠানিক নির্দিষ্টকরণগুলি বর্ণনা করে যে একটি সিস্টেমের কী করা উচিত, সিস্টেমের কীভাবে এটি করা উচিত তা নয়। একটি ভাল নির্দিষ্টকরণের অবশ্যই নিম্নলিখিত বৈশিষ্ট্যগুলির মধ্যে কয়েকটি থাকতে হবেঃ পর্যাপ্ত, অভ্যন্তরীণভাবে সামঞ্জস্যপূর্ণ, দ্ব্যর্থহীন, সম্পূর্ণ, সন্তুষ্ট, ন্যূনতম একটি ভাল নির্দিষ্টকরণ থাকবেঃ গঠনযোগ্যতা, পরিচালনাযোগ্যতা এবং বিবর্তনযোগ্যতা ব্যবহারযোগ্যতা শক্তিশালী এবং দক্ষ বিশ্লেষণ আনুষ্ঠানিক নির্দিষ্টকরণে আগ্রহের অন্যতম প্রধান কারণ হল যে তারা সফ্টওয়্যার বাস্তবায়নের উপর প্রমাণ সম্পাদন করার ক্ষমতা প্রদান করবে। এই প্রমাণগুলি কোনও নির্দিষ্টকরণের বৈধতা যাচাই করতে, নকশার সঠিকতা যাচাই করতে বা কোনও প্রোগ্রাম কোনও নির্দিষ্টকরণকে সন্তুষ্ট করে তা প্রমাণ করতে ব্যবহার করা যেতে পারে। সীমাবদ্ধতা একটি নকশা (বা বাস্তবায়ন) কখনই নিজে থেকে "সঠিক" ঘোষণা করা যায় না। এটি কেবলমাত্র "প্রদত্ত নির্দিষ্টকরণের ক্ষেত্রে সঠিক" হতে পারে। আনুষ্ঠানিক নির্দিষ্টকরণ সঠিকভাবে সমাধান করার সমস্যাটি বর্ণনা করে কিনা তা একটি পৃথক বিষয়। এটি সমাধান করাও একটি কঠিন সমস্যা কারণ এটি শেষ পর্যন্ত একটি অনানুষ্ঠানিক কংক্রিট সমস্যা ক্ষেত্রের বিমূর্ত আনুষ্ঠানিক উপস্থাপনা তৈরি করার সমস্যা নিয়ে উদ্বেগ প্রকাশ করে এবং এই ধরনের বিমূর্ত পদক্ষেপ আনুষ্ঠানিক প্রমাণের জন্য উপযুক্ত নয়। যাইহোক, বৈশিষ্ট্য সম্পর্কিত "চ্যালেঞ্জ" উপপাদ্যগুলি প্রমাণ করে একটি নির্দিষ্টকরণকে বৈধ করা সম্ভব যা নির্দিষ্টকরণটি প্রদর্শন করবে বলে আশা করা হচ্ছে। যদি সঠিক হয়, তবে এই উপপাদ্যগুলি নির্দিষ্টকরণ সম্পর্কে নির্দিষ্টকারীর বোধগম্যতা এবং অন্তর্নিহিত সমস্যা ক্ষেত্রের সাথে এর সম্পর্ককে শক্তিশালী করে। যদি তা না হয়, তাহলে নির্দিষ্টকরণটি উৎপাদন (এবং বাস্তবায়নের) সঙ্গে জড়িত ব্যক্তিদের ডোমেন বোঝাপড়া আরও ভালভাবে প্রতিফলিত করার জন্য সম্ভবত নির্দিষ্টকরণটি পরিবর্তন করা প্রয়োজন। সফ্টওয়্যার বিকাশের আনুষ্ঠানিক পদ্ধতিগুলি শিল্পে ব্যাপকভাবে ব্যবহৃত হয় না। বেশিরভাগ কোম্পানি তাদের সফ্টওয়্যার উন্নয়ন প্রক্রিয়াগুলিতে এগুলি প্রয়োগ করা সাশ্রয়ী বলে মনে করে না। এটি বিভিন্ন কারণে হতে পারে, যার মধ্যে কয়েকটি হলঃ কম পরিমাপযোগ্য রিটার্ন সহ উচ্চ প্রাথমিক স্টার্ট আপ খরচ নমনীয়তা অনেক সফ্টওয়্যার সংস্থা চটপটে পদ্ধতি ব্যবহার করে যা নমনীয়তার উপর দৃষ্টি নিবদ্ধ করে। সামনে পুরো সিস্টেমের একটি আনুষ্ঠানিক নির্দিষ্টকরণ করা প্রায়শই নমনীয়তার বিপরীত হিসাবে বিবেচিত হয়। যাইহোক, "চটপটে" বিকাশের জটিলতার সাথে আনুষ্ঠানিক নির্দিষ্টকরণ ব্যবহারের সুবিধাগুলি সম্পর্কে কিছু গবেষণা রয়েছে তাদের কার্যকরভাবে বোঝার এবং প্রয়োগ করার জন্য উচ্চ স্তরের গাণিতিক দক্ষতা এবং বিশ্লেষণাত্মক দক্ষতার প্রয়োজন। এর একটি সমাধান হ 'ল সরঞ্জাম এবং মডেলগুলি বিকাশ করা যা এই কৌশলগুলি বাস্তবায়িত করার অনুমতি দেয় তবে অন্তর্নিহিত গণিতের সীমিত সুযোগকে লুকিয়ে রাখে তারা প্রকল্পে সমস্ত স্টেকহোল্ডারদের আগ্রহের বৈশিষ্ট্যগুলি ক্যাপচার করে না তারা ব্যবহারকারী ইন্টারফেস এবং ব্যবহারকারীর মিথস্ক্রিয়া নির্দিষ্ট করার জন্য ভাল কাজ করে না। এটি সম্পূর্ণ সত্য নয়, তাদের ব্যবহারকে কেবলমাত্র সমালোচনামূলক সিস্টেমের মূল অংশে সীমাবদ্ধ করে তারা ব্যয়বহুল বলে দেখিয়েছে। অন্যান্য সীমাবদ্ধতাঃ বিচ্ছিন্নতা নিম্ন-স্তরের অ্যান্টোলজিগুলি উদ্বেগের দুর্বল পৃথকীকরণ প্রতিক্রিয়া সরঞ্জাম প্যারাডাইমগুলি আনুষ্ঠানিক নির্দিষ্টকরণ কৌশলগুলি বিভিন্ন ডোমেনে বিদ্যমান রয়েছে। তারা কী ধরনের সিস্টেম মডেল করার চেষ্টা করছে, কীভাবে সেগুলি প্রয়োগ করা হয় এবং সফ্টওয়্যার জীবনচক্রের কোন পর্যায়ে সেগুলি চালু করা হয়েছে তার উপর নির্ভর করে আনুষ্ঠানিক নির্দিষ্টকরণের বাস্তবায়ন ভিন্ন হবে। এই ধরনের মডেলগুলিকে নিম্নলিখিত নির্দিষ্টকরণের দৃষ্টান্তগুলিতে শ্রেণীবদ্ধ করা যেতে পারেঃ সিস্টেমের ইতিহাসের উপর ভিত্তি করে ইতিহাস-ভিত্তিক নির্দিষ্টকরণের আচরণগুলি সময়ের সাথে সাথে ব্যাখ্যা করা হয় সিস্টেমের পর্যায়ক্রমিক ধাপগুলির ধারাবাহিকতার উপর ভিত্তি করে রাজ্য-ভিত্তিক নির্দিষ্টকরণের আচরণ, (যেমন। একটি আর্থিক লেনদেন) জেড, ভি. ডি. এম বা বি-এর মতো ভাষাগুলি স্টেটচার্ট, প্রোমেলা, এস. টি. ই. পি-এস. পি. এল, আর. এস. এম. এল বা এস. সি. আর-এর মতো প্রতিক্রিয়াশীল সিস্টেম ভাষাগুলির সাথে সর্বোত্তমভাবে ব্যবহৃত সিস্টেমের রাজ্য থেকে রাজ্যে রূপান্তরের উপর ভিত্তি করে এই দৃষ্টান্তের উপর নির্ভর করে কার্যকরী নির্দিষ্টকরণ একটি সিস্টেমকে গাণিতিক ফাংশনের কাঠামো হিসাবে নির্দিষ্ট করে ও. বি. জে, এ. এস. এল, পি. এল. ইউ. এস, এল. এ. আর. সি, এইচ. ও. এল বা পি. ভি. এস এই দৃষ্টান্তের উপর নির্ভর করে কার্যকরী নির্দিষ্টকরণ প্রাথমিক ভাষাগুলি যেমন পাইসলে, জি. আই. এস. টি, পেট্রি নেট বা প্রসেস অ্যালজেব্রা এই দৃষ্টান্তের উপর নির্ভর করে উপরের দৃষ্টান্তগুলি ছাড়াও, নির্দিষ্ট কিছু পদ্ধতি প্রয়োগ করার উপায় রয়েছে। এখানে উল্লিখিত গবেষণাপত্রে একটি নির্দিষ্টকরণের নকশা তৈরি করার সময় ব্যবহার করার জন্য হিউরিস্টিক্স নিয়ে সর্বোত্তম আলোচনা করা হয়েছে। তারা বিভাজন ও জয় পদ্ধতির প্রয়োগের মাধ্যমে তা করে। সফ্টওয়্যার সরঞ্জাম জেড নোটেশন একটি নেতৃস্থানীয় আনুষ্ঠানিক নির্দিষ্টকরণ ভাষার একটি উদাহরণ। অন্যান্যগুলির মধ্যে রয়েছে ভিয়েনা উন্নয়ন পদ্ধতির নির্দিষ্টকরণ ভাষা (ভিডিএম-এসএল) এবং বি-পদ্ধতির বিমূর্ত মেশিন নোটেশন (এএমএন)। ওয়েব পরিষেবার ক্ষেত্রে, আনুষ্ঠানিক নির্দিষ্টকরণ প্রায়শই অ-কার্যকরী বৈশিষ্ট্য (ওয়েব পরিষেবার পরিষেবার গুণমান) বর্ণনা করতে ব্যবহৃত হয়। কিছু সরঞ্জাম হলঃ বীজগাণিতিক লার্চ ওবিজে লোটোস মডেল-ভিত্তিক জেড বি ভিডিএম সিএসপি পেট্রি নেটস টিএলএ + আরও দেখুন বীজগাণিতিক নির্দিষ্টকরণ আনুষ্ঠানিক পদ্ধতি মডেল-ভিত্তিক নির্দিষ্টকরণ সফ্টওয়্যার ইঞ্জিনিয়ারিং নির্দিষ্টকরণ ভাষা নির্দিষ্টকরণ (প্রযুক্তিগত মান) রেফারেন্স বাহ্যিক লিঙ্ক কোরিয়থ দ্বারা আনুষ্ঠানিক নির্দিষ্টকরণের (প্রযুক্তি) জন্য একটি কেস