Các phương pháp hình thức

Trong ngành khoa học máy tính, các phương pháp hình thức là các kỹ thuật toán học cho việc đặc tả, phát triển và kiểm định các hệ thống phần mềm và phần cứng. Cách tiếp cận này đặc biệt quan trọng đối với các hệ thống cần có tính toàn vẹn cao, chẳng hạn hệ thống điều khiển lò phản ứng hạt nhân hay điều khiển tên lửa, khi an toàn hay an ninh có vai trò quan trọng, để góp phần đảm bảo rằng quá trình phát triển hệ thống sẽ không có lỗi. Các phương pháp hình thức đặc biệt hiệu quả tại giai đoạn đầu của quá trình phát triển (tại các mức yêu cầu và đặc tả hệ thống), nhưng cũng có thể được sử dụng cho một quá trình phát triển hoàn chỉnh của một hệ thống.

Sử dụng

Các phương pháp hình thức có thể được áp dụng tại nhiều điểm khác nhau trong cả quá trình phát triển phần mềm. (Tuy có thể nói đến một quá trình phát triển bất kỳ, để thuận tiện, ta sẽ dùng các thuật ngữ của mô hình thác nước).

Đặc tả

Các phương pháp hình thức có thể được sử dụng để mô tả về hệ thống cần phát triển, tại bất kỳ mức độ chi tiết nào mà ta muốn. Mô tả hình thức này có thể được sử dụng để hướng dẫn các hoạt động phát triển tiếp theo (xem các mục dưới); ngoài ra, nó có thể được sử dụng để kiểm định xem các yêu cầu cho hệ thống đang được phát triển đã được đặc tả một cách đầy đủ và chính xác hay chưa.
Nhu cầu về các hệ thống đặc tả hình thức đã được nói đến từ nhiều năm. Trong Báo cáo ALGOL 60, John Backus đã trình bày một hệ thống ký hiệu hình thức để mô tả cú pháp ngôn ngữ lập trình (sau này được đặc tên là Backus normal form hay Backus-Naur form (BNF) (Dạng chuẩn tắc Backus));

Kiểm định

Khi một đặc tả hình thức đã được phát triển, đặc tả này có thể được dùng làm cơ sở cho việc chứng minh các tính chất của đặc tả.

Chứng minh của con người

Đôi khi, động cơ cho việc chứng minh tính đúng đắn của một hệ thống không phải là nhu cầu đảm bảo tính đúng đắn của hệ thống mà là mong muốn hiểu rõ hơn về hệ thống. Do đó, một số chứng minh được thực hiện dưới hình thức chứng minh toán học: viết tay hoặc đánh máy nội dung bằng ngôn ngữ tự nhiên, với mức độ phi hình thức như các chứng minh toán học thông thường mà con người vẫn thực hiện. Một chứng minh "tốt" là một chứng minh mà những người khác có thể đọc được và hiểu được.
Các phê phán đối với cách tiếp cận này nói rằng tính đa nghĩa cố hữu trong ngôn ngữ tự nhiên cho phép các lỗi sai trong các chứng minh đó có thể không bị phát hiện; nhiều khi, những lỗi tinh vi có thể xuất hiện trong các chi tiết mức thấp mà thường không được để ý đến bởi những chứng minh thuộc kiểu này. Ngoài ra, việc tạo ra các chứng minh tốt đòi hỏi trình độ toán học cao.

Phê phán

Bên cạnh các phê phán nội bộ nói trên, còn có các phê phán dành cho toàn bộ ngành các phương pháp hình thức. Với tầm phát triển hiện nay, các chứng minh về tính đúng đắn, bằng tay hoặc bằng máy tính, đòi hỏi nhiều thời gian (và do đó cả tiền bạc) để được tạo ra, với lợi ích hạn chế ngoài việc đảm bảo tính đúng đắn. Điều đó làm cho các phương pháp hình thức thường chỉ được dùng trong các lĩnh vực thu được lợi ích từ việc có được các chứng minh đó, hoặc sẽ gặp nguy hiểm nếu có các lỗi không được phát hiện. Ví dụ, trong kỹ thuật hàng không, các lỗi không được phát hiện có thể gây chết chóc, do đó các phương pháp hình thức được dùng rộng rãi trong ngành này hơn trong các lĩnh vực ứng dụng khác.