Đặc tả hình thức - Đặc tả và tính đúng đắn của hàm

Phương pháp này chính là phương pháp kiểm thử chủ đạo được áp dụng trong giai đoạn lập trình và giai đoạn kiểm thử của quy trình phát triển phần mềm trên thế giới hiện nay.
Các công cụ hỗ trợ phương pháp này:
Công cụ phát sinh các dữ liệu thử nghiệm.
Công cụ cho phép thực thi hàm và ghi nhận kết quả.
Công cụ kiểm tra tính phù hợp của cài đặt hàm so với đặc tả.
Các công cụ tự động phát sinh hàm từ đặc tả, cho thực hiện hàm phát sinh và tự động kiểm tra kết quả thực hiện.

Từ khóa: Đặc tả hình thức, phát triển phần mềm, ngôn ngữ hình thức, cơ sở toán học , xây dựng hệ thống, Ngôn ngữ tự nhiên