Có thể viết trình xác minh để kiểm tra xem một chương trình cụ thể có triển khai một thuật toán cụ thể không?

Question

Với một chương trình P, được viết bằng C++, tôi có thể viết một thuật toán tìm thấy nếu chương trình P thực hiện một thuật toán cụ thể không? Có bất kỳ thuật toán nào giải quyết được vấn đề này không. Vấn đề này có thể giải quyết được không?

Ví dụ tôi yêu cầu một người thực hiện thuật toán sắp xếp nhanh và bây giờ nếu tôi muốn đảm bảo rằng người đó thực sự đã triển khai thuật toán sắp xếp nhanh. Người đó có thể thực sự thực hiện một số thuật toán phân loại khác và nó sẽ tạo ra đầu ra chính xác và vượt qua tất cả testcases (thử nghiệm hộp đen). Một cách tôi có thể làm điều này là nhìn vào mã nguồn. Tôi muốn tránh nỗ lực thủ công này và muốn viết một chương trình có thể thực hiện công việc này. Câu hỏi đặt ra là "Có thể không?".

Answer 1

Từ Rice's Theorem, bạn thậm chí không thể quyết định chung xem một đoạn mã có phải là chức năng sắp xếp hay không bằng cách kiểm tra mã. Bạn có thể, tất nhiên, tìm hiểu xem nó có tác dụng sắp xếp cho một số tập hợp các đầu vào hữu hạn hay không bằng cách chạy nó với các đầu vào đó và kiểm tra kết quả.

Bạn có thể làm điều gì đó cho trường hợp cụ thể của thuật toán sắp xếp đích, bằng cách kiểm tra mảng đang được sắp xếp trong sắp xếp, kiểm tra các bất biến là đặc trưng của thuật toán đích. Ví dụ, mỗi cuộc gọi trong một triển khai sắp xếp nhanh chóng đệ quy sẽ dẫn đến một subarray trở thành sắp xếp.

============================================== ===================

Theo dõi từ nhận xét, tôi đề nghị xem Ahmad Taherkhani's home page. Ông đã tiếp tục nghiên cứu trong lĩnh vực này, bao gồm một bài báo năm 2012 về chủ đề này.

Answer 2

Tôi đã suy nghĩ và vẫn nghĩ về kiểm tra stack/heap (cho bạn thử nghiệm dựa trên các giải pháp được tối ưu hóa).
Bạn có thể kiểm tra độ phức tạp về thời gian và độ phức tạp của bộ nhớ tổng thể sẽ thu hẹp kết quả. ngay cả đối với Time: O (n lg n) để kết hợp và sắp xếp nhanh chóng. bạn có thể phân biệt chúng với việc cấp phát bộ nhớ vì chúng là N, Lg (n) theo thứ tự.
bạn cũng có thể kiểm tra những thứ như nhiễu loạn mảng ban đầu..có nhưng đây không phải là trọng lượng quyết định.