ทฤษฎีการรวมโปรแกรม ( Unifying Theories of Programmingหรือ UTP ) ในวิทยาการคอมพิวเตอร์เกี่ยวข้องกับความหมายของโปรแกรม โดยแสดงให้เห็นว่าความ หมายเชิงสัญลักษณ์ความหมายเชิงปฏิบัติการและความหมายเชิงพีชคณิตสามารถนำมาผสมผสานกันในกรอบการทำงานที่เป็นหนึ่งเดียวสำหรับการกำหนดคุณสมบัติอย่างเป็นทางการการออกแบบ และการนำโปรแกรมและระบบคอมพิวเตอร์ ไปใช้งาน ได้ อย่างไร

หนังสือชื่อนี้โดยCAR HoareและHe Jifeng ^{[ 1 ]}ได้รับการตีพิมพ์ในชุดหนังสือวิทยาศาสตร์คอมพิวเตอร์นานาชาติของ Prentice Hallในปี 1998 และเปิดให้ใช้งานได้ฟรีบนเว็บ^{[ 2 ]}

มีการเริ่มจัดชุดการประชุมสัมมนา UTP ในปี 2549 ^{[ 3 ]}

รากฐานทางความหมายของ UTP คือแคลคูลัสเชิงประพจน์ลำดับที่หนึ่งเสริมด้วยโครงสร้างจุดตรึงจากตรรกะลำดับที่สอง ตามแบบอย่างของEric Hehnerโปรแกรมต่างๆ ถือเป็นประพจน์ใน UTP และไม่มีความแตกต่างระหว่างโปรแกรมและข้อกำหนดในระดับความหมาย ดังที่Hoare กล่าวไว้ ว่า:

โปรแกรมคอมพิวเตอร์จะถูกระบุด้วยภาคแสดงที่แข็งแกร่งที่สุดที่อธิบายการสังเกตที่เกี่ยวข้องทั้งหมดที่สามารถทำได้เกี่ยวกับพฤติกรรมของคอมพิวเตอร์ที่ดำเนินการโปรแกรมนั้น^{[ 4 ]}

ในศัพท์เฉพาะของ UTP ทฤษฎีคือแบบจำลองของกระบวนทัศน์การเขียนโปรแกรมเฉพาะอย่างหนึ่ง ทฤษฎี UTP ประกอบด้วยส่วนประกอบสามอย่าง:

• อักษรชุดหนึ่งซึ่งเป็นชุดของชื่อตัวแปรที่บ่งบอกถึงคุณลักษณะของกระบวนทัศน์ที่หน่วยงานภายนอกสามารถสังเกตได้
• ลายเซ็นซึ่งเป็นชุดของโครงสร้างภาษาโปรแกรมที่เป็นส่วนสำคัญของกระบวนทัศน์นั้น และ
• ชุดของเงื่อนไขด้านสุขภาพซึ่งกำหนดขอบเขตของโปรแกรมที่เหมาะสมกับกรอบแนวคิด เงื่อนไขด้านสุขภาพเหล่านี้มักแสดงออกมาในรูปของทรานส์ฟอร์เมอร์เชิง述語แบบเอกภาคที่ ไม่เปลี่ยนแปลง

การปรับปรุงโปรแกรมเป็นแนวคิดสำคัญใน UTP โปรแกรมจะได้รับการปรับปรุงก็ต่อเมื่อการสังเกตทุกอย่างที่สามารถทำได้กับโปรแกรมนั้นเป็นการสังเกตของโปรแกรมด้วยเช่นกันนิยามของการปรับปรุงนั้นเหมือนกันในทฤษฎี UTP ทั่วไป: ${\displaystyle P_{1}}$${\displaystyle P_{2}}$${\displaystyle P_{2}}$${\displaystyle P_{1}}$

${\displaystyle P_{1}\sqsubseteq P_{2}\quad {\text{ก็ต่อเมื่อ}}\quad \left[P_{2}\Rightarrow P_{1}\right]}$

โดยที่^{[ 5 ]}หมายถึงการปิดสากลของตัวแปรทั้งหมดในตัวอักษร ${\displaystyle \left[X\right]}$

ทฤษฎี UTP ที่พื้นฐานที่สุดคือแคลคูลัสภาคแสดงตามลำดับตัวอักษร ซึ่งไม่มีข้อจำกัดเรื่องตัวอักษรหรือเงื่อนไขความสมบูรณ์ใดๆ ส่วนทฤษฎีความสัมพันธ์นั้นมีความเฉพาะเจาะจงมากกว่าเล็กน้อย เนื่องจากตัวอักษรของความสัมพันธ์อาจประกอบด้วยตัวอักษรได้เพียง:

• ตัวแปรที่ไม่มีการตกแต่ง ( ) ซึ่งจำลองการสังเกตโปรแกรมเมื่อเริ่มต้นการทำงาน และ${\displaystyle v}$
• ตัวแปรไพรม์ ( ) จำลองการสังเกตโปรแกรมในขั้นตอนต่อมาของการดำเนินการ${\displaystyle v'}$

โครงสร้างทางภาษาทั่วไปบางอย่างสามารถนิยามได้ในทฤษฎีความสัมพันธ์ดังนี้:

• คำสั่ง skip ซึ่งไม่เปลี่ยนแปลงสถานะของโปรแกรมแต่อย่างใด ถูกจำลองขึ้นมาในรูปแบบของเอกลักษณ์เชิงสัมพันธ์:

${\displaystyle \mathbf {skip} \equiv v'=v}$

• การกำหนดค่าให้กับตัวแปรหนึ่งนั้น จำลองได้โดยการตั้งค่า ตัวแปรหนึ่ง เป็น ค่าคงที่ และคงค่าตัวแปรอื่นๆ ทั้งหมด (ซึ่งแทนด้วย) ให้คงที่:${\displaystyle E}$${\displaystyle a}$${\displaystyle a'}$${\displaystyle E}$${\displaystyle u}$

${\displaystyle a:=E\equiv a'=E\land u'=u}$

• การประกอบลำดับของโปรแกรมสองโปรแกรมก็คือการประกอบเชิงสัมพันธ์ของสถานะกลางนั่นเอง:

${\displaystyle P_{1};P_{2}\equiv \exists v_{0}\bullet P_{1}[v_{0}/v']\land P_{2}[v_{0}/v]}$

• การเลือกใช้โปรแกรมแบบไม่แน่นอนถือเป็นขีดจำกัดล่างสุดของวิธีการนี้:

${\displaystyle P_{1}\sqcap P_{2}\equiv P_{1}\lor P_{2}}$

• การเลือกแบบมีเงื่อนไขระหว่างโปรแกรมต่างๆ เขียนโดยใช้สัญกรณ์แบบอินฟิกซ์:

${\displaystyle P_{1}\triangleleft C\triangleright P_{2}\equiv (C\land P_{1})\lor (\lไม่ใช่ C\land P_{2})}$

• ความหมายของการเรียกซ้ำนั้นกำหนดโดยจุดตรึงที่เล็กที่สุด ของตัวแปลง述語แบบโมโนโทนิก:${\displaystyle \mu \mathbf {F} }$${\displaystyle \mathbf {F} }$

${\displaystyle \mu X\bullet \mathbf {F} (X)\equiv \sqcap \left\{X\mid \mathbf {F} (X)\sqsubseteq X\right\}}$

• Woodcock, Jim ; Cavalcanti, Ana (2004). "บทนำเชิงแนะนำเกี่ยวกับการออกแบบในทฤษฎีการเขียนโปรแกรมแบบบูรณาการ" (PDF)วิธีการเชิงรูปธรรมแบบบูรณาการบันทึกการบรรยายในวิทยาการคอมพิวเตอร์ หน้า 40–66 เล่มที่ 2999 Springer หน้า  40–66 doi : 10.1007/978-3-540-24756-2_4 ISBN 978-3-540-21377-2.
• Cavalcanti, Ana; Woodcock, Jim (2006). " บทนำเชิงสอนเกี่ยวกับ CSP ในทฤษฎีการเขียนโปรแกรมแบบรวม" (PDF)เทคนิคการปรับปรุงในวิศวกรรมซอฟต์แวร์บันทึกการบรรยายในวิทยาการคอมพิวเตอร์ เล่มที่ 3167 Springer หน้า  220–268 doi : 10.1007 /11889229_6 ISBN 978-3-540-46253-8.

• เว็บไซต์หนังสือ UTP
• หนังสือ UTPบนArchive.org
• หนังสือ UTPในห้องสมุดเปิด ของ Internet Archive