程式正確性理論

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