Luận lý Hoare

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ý để 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ý Hoare là bộ 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

${\displaystyle \{P\}\;C\;\{Q\}}$

trong đó P và Q là những khẳng định và C là một mệnh lệnh. P được gọi là tiền điều kiện và Q là hậ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 đề và 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

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

Luật tiên đề rỗng

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

Luật về phát biểu gá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:

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

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

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

• ${\displaystyle \{x+1=43\}\ y:=x+1\ \{y=43\}\!}$
• ${\displaystyle \{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ụ,

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

là không đúng nếu x và y 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

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ự S và T, trong đó S thực thi trước T và được viết là S;T.

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

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

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

và

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

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

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

Luật điều kiện

${\displaystyle {\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

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

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

Luật hệ quả

${\displaystyle {\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

${\displaystyle {\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ụ

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

Xem thêm

• Thiết kế theo hợp đồng
• Luận lý động
• Edsger W. Dijkstra
• Ngữ nghĩa biến đổi vị từ
• Thẩm định chương trình
• Phân tích mã tĩnh
• Điều kiện bất biến của vòng lặp

Tham khảo

1. C. A. R. Hoare. "An axiomatic basis for computer programming Lưu trữ 2016-03-04 tại Wayback Machine". Communications of the ACM, 12(10):576–585, tháng 10 năm 1969. doi:10.1145/363235.363259

Đọc thêm

• Robert D. Tennent. Specifying Software (a recent textbook that includes an introduction to Hoare logic) ISBN 0-521-00401-2

Liên kết ngoài

• Project Bali Lưu trữ 2011-05-13 tại Wayback Machine has defined Hoare logic-style rules for a subset of the Java programming language, for use with the Isabelle theorem prover
• KeY-Hoare Lưu trữ 2007-11-17 tại Wayback Machine 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 Lưu trữ 2011-05-05 tại Wayback Machine — A visualisation of the Hoare calculus in the in the algorithm visualisation program j-Algo