Trong chứng minh tính đúng đắn, một tên gọi chỉ ra rằng một chương trình khẳng định đầu ra theo một cách hợp lý từ khẳng định đầu vào và xử lý bước của nó, và rằng, ngoài ra, chương trình chấm dứt theo tất cả quy định đầu vào điều kiện.