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

การกำหนดคุณสมบัติเชิงพีชคณิตมุ่งพัฒนาโปรแกรมให้มีประสิทธิภาพมากขึ้นอย่างเป็นระบบโดย:

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

การกำหนดคุณสมบัติเชิงพีชคณิตบรรลุเป้าหมายเหล่านี้โดยการกำหนดชนิดข้อมูลอย่างน้อยหนึ่งชนิด และระบุชุดฟังก์ชันที่ทำงานกับชนิดข้อมูลเหล่านั้น ฟังก์ชันเหล่านี้สามารถแบ่งออกได้เป็นสองประเภท:

1. ฟังก์ชันตัวสร้าง (Constructor functions ): ฟังก์ชันที่สร้างหรือกำหนดค่าเริ่มต้นให้กับองค์ประกอบข้อมูล หรือสร้างองค์ประกอบที่ซับซ้อนจากองค์ประกอบที่เรียบง่ายกว่า ชุดของฟังก์ชันตัวสร้างที่มีอยู่จะถูกกำหนดโดยลายเซ็น ของข้อกำหนด นอกจากนี้ ข้อกำหนดอาจมีสมการที่กำหนดความเท่าเทียมกันระหว่างวัตถุที่สร้างขึ้นโดยฟังก์ชันเหล่านี้ การแสดงผลพื้นฐานจะเหมือนกันหรือไม่สำหรับโครงสร้างที่แตกต่างกันแต่เทียบเท่ากันนั้นขึ้นอยู่กับการใช้งาน
2. ฟังก์ชันเพิ่มเติม : ฟังก์ชันที่ทำงานกับชนิดข้อมูล และถูกกำหนดขึ้นโดยใช้ฟังก์ชันตัวสร้าง

พิจารณาข้อกำหนดเชิงพีชคณิตอย่างเป็นทางการสำหรับชนิดข้อมูล บูลีน

ข้อกำหนดทางพีชคณิตที่เป็นไปได้ข้อหนึ่งอาจให้ฟังก์ชันตัวสร้างสองฟังก์ชันสำหรับองค์ประกอบข้อมูล ได้แก่ ตัวสร้าง ค่าจริงและ ตัวสร้าง ค่าเท็จดังนั้น องค์ประกอบข้อมูลแบบบูลีนจึงสามารถประกาศ สร้าง และกำหนดค่าเริ่มต้นได้ ในสถานการณ์นี้องค์ประกอบการเชื่อมต่อ อื่นๆ ทั้งหมด เช่นXORและANDจะเป็นฟังก์ชันเพิ่มเติมดังนั้น องค์ประกอบข้อมูลจึงสามารถกำหนดค่าได้ด้วยค่า "จริง" หรือ "เท็จ" และสามารถใช้ฟังก์ชันเพิ่มเติมเพื่อดำเนินการใดๆ กับองค์ประกอบข้อมูลได้

อีกทางเลือกหนึ่งคือ สามารถกำหนดระบบข้อมูลประเภทบูลีนทั้งหมดได้โดยใช้ชุดฟังก์ชันตัวสร้างที่แตกต่างกัน ได้แก่ ตัวสร้าง ค่าเท็จและ ตัวสร้างค่า ไม่ใช่ ในกรณีนั้น อาจกำหนดฟังก์ชันtrue เพิ่มเติมเพื่อให้ได้ค่า ไม่ใช่เท็จ และ ควรเพิ่ม สมการ เข้าไปด้วย${\displaystyle ({\text{ไม่ใช่}}\;{\text{ไม่ใช่}}\;x)=x}$

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

สำหรับตัวอย่างที่ซับซ้อนกว่านี้ สามารถระบุ จำนวนเต็มได้ (นอกเหนือจากวิธีการอื่นๆ อีกมากมาย และโดยการเลือกรูปแบบใดรูปแบบหนึ่งจากหลายรูปแบบ) ด้วยตัวสร้างสองตัว

 1 : Z (_ - _) : Z × Z -> Z 

และสมการสามสมการ:

 (1 - (1 - p)) = p ((1 - (n - p)) - 1) = (p - n) ((p1 - n1) - (n2 - p2)) = (p1 - (n1 - (p2 - n2))) 

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

 ... (((1 - 1) - 1) - 1) ((1 - 1) - 1) (1 - 1) 1 (1 - ((1 - 1) - 1)) (1 - (((1 - 1) - 1) - 1)) ... 

ดังนั้น การใช้งานใดๆ ที่สอดคล้องกับข้อกำหนดนี้ จะทำงานเหมือนกับจำนวนเต็ม หรืออาจจะเป็นช่วงที่จำกัดของจำนวนเต็ม เช่นเดียวกับชนิดข้อมูลจำนวนเต็มทั่วไปที่พบในภาษาโปรแกรมส่วนใหญ่

• ภาษากำหนดคุณสมบัติพีชคณิตทั่วไป
• ข้อกำหนดอย่างเป็นทางการ
• โอบีเจ