程序正確性理論(theory of program correctness)是程序設計理論的一個重要組成部分，研究如何使用程序設計語言編製程序，以正確實現預定的目標。
程序正確性理論 (theory of program correctness)程序設計理論的一個重要組成部分。研究如何使用程序設計語言編製程序，以正確實現預定的目標。程序正確性理論提出編製正確程序的兩種途徑一種稱為程序驗證，研究如何使用
數學推理來嚴格論證程序是否符合其目標。另一種稱為程序綜合，研究如何由給定目標出發，逐步構造一個在計算機系統上可運行的程序，而且要求
構造過程的每一步都是嚴格保持正確無誤的。在保證正確性的前提下，為提高程序運算效率而實現的程序之間的轉換，稱為程序變形，也是程序正確性理論的一個重要內容。
程序綜合和程序變形是
自動程序設計的理論基礎.