ในวิทยาการคอมพิวเตอร์ข้อกำหนดอย่างเป็นทางการคือเทคนิคทางคณิตศาสตร์ที่มีจุดประสงค์เพื่อช่วยในการใช้งานระบบและซอฟต์แวร์ โดยใช้เพื่ออธิบายระบบ วิเคราะห์พฤติกรรม และช่วยในการออกแบบโดยการตรวจสอบคุณสมบัติหลักที่น่าสนใจผ่านเครื่องมือการให้เหตุผลที่เข้มงวดและมีประสิทธิภาพ^{[ 1 ] [ 2 ]}ข้อกำหนดเหล่านี้เป็นแบบทางการในแง่ที่ว่ามีไวยากรณ์ ความหมายอยู่ในโดเมนเดียว และสามารถใช้เพื่ออนุมานข้อมูลที่เป็นประโยชน์ได้^{[ 3 ]}

ในแต่ละทศวรรษที่ผ่านมา ระบบคอมพิวเตอร์มีประสิทธิภาพมากขึ้นเรื่อยๆ และส่งผลให้มีผลกระทบต่อสังคมมากขึ้นเช่นกัน ด้วยเหตุนี้ จึงจำเป็นต้องมีเทคนิคที่ดีกว่าเพื่อช่วยในการออกแบบและใช้งานซอฟต์แวร์ที่เชื่อถือได้ สาขาวิชาวิศวกรรมที่ได้รับการยอมรับใช้การวิเคราะห์ทางคณิตศาสตร์เป็นพื้นฐานในการสร้างและตรวจสอบความถูกต้องของการออกแบบผลิตภัณฑ์ ข้อกำหนดอย่างเป็นทางการเป็นวิธีหนึ่งในการบรรลุความน่าเชื่อถือในวิศวกรรมซอฟต์แวร์ดังที่เคยคาดการณ์ไว้ วิธีการอื่นๆ เช่น การทดสอบมักใช้เพื่อเพิ่มคุณภาพของโค้ด^{[ 1 ]}

เมื่อมีข้อกำหนด ดังกล่าวแล้ว ก็สามารถใช้ เทคนิค การตรวจสอบอย่างเป็นทางการเพื่อแสดงให้เห็นว่าการออกแบบระบบนั้นถูกต้องตามข้อกำหนด วิธีนี้ช่วยให้สามารถแก้ไขการออกแบบระบบที่ไม่ถูกต้องได้ก่อนที่จะมีการลงทุนครั้งใหญ่ในการนำไปใช้งานจริง อีกแนวทางหนึ่งคือการใช้ ขั้นตอน การปรับปรุง ที่พิสูจน์ได้ว่าถูกต้อง เพื่อเปลี่ยนข้อกำหนดให้เป็นการออกแบบ ซึ่งในที่สุดจะถูกเปลี่ยนเป็นการนำไปใช้งานที่ถูก ต้องตั้งแต่เริ่มต้น

ข้อกำหนดอย่างเป็นทางการไม่ใช่การนำไปใช้งาน จริง แต่สามารถนำไปใช้เพื่อพัฒนาการนำไปใช้งานจริงได้ ข้อกำหนดอย่างเป็นทางการอธิบายว่าระบบควรทำอะไร ไม่ใช่ว่า ระบบควรทำ อย่างไร

ข้อกำหนดที่ดีต้องมีคุณสมบัติดังต่อไปนี้: เพียงพอ สอดคล้องกันภายใน ไม่คลุมเครือ ครบถ้วน ตรงตามความต้องการ น้อยที่สุด^{[ 3 ]}

ข้อกำหนดที่ดีควรมี: ^{[ 3 ]}

• ความสามารถในการก่อสร้าง ความสามารถในการจัดการ และความสามารถในการพัฒนาต่อยอด
• ความสามารถในการใช้งาน
• ความสามารถในการสื่อสาร
• การวิเคราะห์ที่มีประสิทธิภาพและทรงพลัง

เหตุผลหลักประการหนึ่งที่ทำให้เกิดความสนใจในข้อกำหนดอย่างเป็นทางการก็คือ ข้อกำหนดเหล่านั้นจะช่วยให้สามารถพิสูจน์การใช้งานซอฟต์แวร์ได้^{[ 2 ]}การพิสูจน์เหล่านี้อาจใช้เพื่อตรวจสอบความถูกต้องของข้อกำหนด ตรวจสอบความถูกต้องของการออกแบบ หรือเพื่อพิสูจน์ว่าโปรแกรมตรงตามข้อกำหนด^{[ 2 ]}

การออกแบบ (หรือการนำไปใช้) ไม่สามารถประกาศว่า “ถูกต้อง” ได้ด้วยตัวเอง มันจะถูกต้องได้ก็ต่อเมื่อ “สอดคล้องกับข้อกำหนดที่กำหนดไว้” เท่านั้น ว่าข้อกำหนดอย่างเป็นทางการนั้นอธิบายปัญหาที่จะแก้ไขได้อย่างถูกต้องหรือไม่ เป็นอีกประเด็นหนึ่ง และเป็นประเด็นที่ยากต่อการแก้ไขเช่นกัน เนื่องจากท้ายที่สุดแล้วมันเกี่ยวข้องกับปัญหาการสร้างแบบจำลองที่เป็นทางการที่เป็นนามธรรมของโดเมนปัญหา ที่เป็นรูปธรรมอย่างไม่เป็นทางการ และขั้นตอนการสร้างนามธรรมดังกล่าวไม่สามารถพิสูจน์ได้ด้วยหลักฐานอย่างเป็นทางการ อย่างไรก็ตาม เป็นไปได้ที่จะตรวจสอบ ความถูกต้องของข้อกำหนดโดยการพิสูจน์ ทฤษฎีบท “ท้าทาย” เกี่ยวกับคุณสมบัติที่คาดว่าข้อกำหนดจะแสดงออกมา หากถูกต้อง ทฤษฎีบทเหล่านี้จะเสริมความเข้าใจของผู้กำหนดข้อกำหนดเกี่ยวกับข้อกำหนดและความสัมพันธ์กับโดเมนปัญหาพื้นฐาน หากไม่ถูกต้อง ข้อกำหนดอาจจำเป็นต้องเปลี่ยนแปลงเพื่อให้สะท้อนถึงความเข้าใจในโดเมนของผู้ที่เกี่ยวข้องกับการสร้าง (และการนำไปใช้) ข้อกำหนดได้ดียิ่งขึ้น

วิธีการพัฒนาซอฟต์แวร์ที่เป็นทางการไม่ได้ถูกนำมาใช้กันอย่างแพร่หลายในอุตสาหกรรม บริษัทส่วนใหญ่ไม่คิดว่าการนำวิธีการเหล่านี้มาใช้ในกระบวนการพัฒนาซอฟต์แวร์ของตนนั้นคุ้มค่า^{[ 4 ]}ซึ่งอาจเป็นเพราะเหตุผลหลายประการ ซึ่งบางส่วนได้แก่:

• เวลา
  • ต้นทุนเริ่มต้นสูง แต่ผลตอบแทนที่วัดได้ต่ำ
• ความยืดหยุ่น
  • บริษัทซอฟต์แวร์จำนวนมากใช้ระเบียบวิธีแบบ Agileซึ่งเน้นความยืดหยุ่น การกำหนดรายละเอียดของระบบทั้งหมดอย่างเป็นทางการตั้งแต่เริ่มต้นมักถูกมองว่าเป็นสิ่งที่ตรงกันข้ามกับความยืดหยุ่น อย่างไรก็ตาม มีงานวิจัยบางชิ้นที่แสดงให้เห็นถึงประโยชน์ของการใช้ข้อกำหนดอย่างเป็นทางการกับการพัฒนาแบบ "Agile" ^{[ 5 ]}
• ความซับซ้อน
  • พวกเขาต้องการความเชี่ยวชาญทางคณิตศาสตร์ระดับสูงและทักษะการวิเคราะห์เพื่อทำความเข้าใจและนำไปใช้อย่างมีประสิทธิภาพ^{[ 5 ]}
  • วิธีแก้ปัญหานี้คือการพัฒนาเครื่องมือและแบบจำลองที่ช่วยให้สามารถนำเทคนิคเหล่านี้ไปใช้ได้ แต่ซ่อนคณิตศาสตร์พื้นฐานไว้^{[ 2 ] [ 5 ]}
• ขอบเขตจำกัด^{[ 3 ]}
  • พวกเขาไม่ได้บันทึกคุณสมบัติที่น่าสนใจสำหรับผู้มีส่วนได้ส่วนเสีย ทั้งหมด ในโครงการ^{[ 3 ]}
  • พวกเขาไม่ได้ระบุอินเทอร์เฟซผู้ใช้และการโต้ตอบกับผู้ใช้ได้ดี^{[ 4 ]}
• ไม่คุ้มค่า
  • เรื่องนี้ไม่เป็นความจริงทั้งหมด เพราะการจำกัดการใช้งานไว้เฉพาะส่วนหลักของระบบที่สำคัญเท่านั้น ทำให้พบว่ามีประสิทธิภาพคุ้มค่า^{[ 4 ]}

ข้อจำกัดอื่นๆ: ^{[ 3 ]}

• การแยกตัว
• ออนโทโลยีระดับต่ำ
• คำแนะนำที่ไม่ดี
• การแยกประเด็นที่ไม่ดี
• ฟีดแบ็กเครื่องมือที่ไม่ดี

เทคนิคการกำหนดคุณสมบัติอย่างเป็นทางการมีอยู่ในโดเมนต่างๆ และในระดับต่างๆ มานานแล้ว^{[ 6 ]} การนำข้อกำหนดอย่างเป็นทางการไปใช้จะแตกต่างกันไป ขึ้นอยู่กับประเภทของระบบที่พยายามสร้างแบบจำลอง วิธีการนำไปใช้ และช่วงเวลาใดในวงจรชีวิตของซอฟต์แวร์ที่นำมาใช้^{[ 2 ]}โมเดลประเภทนี้สามารถจัดอยู่ในกรอบแนวคิดการกำหนดคุณสมบัติดังต่อไปนี้:

• ข้อกำหนดตามประวัติ^{[ 3 ]}
  • พฤติกรรมที่อิงตามประวัติของระบบ
  • ข้อกล่าวอ้างต่างๆ จะถูกตีความไปตามกาลเวลา
• ข้อกำหนดตามสถานะ^{[ 3 ]}
  • พฤติกรรมที่ขึ้นอยู่กับสถานะของระบบ
  • ชุดของขั้นตอนต่อเนื่อง (เช่น ธุรกรรมทางการเงิน)
  • ภาษาต่างๆ เช่นZ , VDMหรือBอาศัยแบบแผนนี้^{[ 3 ]}
• ข้อกำหนดตามการเปลี่ยนผ่าน^{[ 3 ]}
  • พฤติกรรมที่ขึ้นอยู่กับการเปลี่ยนสถานะจากสถานะหนึ่งไปอีกสถานะหนึ่งของระบบ
  • ใช้ได้ดีที่สุดกับระบบตอบสนอง
  • ภาษาต่างๆ เช่น Statecharts, PROMELA, STeP-SPL, RSML หรือ SCR อาศัยกระบวนทัศน์นี้^{[ 3 ]}
• ข้อกำหนดเชิงฟังก์ชัน^{[ 3 ]}
  • ระบุระบบเป็นโครงสร้างของฟังก์ชันทางคณิตศาสตร์
  • OBJ, ASL, PLUSS, LARCH, HOL หรือ PVS อาศัยแบบแผนนี้^{[ 3 ]}
• ข้อกำหนดการปฏิบัติงาน^{[ 3 ]}
  • ภาษาในยุคแรก เช่นPaisley , GIST, Petri nets หรือพีชคณิตกระบวนการ อาศัยกระบวนทัศน์นี้^{[ 3 ]}
• ภาษาหลายกระบวนทัศน์
  • FizzBee เป็นภาษากำหนดคุณสมบัติแบบหลายกระบวนทัศน์ที่อนุญาตให้กำหนดคุณสมบัติโดยอิงตามการเปลี่ยนสถานะ/การกระทำ การกำหนดคุณสมบัติเชิงพฤติกรรมด้วยการเปลี่ยนสถานะที่ไม่ใช่แบบอะตอมิก และยังมีโมเดลแอคเตอร์อีกด้วย

นอกเหนือจากแบบแผนข้างต้นแล้ว ยังมีวิธีนำฮิวริสติกบางอย่างมาใช้เพื่อช่วยปรับปรุงการสร้างข้อกำหนดเหล่านี้ เอกสารที่อ้างอิงในที่นี้ได้กล่าวถึงฮิวริสติกที่ควรใช้ในการออกแบบข้อกำหนดได้ดีที่สุด^{[ 6 ]}พวกเขาทำเช่นนั้นโดยการใช้แนวทาง แบ่งและพิชิต

สัญกรณ์ Zเป็นตัวอย่างหนึ่งของภาษากำหนดคุณสมบัติ อย่างเป็นทางการชั้นนำ ตัวอย่างอื่นๆ ได้แก่ ภาษากำหนดคุณสมบัติ (VDM-SL) ของวิธีการพัฒนาเวียนนาและสัญกรณ์เครื่องจักรนามธรรม (AMN) ของวิธีการ Bใน ด้าน บริการเว็บการกำหนดคุณสมบัติอย่างเป็นทางการมักใช้เพื่ออธิบายคุณสมบัติที่ไม่ใช่ฟังก์ชัน^{[ 7 ]} ( คุณภาพการ บริการของบริการเว็บ )

เครื่องมือบางอย่างได้แก่: ^{[ 4 ]}

• พีชคณิต
  1. ต้นสนชนิดหนึ่ง
  2. โอบีเจ
  3. บัว
• อิงตามแบบจำลอง
  1. ซ
  2. บี
  3. วีดีเอ็ม
  4. ซีเอสพี
  5. ตาข่ายเพทรี
  6. ทีแอลเอ+
  7. ฟิซบี

Wikimedia Commons มีสื่อที่เกี่ยวข้องกับข้อกำหนดอย่างเป็นทางการ (Formal specification )

• บทความเรื่อง "A Case for Formal Specification (Technology)"ถูกเก็บถาวรไว้ใน Wayback Machine เมื่อวันที่ 21 ตุลาคม 2548 โดย Coryoth เมื่อวันที่ 30 กรกฎาคม 2548