Luận lý Hoare

Bách khoa toàn thư mở Wikipedia
Bước tới: menu, tìm kiếm

Luận lý Hoare (còn được biết đến với tên Luận lý Floyd–Hoare) là một hệ chính quy do nhà khoa học máy tính người Anh C. A. R. Hoare phát triển, và sau đó được Hoare và những nhà nghiên cứu khác tinh lọc lại. Mục đích của hệ thống là cung cấp một tập các quy luật luận lúy để suy luận tính đúng đắn của các chương trình máy tính bằng tính chính xác của luận lý toán học.

Nó được xuất bản trong bài báo năm 1969 của Hoare[1], ở đó Hoare đã sử dụng lại những đóng góp trước đó của Robert Floyd, người đã xuất bản một hệ thống tương tự dành cho sơ đồ luồng (flowchart).

Đặc điểm trung tâm của luận lý Hoarebộ ba Hoare. Bộ ba này mô tả sự thực thi một đoạn mã có thể thay đổi trạng thái tính toán như thế nào. Bộ ba Hoare có dạng

\{P\}\;C\;\{Q\}

trong đó PQ là những khẳng địnhC là một mệnh lệnh. P được gọi là tiền điều kiệnQhậu điều kiện. Những khẳng định là những công thức có dạng luận lý vị từ.

Luận lý Hoare có những tiên đềluật suy diễn dành cho tất cả những mẫu cơ bản của ngôn ngữ lập trình mệnh lệnh. Ngoài các luật dành cho ngôn ngữ đơn giản trong bài báo nguyên thủy của Hoare, những luật dành cho những mẫu ngôn ngữ khác cũng đã được phát triển từ lúc đó bởi Hoare và nhiều nhà nghiên cứu khác. Có những luật dành cho đồng thời, thủ tục, nhảy, và con trỏ.

Tính đúng đắn bộ phận và toàn phần[sửa | sửa mã nguồn]

Luận lý Hoare chuẩn chỉ chứng minh tính đúng đắn bộ phận, trong khi điều kiện dừng phải được chứng minh độc lập. Do đó cách diễn dịch bộ ba Hoare là: Nếu P là trạng thái trước khi thực thi C, thì Q sẽ là trạng thái sau khi thực thi nó, hoặc C không dừng (chạy vô tận). Chú ý rằng nếu C không dừng thì sẽ không có khái niệm "sau", do đó Q có thể là bất cứ thứ gì. Thực vậy, người ta có chọn Q là false để diễn tả rằng C không dừng.

Tính đúng đắn toàn phần cũng có thể được chứng minh bằng phiên bản mở rộng của quy luật While.

Các quy luật[sửa | sửa mã nguồn]

Luật tiên đề rỗng[sửa | sửa mã nguồn]

 \frac{}{\{P\}\ \textbf{skip}\ \{P\}} \!

Luật về phát biểu gán[sửa | sửa mã nguồn]

Tiên đề gán chỉ ra rằng sau phép gán, bất kỳ vị từ nào chứa biến là true đối với vế phải phép gán:

 \frac{}{\{P[x/E]\}\ x:=E \ \{P\} } \!

Ở đây P[x/E] chỉ ra rằng biểu thức P trong đó tất cả các lần xuất hiện tự do của biến x đã được thay bằng biểu thức E.

Ý nghĩa của tiên đề gán này là giá trị đúng sai của \{P[x/E]\} là tương đương với giá trị đúng sai của \{P\} sau khi gán. Do đó nếu \{P[x/E]\}true trước phép gán, nhờ tiên đề gán \{P\} cũng sẽ true sau phép gán. Ngược lại, nếu \{P[x/E]\}false trước phép gán, thì chắc chắn \{P\} phải là false sau phép gán.

Các ví dụ về những bộ ba đúng:

  • \{x+1 = 43\}\ y:=x + 1\ \{ y = 43 \}\!
  • \{x + 1 \leq N \}\ x:= x  + 1\ \{x \leq N\}\ \!

Tiên đề gán do Hoare đưa ra không áp dụng vào trường hợp có nhiều hơn một tên cùng chỉ một giá trị lưu trữ. Ví dụ,

\{ y = 3\} \ x:= 2\ \{y = 3 \}

là không đúng nếu xy cùng đại diện cho một biến, vì không có tiền điều kiện nào có thể khiến cho y bằng 3 sau khi x được gán bằng 2.

Luật ghép[sửa | sửa mã nguồn]

Luật về phát biểu ghép của Hoare áp dụng cho những chương trình được thực thi tuần tự ST, trong đó S thực thi trước T và được viết là S;T.

 \frac {\{P\}\ S\ \{Q\}\, \ \{Q\}\ T\ \{R\} } {\{P\}\ S;T\ \{R\}} \!

Ví dụ, xét hai phát biểu sau:

\{ x + 1 = 43\} \ y:=x + 1\ \{y =43 \}

\{ y = 43\} \ z:=y\ \{z =43 \}

Theo luật ghép, ta có thể kết luận:

\{ x + 1 = 43\} \ y:=x + 1; z:= y\ \{z =43 \}

Luật điều kiện[sửa | sửa mã nguồn]

\frac { \{B \wedge P\}\ S\ \{Q\}\,\ \{\neg B \wedge P \}\ T\ \{Q\} }
              { \{P\}\ \textbf{if}\ B\ \textbf{then}\ S\ \textbf{else}\ T\ \textbf{endif}\ \{Q\} } \!

Luật While[sửa | sửa mã nguồn]

\frac { \{P \wedge B \}\ S\ \{P\} }
              { \{P \}\ \textbf{while}\ B\ \textbf{do}\ S\ \textbf{done}\ \{\neg B \wedge P\} }
\!

Ở đây Pđiều kiện bất biến của vòng lặp.

Luật hệ quả[sửa | sửa mã nguồn]


\frac {  P^\prime \rightarrow\ P\,\ \lbrace P \rbrace\ S\ \lbrace Q \rbrace\,\ Q \rightarrow\ Q^\prime }
 	{ \lbrace P^\prime\ \rbrace\ S\ \lbrace Q^\prime\rbrace }
\!

Luật While dành cho tính đúng đắn toàn phần[sửa | sửa mã nguồn]


\frac { \{P \wedge B \wedge t = z \}\ S\ \{P \wedge t < z \} \,\ P \rightarrow t \geq 0}
              { \{P \}\ \textbf{while}\ B\ \textbf{do}\ S\ \textbf{done}\ \{\neg B \wedge P\} }
\!

Trong luật này, ngoài việc giữ các điều kiện bất biến vòng lặp, ta cũng phải chứng minh dừng bằng cách chứng minh giá trị của một số hạng giảm dần sau mỗi lần lặp, ở đây là t. Chú ý rằng t phải là giá trị thuộc tập chắc chắn, để cho mỗi bước lặp có thể tính được bằng cách giảm giá trị đi một chuỗi hữu hạn.

Ví dụ[sửa | sửa mã nguồn]

Example 1
\{x+1 = 43\}\! \ y:=x + 1\ \! \{ y = 43 \}\! (Tiên đề gán)
(x + 1 = 43 \implies x = 42)
\{x=42\}\! \ y:=x + 1\ \! \{y=43 \land x=42\}\! (Luật hệ quả)
Example 2
\{x + 1 \leq N \}\! \ x:= x  + 1\ \! \{x \leq N\}\ \! (Tiên đề gán)
( x < N \implies x + 1 \leq N với x, N là kiểu số nguyên.)
\{x < N \}\! \ x:= x  + 1\ \! \{x \leq N\}\ \! (Luật hệ quả)

Xem thêm[sửa | sửa mã nguồn]

Tham khảo[sửa | sửa mã nguồn]

  1. ^ C. A. R. Hoare. "An axiomatic basis for computer programming". Communications of the ACM, 12(10):576–585, tháng 10 năm 1969. doi:10.1145/363235.363259

Đọc thêm[sửa | sửa mã nguồn]

Liên kết ngoài[sửa | sửa mã nguồn]

  • Project Bali has defined Hoare logic-style rules for a subset of the Java programming language, for use with the Isabelle theorem prover
  • KeY-Hoare is a semi-automatic verification system built on top of the KeY theorem prover. It features a Hoare calculus for a simple while language.
  • j-Algo-modul Hoare calculus — A visualisation of the Hoare calculus in the in the algorithm visualisation program j-Algo