Giáo trình Công nghệ phần mềm - Phần 1 - Phan Huy Khánh

Điều kiện trước E được tính toán theo quy tắc đã trình bày ở mục I để tạo ra các tiên đề gán là điều kiện trước yếu nhất của một lệnh gán x := và của một điều kiện sau S, khi đại lượng termE(x := ) có giá trị true. Trong trường hợp này, tiên đề được ký hiệu bởi : pfpre(x := , S) { x := } S Trong trường hợp tổng quát, ta có : pfpre(x := , S) ~ if pfpre(x := , true) then S(x / ) else false. Điều kiện pfpre(x := , true) thể hiện : - x và các toán hạng của được định nghĩa : chỉ số của mảng nằm giữa cận dưới và cận trên, các con trỏ chỉ đến các biến khác nil, v.v., - mọi phép toán thực thi đều cho kết quả : có sự tương thích về kiểu của các toán hạng, không có phép chia cho 0, v.v. Ở đây ta không thấy sự vi phạm về tính hợp thức của các tiên đề đã nêu trong mục I về tính đúng đắn từng phần : nếu termE(x := ) có giá trị false, phát biểu E { x := } S là true. Người ta có thể củng cố điều kiện trước của các tiên đề này bởi các điều kiện do pfpre(x := , true) đưa đến.