एक औपचारिक तकनीक एक हार्डवेयर और/या सॉफ्टवेयर सिस्टम को निर्दिष्ट करने के लिए एक गणितीय विधि है, सत्यापित करें कि क्या एक विनिर्देश प्राप्त करने योग्य है, सत्यापित करें कि एक कार्यान्वयन इसके विनिर्देश को पूरा करता है, सिस्टम को चलाने के बिना सिस्टम के गुणों को साबित करता है, आदि। एक का गणितीय आधार औपचारिक विधि इसकी विशिष्ट भाषा द्वारा प्रदान की जाती है। अधिक सटीक रूप से, एक औपचारिक विनिर्देश भाषा में दो सेट होते हैं - सिन और सेम, और उनके बीच एक संबंध होता है। सेट सिंक को सिंटैक्टिक डोमेन कहा जाता है, सेट सेम को सिमेंटिक डोमेन कहा जाता है, और रिलेशन सैट को संतुष्टि रिलेशन कहा जाता है।
Syntactic domains:
औपचारिक विनिर्देश भाषा के वाक्य-विन्यास क्षेत्र में प्रतीकों की एक वर्णमाला और वर्णमाला से अच्छी तरह से गठित सूत्रों का निर्माण करने के लिए गठन नियमों का एक सेट होता है। एक प्रणाली को निर्दिष्ट करने के लिए अच्छी तरह से गठित सूत्रों का उपयोग किया जाता है।
Semantic domains:
औपचारिक तकनीकों में काफी भिन्न अर्थपूर्ण डोमेन हो सकते हैं। सार डेटा प्रकार विनिर्देश भाषाओं का उपयोग बीजगणित, सिद्धांतों और कार्यक्रमों को निर्दिष्ट करने के लिए किया जाता है। प्रोग्रामिंग भाषाओं का उपयोग इनपुट से आउटपुट मानों तक के कार्यों को निर्दिष्ट करने के लिए किया जाता है।
