Sử dụng phương pháp làm mịn dần để giải bài toán sau: Cho trước số tự nhiên không âm n, viết chương trình kiểm tra xem số n có phải là số nguyên tố hay không? Chương trình cần thông báo "CÓ" nếu n là số nguyên tế, ngược lại thông báo "KHÔNG".

Phát biểu trên là đúng. Khi thiết kế chương trình, việc đầu tiên là hiểu rõ yêu cầu chung của bài toán, xác định đầu vào và đầu ra của bài toán. Việc này giúp định hướng rõ ràng cho quá trình thiết kế, đảm bảo rằng chương trình được xây dựng đúng theo yêu cầu của bài toán và đáp ứng được các yêu cầu của người dùng. Sau đó, mới đi vào chi tiết thiết kế chương trình, bao gồm việc lựa chọn thuật toán, cấu trúc dữ liệu, giao diện người dùng, kiểm tra lỗi, v.v. Việc đúng đắn từ đầu sẽ giúp tiết kiệm thời gian và nguồn lực trong quá trình phát triển chương trình.

Để chứng minh tính đúng đắn của thuật toán sắp xếp chèn với các lệnh thay đổi trên, ta cần chứng minh hai điều kiện sau đây:

Điều kiện ban đầu (trước khi bắt đầu vòng lặp): Sau khi thực hiện lệnh j = 1, giá trị của j đang là 1, và dãy con A[0] chỉ gồm một phần tử là A[0] (vì j-1 là 0). Do đó, dãy con này đã được sắp xếp đúng.

Điều kiện duy trì (trong quá trình vòng lặp): Trong mỗi vòng lặp của while, nếu A[j] < A[j-1], ta hoán đổi giá trị của A[j] và A[j-1] bằng lệnh Đổi chỗ A[j] và A[j-1]. Sau đó, ta giảm giá trị của j đi 1 đơn vị bằng lệnh j = j - 1. Lúc này, giá trị của A[j] là giá trị của A[j-1] trước khi hoán đổi, và giá trị của A[j-1] là giá trị của A[j] trước khi hoán đổi. Điều này đồng nghĩa với việc dãy con A[0], A[1], ..., A[j-1] đã được sắp xếp đúng sau mỗi vòng lặp.

Vậy nên, dãy con A[0], A[1], ..., A[j-1] luôn được sắp xếp đúng sau mỗi vòng lặp của while, và dãy con này sẽ không bị thay đổi giá trị trong quá trình hoán đổi. Do đó, tính đúng đắn của thuật toán sắp xếp chèn vẫn được duy trì sau khi thay toàn bộ phần chèn A[i] vào vị trí đúng của dãy con A[0], A[1], ..., A[i-1] bằng các lệnh trên.