NGHIÊN CỨU HỆ TIÊN ĐỀ HOARE VÀ TRIỂN KHAI TRÊN NGÔN NGỮ JAVA

NGHIÊN CỨU HỆ TIÊN ĐỀ HOARE VÀ TRIỂN KHAI TRÊN NGÔN NGỮ JAVA

• Ý NGHĨA VẤN ĐỀ NGHIÊN CỨU

Lập trình máy tính là một công việc mà trong đó tài năng của các nhà toán học được yêu cầu rất cấp thiết và có thể được ứng dụng hiệu quả nhất. Toán học của lập trình là một chủ đề thú vị cho nghiên cứu, và hứa hẹn mang lại những kết quả hữu ích. Nhưng thách thức cũng là động lực đó là áp dụng toán học và kĩ nghệ để thiết kế và đưa ra một sản phẩm có thể tin tưởng thực hiện một dịch vụ có giá trị. Đó thường là một kiểu sản phẩm mới và đôi khi trở nên vượt trội.

Lập trình cũng là một trong những lĩnh vực khó nhất của toán học ứng dụng. Có thể coi lập trình như một khoa học. Khoa học này không nhằm đặt ra những công cụ thần kì hoặc những phép màu nhiệm mà chỉ đề xuất những nguyên lý và phương pháp nhằm nâng cao năng xuất lao động cho các lập trình viên. Năng suất

• đây cần được hiểu theo nghĩa khác với tiết kiệm một bit, một byte hoặc một phần ngàn giây mà định hướng trước hết đến tính đúng đắn của chương trình, tính dễ đọc dễ thực hiện, dễ sửa, tận dụng tối đa khả năng của thiết bị mà vẫn không phụ thuộc vào thiết bị.

Thêm nữa, bất kì quốc gia nào cũng có những lĩnh vực cần có những chương trình máy tính tuyệt đối đúng như điều khiển phản ứng hạt nhân, đưa người lên mặt trăng, chiến tranh mạng, … đều đòi hỏi cơ sở toán học và buộc phải chứng minh tính đúng. Trở thành chuyên gia trong lĩnh vực này là rất đáng quý.

Như vậy tiêu chuẩn số một của kĩ sư phần mềm là phải biết diễn đạt trong sáng và đúng đắn các chỉ thị. Thực chất của quá trình lập trình người ta không lập trình trên một ngôn ngữ cụ thể mà lập trình hướng tới nó. Chương trình phải được biết dưới dạng các thao tác có cấu trúc trên các đối tượng có cấu trúc và các mệnh đề nhằm khẳng định tính đúng đắn của kết quả. Vậy vấn đề đặt ra là làm sao để chứng minh tính đúng đắn của chương trình. Do đó việc vận dụng các tiên đề của Hoare và các chứng minh toán học để giải quyết vấn đề là rất cần thiết.

3

2. MỤC TIÊU NGHIÊN CỨU

• Tìm hiểu các tiên đề Hoare
• Tìm hiểu các kỹ thuật chứng minh tính đúng của chương trình
• Triễn khai hệ tiên đề Hoare cho lập trình dựa trên ngôn ngữ Java
• Vận dụng chứng minh tính đúng của chương trình vào một số chương

trình truyền thống

Những vấn đề được đề cập trong đề tài có thể được áp dụng thực tế vào việc chứng minh tính đúng của chương trình và phát triển ngôn ngữ lập trình. Yêu cầu thực tế đối với các chuyên viên phát triển phần mềm đó là có thể cho ra một sản phẩm phần mềm tốt tức là phải đảm bảo chương trình đúng.

3. ĐỐI TƢỢNG NGHIÊN CỨU

• Các phương pháp chứng minh toán học và cách đặt vấn đề chứng minh tính đúng của chương trình
• Hệ tiên đề Hoare

4. PHƢƠNG PHÁP NGHIÊN CỨU

• Về lý thuyết

o Nghiên cứu về hệ tiên đề Hoare kết hợp với các phương pháp chứng minh toán học

o Nghiên cứu sơ đồ cách chứng minh thuật toán Euclid‟s mở rộng

• Về thực nghiệm

o Chương trình được viết bằng ngôn ngữ Java, theo phương pháp lập trình tuần tự để xây dựng, thiết kế chương trình theo các thuật toán đã nghiên cứu.

Thế nào là chứng minh tính đúng của chương trình?

4

Chứng minh tính đúng của chương trình trước tiên được hiểu các ngữ nghĩa của một chương trình phù hợp với một số đặc điểm kỹ thuật cho chương trình. Có hai điều kiện đầu tiên cho việc này: Thứ nhất phải có một số đặc điểm kỹ thuật chính thức cho chương trình. Như một định nghĩa có thể mang hình thức của một bộ tiên đề. Thứ hai là một bộ quy tắc suy luận cho thấy làm thế nào ngữ nghĩa của bất kì đoạn mã nào trong chương trình là đúng.

Như vậy ta có thể đưa ra hai khẳng định:

• Xác nhận đầu vào Input khẳng định là đúng thì đầu ra Output cũng phải được khẳng định là đúng
• Chứng minh tính đúng đắn từng phần của chương trình bằng cách ở giữa Input và Output của chương trình ta gắn các khẳng định và trước và sau mỗi câu lệnh. Các khẳng định này gọi là trung gian xác nhận. Với mỗi

câu lệnh sau khi tuyên bố thì các khẳng định này biết đến tương ứng như là điều kiện đầu và cuối của tuyên bố đó

Ta thấy rằng việc chứng minh tính đúng của chương trình là bằng cách xử lý các chương trình như một đối tượng toán học mà tiên đề nhất định và quy tắc suy luận được áp dụng.

5. BỐ CỤC CỦA LUẬN VĂN

Tên đề tài: “Nghiên cứu hệ tiên đề Hoare và triển khai trên ngôn ngữ Java” Toàn bộ nội dung luận văn được chia thành 3 chương:

• Chƣơng 1: TỔNG QUAN VỀ CÔNG NGHỆ PHẦN MỀM

Đề cập sơ lược các tính chất cơ bản trong quy trình phát triển phần mềm hiện đại. Đề cập đến những vấn đề cần giải quyết trong lập trình máy tính, kiểm soát chương trình và chứng minh tính đúng của chương trình.

• Chƣơng 2: HỆ TIÊN ĐỀ HOARE

5

Tìm hiểu và phát triển các kỹ thuật chứng minh chương trình là đúng đắn. Việc xác định một chương trình là đúng trong thực tế thường được tiếp cận với 2 phương pháp:

o Kiểm thử (testing) chương trình nhưng không thể chứng mình chương trình hoàn toàn đúng.

o Chứng minh chương trình đúng bằng kỹ thuật dựa trên bộ tiên đề và suy luận toán học dựa trên hệ tiên đề Hoare.

• Chƣơng 3:

Chứng minh tính đúng đắn của thuật toán trong các chương trình máy tính truyền thống tổ chức từ đơn giản đến phức tạp và được lập trình viên sử dụng nhiều trong các ứng dụng phần mềm áp dụng phương pháp đặt vấn đề và suy luận với hệ tiên đề Hoare.

Các chương trình được sử dụng để chứng mình bao gồm:

1. Các thuật toán số học:
   • Thuật toán tính số fibonacci thứ n
   • Thuật toán nhân nhanh hai số Ấn Độ
   • Thuật toán chia nhanh hai số Ấn Độ
   • Thuật toán Eulid‟s
   • Thuật toán Eulid‟s mở rộng
2. Các thuật toán về cấu trúc dữ liệu:
   1. Thuật toán tìm phần tử có giá trị lớn trong mảng với vòng lặp 1 biến
   2. Thuật toán tô màu cờ Hà Lan – nhóm các phần từ cùng tính chất trong mảng

KẾT LUẬN VÀ HƯỚNG PHÁT TRIỂN

TÀI LIỆU THAM KHẢO

6

CHƢƠNG 1

TỔNG QUAN VỀ CÔNG NGHỆ PHẦN MỀM

1.1. LƢỢC SỬ VỀ CÔNG NGHỆ PHẦN MỀM

1.1.1. Kỹ thuật lập trình giai đoạn thứ nhất của máy tính điện tử

Trước những năm sáu mươi người ta coi lập trình như hoạt động nghệ thuật nhuốm màu sắc tài nghệ cá nhân hơn là khoa học. Thời đó được hiểu như: một người nắm được một ngôn ngữ lập trình và một mẹo vặt tận dụng cấu hình vật lý cụ thể của máy tính có thể được coi là một chuyên gia nắm bắt được những bí ẩn của nghệ thuật lập trình.

1.1.2. Cuộc khủng hoảng lập trình những năm 60

1.1.3. Những tƣ tƣởng cách mạng trong lập trình

Tính cách mạng của những quan điểm khoa học nảy nở trong giai đoạn này thể hiện ở những điểm sau:

• Chương trình máy tính và lập trình viên trở thành đối tượng nghiên cứu của lý thuyết lập trình.
• Vấn đề cơ bản đặt ra đối với lý thuyết lập trình là làm thế nào để có thể làm chủ được sự phức tạp của hoạt động lập trình.
• Do trí tuệ của từng cá nhân lập trình viên là có hạn mà các vấn đề thực tiễn cần giải quyết bằng các công cụ tin học là lớn và phức tạp cho nên vấn đề đặt ra là liệu có thể phân một bài toán lơn thành những bài toán nhỏ có độ phức tạp thấp để giải riêng sau đó tổng hợp kết quả lại được không?

Bất kì quốc gia nào cũng cần có nhưng chương trình máy tính tuyệt đối đúng. Chi phí để bảo trì những chương trình như vậy thường rất lớn.

7

1.2. MỤC TIÊU CỦA CÔNG NGHỆ PHẦN MỀM

1.2.1. Công nghệ phần mềm là gì?

Việc phát triển phần mềm nhằm đặt được các tiêu chí cơ bản sau một cách tốt nhất:

• Tính đúng đắn
• Tính khoa học (hệ thống)
• Tính dễ đọc
• Tính dễ sửa đổi, cải tiến
• Tính dễ sử dụng
• Tính phổ dụng
• Tính độc lập với thiết bị

Ngoài ra tùy vào mục tiêu của dự án phần mềm và lĩnh vực áp dụng phần mềm thì phải thõa mãn thêm những tiêu chi cơ bản đặc trưng khác.

Trong thực tiễn ta thường gặp những bài toán phức tạp trong các dự án như xây dựng hệ điều hành, chương trình dịch, những hệ thống phần mềm chuyên sâu cho các ngành kinh tế, khoa học tự nhiên… Nếu bài toán có độ phức tạp lớn rõ ràng nó vượt khỏi tầm tay của một lập trình viên phát triển đơn lẻ. Nó đòi hỏi một nhóm có tổ chức của các chuyên viên phát triển phần mềm thành thạo trong việc sử dụng các kĩ nghệ phát triển phần mềm. Công nghệ phần mềm hướng tới mục tiêu nói trên đó là tổ chức một nhóm người liên quan để thiết kế và cài đặt được những chương trình đáp ứng các tiêu chí chuẩn xác.

8

1.2.2. Những nội dung cơ bản của công nghệ phần mềm

1.2.2.1. Tìm hiểu và phân tích các yêu cầu

1.2.2.2. Đặc tả thiết kế chương trình (Program Specification)

1.2.2.3. Lập trình cấu trúc (Structured Programming)

1.2.2.4. Kiểm thử chương trình một cách hệ thống (Systemic Testing)

1.2.2.5. Chứng minh tính đúng đắn của chương trình

1.2.2.6. Quy trình đảm bảo chất lượng chương trình

1.2.2.7. Quản lí thiết kế, cài đặt, lập hồ sơ

CHƢƠNG 2

HỆ TIÊN ĐỀ HOARE

Mục đích chính của luận văn là tìm hiểu và phát triển các kỹ thuật chứng minh chương trình là đúng đắn. Việc xác định một chương trình là đúng trong thực tế có thể được tiếp cận với 2 phương pháp là:

• Kiểm thử chương trình (software testing) nhưng không thể nào xác định một chương trình là hoàn toàn đúng vì tính chất vô hạn của dữ liệu đầu vào (input)
• Chứng minh chương trình đúng bằng kỹ thuật dựa trên bộ tiên đề và suy luận toán học

Hệ tiên đề Hoare là một hệ chính quy do nhà khoa học máy tính C.A.R Hoare phát triển và sau đó được những nhà nghiên cứu khác tinh lọc lại. Mục đích của hệ tiên đề là cung cấp một tập các luật để 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 toán học.

Đặc điểm trung tâm của hệ tiên đề Hoare được gọi là bộ ba Hoare:

{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à điều kiện trước và Q là điều kiện sau.

9

Hệ tiên đề Hoare có những tiên đề và luật suy diễn cơ bản dành cho tất cả những ngôn ngữ lập trình mệnh lệnh tuần tự.

2.1. TIÊU CHUẨN TÍNH ĐÚNG ĐẮN CHO MỘT SẢN PHẨM PHẦN MỀM

Chương trình P được gọi là đúng nếu P thực hiện đầy đủ và chính xác những yêu cầu của nhà thiết kế đó là nếu dữ liệu vào Input có tính chất A sau khi thực hiện chương trình P thì dữ liệu ra Output phải có tính chất B. Trong đó A, B là các mệnh đề logic.

2.2. CÁCH ĐẶT VẤN ĐỀ CHỨNG MINH

Chương trình như một bộ biến đổi tuần tự P chuyển dữ liệu đầu vào có tính chất X thành dữ liệu đầu ra có tính chất Y. Khi lập trình, người lập trình đã xác định được mục tiêu hết sức rõ ràng, tức là chúng ta đã biết cái đầu vào X và cái ra là Y.

Việc là cơ bản là xác định dãy thao tác tuần tự P sao cho:

X Y {Trong đó: vào X, ra Y}

• input: X P?
• output: Y

X là mệnh đề nói về cái ta có hay là miền xác định của chương trình P. Ta

cũng có thể nói X là tính chất của dữ liệu đầu vào của chương trình P. Còn Y là

mệnh đề nói về cái ta muốn có hay là miền giá trị của P, ta cũng hiểu Y là tính chất

của tập dữ liệu ra mà ta mong muốn.

X và Y là do người thiết kế

2.3. TIÊN ĐỀ GÁN

2.3.1. Phát biểu

Tiên đề gán:

10

• • A

x = e;

• • Q
  • A → Q[x/e]
• nghĩa:

Điều kiện đủ để Q đúng sau khi thực hiện lệnh gán x = e, trong đó e là một biểu thức, là trước khi thực hiện lệnh gán nói trên ta phải có Q[x/e] đúng. Q[x/e] là mệnh đề thu được từ Q bằng phép thay thế mọi xuất hiện trong Q của x bằng e. Một dạng phát biểu khác của tính chất trên là:

Điều kiện đủ để có Q sau khi thực hiện lệnh gán x = e; là trước đó ta phải có P suy dẫn được ra Q[x/e].

2.3.2. Kỹ thuật chứng minh

Bước 1: Xác định output và input (giả sử P, Q là mệnh đề logic mô tả tính chất input và output)

Bước 2: Xuất phát từ mệnh đề Q (output) ta lần ngược lên trên tuần tự qua các phép gán để được các mệnh đề Q1= Q[x/e], Q2 = Q1[x/e], … Qn cho đến khi gặp P (input)

Bước 3: Chứng minh P → Qn

2.3.3. Ví dụ minh họa

Ví dụ 1:

Đoạn chương trình cho đầu vào Input là 1 số nguyên x, với x > n. Sau khi thực hiện chương trình thu được kết quả là 1 số nguyên x, thõa x > n + 1.

• P: x > n
• P1 = Q[x/(x + 1)]: x + 1 < x + 1 + 1
  1. = x + 1;

11

// Q: x > n + 1

Đề có Q đúng, cần chứng minh P → P1, bằng phương pháp biến đổi lần ngược từ mệnh đề Q.

Ta có P1=Q[x/(x + 1)]: x + 1 > n + 1 <=> x > n + 2 → P: x > n + 1, mệnh đề cần chứng minh.

2.4. TIÊN ĐỀ TUẦN TỰ

2.4.1. Phát biểu

Trong ngôn ngữ lập trình Java tiên đề tuần tự được phát biểu như sau

Nếu /* A */ P₁ ; /* B */

Và/*B*/P₂; /*C*/

Thì /* A */ P₁ , P₂ /* C */

2.4.2. Kĩ thuật chứng minh

Cho các dãy lệnh P₁;

P₂;

.

.

.

P_n;

// I

Nếu // I thực hiện P thì được // Q P₁;

P₂;

.

.

.

P_n;

// Q

12

Quy trình chức minh // I

P₁;

• I₁ P₂;

.

.

.

P_n;

• • I_n
• Thực hiện dãy lệnh tuần tự từ trên xuống dưới, từ trái qua phải
• Phải chứng minh I_n → Q được thì chương trình đúng, không được thì chương trình sai
• Lập luận chứng minh được chương trình

2.5. TIÊN ĐỀ CẤU TRÚC RẼ NHÁNH

2.5.1. Phát biểu

Trong ngôn ngữ lập trình Java cấu trúc rẽ nhánh có hai dạng cú pháp như

sau

Dạng đủ:

if(e) P; else Q;

Nếu /* A ∩ e */ P /* B */ (1)

Nếu /* A ∩ !e */ Q /* B */ (2)

Thì /* A */ if (e) P; else Q; đều thu được dữ liệu đầu ra có tính chất /* B */ !e = phủ định của e

13

Dạng khuyết:

if (e) P;

Nếu /* A ∩ e */ P; /* B */ (1)

Và /* A ∩ !e */ → /* B */ (2)

Thì /* A */ if(e) P; /* B */

2.5.2. Kỹ thuật chứng minh

Để chứng minh được cấu trúc rẽ nhánh thu được dữ liệu đầu ra có tính chất

1. thì ta phải chứng minh hai mệnh đề ở (1) và (2) đồng thời. Kết hợp các phương

pháp chứng minh toán học và phương pháp lần ngược để chứng minh.

2.5.3. Ví dụ minh họa

Ví dụ 1:

Chứng minh đoạn chương trình Java với đầu vào là 2 số nguyên x, y,

trong đó x < y. Sau khi thực hiện chương trình cho ra kết quả là một mảng số nguyên có 2 phần từ x, y, có tính chất y > x + 1.

// A: x < y

if(x < -2){

• A ∩ e: x < y ∩ x < -2
• A3=A2[y/(x*x)]: x * x > 1 – x y = x * x;
• A2=B[x/(-x)]: y > 1 – x

x = -x;

} else {

• A ∩ !e: x < y ∩ x >= -2
• A1=B[y/(x+y+3)]: x + y + 3 > x + 1 ^ y > -2 y = x + y + 3;

14

}

// B: y > x + 1

Đặt B: y > x + 1, cần chứng minh:

1. A e → A3

Ta có A e: x < y ∩ x < -2

A3: x*x > 1 – x → A, theo định lí về dấu của tam thức bậc hai muốn có

x² + x – 1 > 0 ta phải có (-1-√ )/2 > x || (-1+√ )/2 < x vì x < -2 nên x < (-1-√ )/2

1. A ∩ !e → A1

Mệnh đề A ∩!e: x < y ∩ x >= -2 ↔ -2 <= x < y

Và A1: x + y + 3 > x + 1 → y > -2. Vậy A ∩ !e → A1

2.6. TIÊN ĐỀ LẶP ĐIỀU KIỆN TRƢỚC WHILE

2.6.1. Phát biểu

Cấu trúc vòng lặp while trong ngôn ngữ Java được phát biểu như sau

Mệnh đề A là bất biến của vòng lặp

while (e){ P; }

Nếu // A ∩ e

P

• A Thì // A

while (e) { P; }

• A ∩ !e

!e là phủ định của e

15

2.6.2. Kỹ thuật chứng minh

Nhiệm vụ của ta bao giờ cũng phải chỉ ra được bất biến của vòng lặp để vận dụng tiên đề lặp

1. Phải chứng minh bất biến

// A ∩ e

P (các thao tác trong vòng lặp)

• • A

1. Sau khi chứng minh xong kết quả thu được khi kết thúc vòng lặp là A ∩ !e

Giả sử A → C

Yêu cầu chứng minh:

1. Xác định bất biến A của vòng lặp

// A ∩ e

P;

// A

1. Chứng minh A → C
2. Chứng minh A ∩ !e → B

2.6.3. Ví dụ minh họa

Ví dụ 1:

Chứng minh tính đúng của chương trình Java sau:

Chương trình nhận đầu vào là hai số nguyên dương x , y . Thực hiện chương trình thu được kết quả là một mảng số nguyên với 2 phần tử x‟, y‟ mang tính chất x’ d, y’ d

// P: x d ∩ y d ∩ x, y > 0

while ( x >= y ) {

// P ∩ e: x d, y d, 0 < y <= x

16

// P1=Q[x/(x-y)]: x – y d ∩ y d ∩ 0 < y <= x x = x – y;

}

// Q: x d, y d

Từ P ta có x = a*d, y = b*d ↔ x – y = (a – b) * d Vậy P ∩ e → P1: (x – y) d ∩ y d ∩ 0 < y <= x

Đoạn chương trình cho ta biết Q: x d, y d chính là bất biến của vòng lặp

2.7. TIÊN ĐỀ LẶP ĐIỀU KIỆN SAU DO…WHILE

2.7.1. Phát biểu

Cấu trúc lặp do … while trong ngôn ngữ Java được phát biểu như sau do{

P;

}while (e);

Nếu /*A*/ P; /*B*/

Và /*B ∩ !e*/ P; /*B*/

Thì /*A*/

do { P; } while(e);

/*B ∩ e*/

2.7.2. Kỹ thuật chứng minh

Giả sử B → D

1. Chứng minh /*A*/ P; /*B*/
2. Xác định bất biến I của vòng lặp

/* B ∩ !e */ S /* B */

1. Chứng minh /* B */ → /* D */
2. Chứng minh /* B ∩ e */ → /* C */

17

2.8. TIÊN ĐỀ LẶP FOR

2.8.1. Phát biểu

Tiên đề cấu trúc lặp for trong ngôn ngữ lập trình Java được phát biểu như sau for (i = d; i <= c; i++ ) {

P;

}

Trong đó:

• • i là biến điều khiển kiểu T
  • d là giá trị ban đầu kiểu T được gán cho biến điều khiển
  • c là giá trị cuối cùng kiểu T mà biến điều khiển nhận được Biểu diễn for dưới dạng while được như sau:
• A

i = d;

// B

while(i <= c){

T;

i = i + 1;

}

• B ∩ i <= c Nếu B ∩ i <= c T;

B

Thì // B

for (i = d; i <= c; i++) { T;

}

18

// B ∩ i > c

CHƢƠNG 3

CHỨNG MINH MỘT SỐ GIẢI THUẬT

Chứng minh tính đúng đắn của thuật toán trong các chương trình máy tính truyền thống tổ chức từ đơn giản đến phức tạp được sử dụng nhiều trong các ứng dụng phần mềm áp dụng phương pháp đặt vấn đề và suy luận với hệ tiên đề Hoare.

3.1. THUẬT TOÁN EUCLID’S

Giải thuật Euclid là một giải thuật giúp tính ước số chung lớn nhất (USCLN) của hai số một cách hiệu quả. Giải thuật này đã được biết đến từ năm 300 trước Công Nguyên. Nhà toán học Hy Lạp cổ Euclid đã viết giải thuật này trong cuốn sách toán nổi tiếng Elements.

3.1.1. Ví dụ

Tính ước số chung lớn nhất của 91 và 287.

Trước hết ta lấy 287 (là số lớn hơn trong 2 số) chia cho 91:

287 = 91 * 3 + 14, trong đó 91 ∩ 14 sẽ được dùng cho vòng lặp kế tiếp Nhận xét: bất kì số nào chia hết bởi 287 và 91 cũng sẽ chia hết bởi 287 – 91

• 3 = 14. Tương tự, số chia hết bởi 91 và 14 cũng chia hết bởi 91*3 + 14 = 287. Do đó, USCLN(287,91) = USCLN(91,14). Bài toán trở thành tìm USCLN(91,14). Lặp lại quy trình trên cho đến khi phép chia không còn số dư như sau:

91 = 14 * 6 + 7, 14 ∩ 7 sẽ được dùng cho vòng lặp kế

14 = 7 * 2, không còn số dư, kết thúc và nhận 7 làm kết quả

Cuối cùng ta có: 7 = USCLN(14,7) = USCLN(91,14) = USCLN(287,91)

3.1.2. Bổ đề

Bổđề1

Giả sử a = b*q + r và a > b, với a, b, q, r là các số nguyên, ta có:

19

Bổđề2

Ký hiệu gcd(a,b) là ước chung lớn nhất của a và b

1. gcd(a,b) = gcd(b,a)
2. gcd(a,0) = a gcd(0,0) = 0
3. gcd(a,b) = gcd( a mod b, b) với b ≠ 0

3.1.3. Chƣơng trình dùng vòng lặp

Chương trình sau đây được dùng để tính giá trị ước chung lớn nhất của 2 số nguyên dương a và b, được viết với ngôn ngữ lập trình Java

public static int calcGCD( int a, int b ) {

int r;

int x = a;

int y = b;

while(y != 0) {

r = x mod y;

x = y;

y = r;

}

return x;

}

20

Viết lại chƣơng trình với các khẳng định Hoare logic

public static int calcGCD(int a, int b) {

// A: d = gcd(a,b)

int r;

int x = a;

int y = b;

// A1: d = gcd(x,y)

while (y != 0) {

// A1 ∩ e: d = gcd(x,y) ∩ y ≠ 0

// A4=A3[r/(x mod y)]: d = gcd(y, x mod y)

r = x mod y;

// A3=A2[x/y]: d = gcd(y,r)

x = y;

// A2=A1[y/r]: d = gcd(x,r)

y = r;

// A1: d = gcd(x,y)

}

// B: x = d

return x;

}

Tính đúng của chương trình cần chứng minh:

1. Chứng minh A1 là bất biến: A1 => A4

Dựa vào tính chất 3 của bổ đề 2 ta suy ra d = gcd(x,y) = gcd(x mod y, y) Dựa vào tính chất 1 của bổ đề 1 ta suy ra d = gcd(x mod y, y) = gcd(y, x mod y)

Vậy A1 => A4 điều phải chứng minh

1. Chứng minh A1 ∩ !e => B

21

Ta có A1 ∩ !e: d = gcd(x,y) ∩ y = 0 → d = gcd(x,0)

Dựa vào tính chất 2 của bổ đề 2 ta có d = gcd(x,0) = x → B

1. Chứng minh A => A1

Dựa vào biến đổi lần ngược hiển nhiên ta chứng minh được A => A1

3.1.4. Bảng kết quả thực nghiệm tính toán

Nếu x < y thì ( x mod y ) = x

Với x = 56, y = 77 giải thuật trải qua các bước như sau

Bảng 3.4. Bảng minh họa các bước giải trong giải thuật Euclid’s

Khi nào y = 0 thì dừng vòng lặp, kết quả thu được là x.

3.2. BÀI TOÁN TÔ MÀU CỜ HÀ LAN

3.2.1. Ý tƣởng

Cho mảng a[0…N – 1] mỗi phần tử trong mảng thuộc 1 trong 2 tính chất hoặc ĐỎ hoặc XANH. Cần sắp xếp lại các phần tử trong mảng a sao cho tất cả những phần tử ĐỎ được sắp đứng trước các phần tử XANH

3.2.2. Thuật toán

Chọn vị trí k là biên giữa vùng ĐỎ và XANH

0 k

N

22

Vùng ĐỎ

Vùng XANH

Đặt R: e a[0…k – 1] là ĐỎ x a[k…N – 1] là XANH

Để biểu thức R rõ ràng hơn và được sử dụng là mệnh đề bất biến của vòng lặp, R được viết lại như sau Inv:

e a[0…k – 1] là ĐỎ x a[k…m – 1] là XANH m = N

Trong đó mọi phần tử thỏa mãn Inv cũng thỏa mãn R

Sử dụng biểu thức B: m != N như điều kiện của vòng lặp. Khi đó mệnh đề

bất biến của vòng lặp là Inv: e a[0…k – 1] là ĐỎ x a[k…m – 1] là

XANH

3.2.3. Chƣơng trình và chứng minh tính đúng

int m = 0, k = 0; // khởi tạo k và m

// Inv: e a[0…k – 1] là ĐỎ x a[k…m – 1] là XANH

while (m != N) {

// Inv & B: e a[0…k – 1] là ĐỎ x a[k…m – 1] là XANH m != N

if ( a[m] == „X‟) {

// Q2: e a[0…k – 1] là ĐỎ x a[k…m – 1] là XANH

m != N a[m] là XANH

}

else { // a[m] là ĐỎ

// D1: e a[0…k – 1] là ĐỎ x a[k…m – 1] là XANH m != N a[m] là ĐỎ

// Giả định rằng tồn tại một phương thức hoán đổi giá trị a[k] và

a[m]

swap( a, k, m);

23

// Inv2: e a[0…k] là ĐỎ k = k + 1;

x a[k+1…m] là XANH

// Inv:

}

// Inv1: e a[0…k – 1] là ĐỎ x a[k…m + 1 – 1] là XANH

m = m + 1;

e a[0…k – 1] là ĐỎ x a[k…m – 1] là XANH

}

//Q&!B:

e a[0…k – 1] là ĐỎ

x a[k…m – 1] là XANH

m = N

3.2.4. Bảng kết quả thực nghiệm

Với a = [Đ, X, X, Đ, Đ, X, Đ, X]

Bảng 3.6. Bảng kết quả thực nghiệm

Sau khi thực hiện thuật toán cho kết quả mảng a = [Đ,Đ,Đ,Đ,X,X,X,X]

24

KẾT LUẬN & PHÁT TRIỂN ĐỀ TÀI

Kết luận:

Chứng minh tính đúng đắn của chương trình bằng phương pháp hình thức đã góp phần rất quan trọng cho công nghệ phần mềm trong đó có nhiều tiến bộ trong sự hiểu biết về ngôn ngữ lập trình, những nguyên tắc, và các phương pháp có nguồn gốc chính thức. Ngoài phạm vi cho các ứng dụng thực tế của chương trình bằng chứng là ngày càng tăng và các phương pháp tiếp cận chương trình chính thức để xác định tầm quan trọng của nó ngày càng tăng.

Chứng minh tính đúng của chương trình đã đưa ra được cái nhìn đúng về hoạt động, hành vi của chương trình máy tính.

Tầm quan trọng của một chương trình hoàn toàn đúng, sẽ dẫn đến kết quả các thử nghiệm sẽ thành công.

Chứng minh tính đúng đắn cũng cung cấp một cơ hội tốt để chứng minh tầm quan trọng của toán học, đặc biệt là đối với tin học.

Những vấn đề cần thiết để chúng ta làm quen với phương pháp tiếp cận để chứng minh tính đúng của một chương trình là:

1. Mối liên hệ giữa các khẳng định đầu vào Input và đầu ra Output
2. Sự kết nối hợp lý, phủ định, quy tắc của suy luận, phương pháp chứng minh chính thức, chứng minh bất biến của vòng lặp bằng quy nạp theo số lần lặp
3. Nhìn nhận được chiến lược giải quyết vấn đề
4. Tìm hiểu phương pháp “lần ngược” vấn đề. Với một bộ các tiên đề và các quy tắc suy luận ta có thể xây dựng các bước chứng minh đi từ kết luận ngược đến tiên đề.
5. Chứng minh từng phần đúng trong chương trình

Chương trình đúng đắn của một giải thuật có thể được chứng minh là chính xác bằng phương pháp sử dụng các tiên đề và suy luận toán học hình thức.

25

Hƣớng phát triển:

• Bộ tiên đề và các quy tắc suy luận được sử dụng để chứng minh chương trình không bị ràng buộc bởi một ngôn ngữ lập trình cụ thể, chính vì vậy có thể phát triển áp dụng cho bất kì ngôn ngữ lập trình tuần tự nào mong muốn.
• Là nền tảng phát triển hệ thống phân tích và chứng minh tính đúng của chương trình máy tính thông qua khả năng tạo các mệnh đề khẳng định logic tự động.

LIỆN HỆ:

SĐT+ZALO: 0935568275

E:\DỮ LIỆU COP CỦA CHỊ YẾN\LUAN VAN DUY TAN\LUAN VAN DUY TAN\TRAN DUC HANH\New folder