Làm thế nào để các lập trình viên kiểm tra thuật toán của họ trong TopCoder hoặc các cuộc thi khác?

Question

Những người lập trình giỏi viết chương trình từ trung bình đến cao hơn trong các cuộc thi của TopCoder hoặc ACM ICPC, phải đảm bảo tính đúng đắn của thuật toán trước khi gửi.

Mặc dù chúng được cung cấp một số trường hợp thử nghiệm mẫu để đảm bảo đầu ra chính xác, nhưng làm cách nào để đảm bảo rằng chương trình sẽ hoạt động chính xác? Họ có thể viết một số trường hợp thử nghiệm của riêng mình nhưng nó sẽ không thể có trong mọi trường hợp để biết câu trả lời đúng thông qua tính toán thủ công. Họ làm nó như thế nào?

Cập nhật: Như có vẻ như, nó không phải là hoàn toàn có thể để phân tích và đảm bảo kết quả của một thuật toán cho các ràng buộc chặt chẽ của một môi trường cạnh tranh. Tuy nhiên, nếu có bất kỳ hướng dẫn sử dụng, các đặc điểm phổ biến hơn được áp dụng trong khi giải quyết các vấn đề như vậy - phải đủ để trả lời câu hỏi. Một cái gì đó giống như các phương pháp hay nhất ..

Answer 1

Trong các cuộc thi, các lập trình viên hàng đầu có đủ kinh nghiệm để đọc câu hỏi và nghĩ về một số trường hợp thử nghiệm sẽ nắm bắt hầu hết các khả năng nhập liệu.
Nó bắt hầu hết các lỗi thường - nhưng không an toàn 100%.

Tuy nhiên, trong các ứng dụng quan trọng trong cuộc sống thực (các hệ thống quan trọng trên máy bay hoặc lò phản ứng hạt nhân chẳng hạn) có các phương pháp PROVE một số đoạn mã sẽ thực hiện những gì.

Đây là lĩnh vực formal verification - quá phức tạp và tốn thời gian để thực hiện trong cuộc thi, nhưng đối với một số hệ thống, nó được sử dụng vì không thể dung thứ được sai lầm.

---

Một số thông tin bổ sung:
xác minh chính thức về cơ bản bao gồm 2 phần:

1. xác minh Manual - ở đây chúng tôi sử dụng hệ thống chứng minh như Hoare logic và tự chứng minh chương trình làm những gì chúng ta muốn nó phải làm.
2. Tự động model checking - mô hình hóa sự cố là máy trạng thái và sử dụng công cụ Kiểm tra mô hình để xác minh rằng mô-đun thực hiện nhiệm vụ (hoặc không làm điều gì đó "xấu").
   Chỉ định "việc cần làm" thường được thực hiện với temporal logic.
   Điều này thường được sử dụng để xác minh tính chính xác của mô hình phần cứng. Ví dụ Intel sử dụng nó để đảm bảo rằng họ sẽ không nhận được floating point bug nữa.

Answer 2

Có yếu tố thời gian với Bộ mã hóa hàng đầu, do đó không thể kiểm tra mọi kết hợp trong giới hạn đó. Họ có thể làm tốt nhất họ có thể và dựa vào kinh nghiệm cho phần còn lại, giống như người ta làm trong đời thực. Tôi không biết rằng nó có thể đảm bảo rằng một đoạn mã quan trọng là lỗi miễn phí mãi mãi.

Answer 3

Hình ảnh này, hãy tưởng tượng bạn là một lập trình viên hàng đầu.Đọc bạn biết một loạt thuật toán và không nghĩ suy nghĩ hai lần khi triển khai chúng. Bạn biết cách sửa đổi thuật toán đã biết để phù hợp với nhu cầu của vấn đề.Bạn mạnh mẽ với ước tính thời gian và độ phức tạp và bạn mong đợi rằng trong trường hợp xấu nhất thuật toán được thiết kế của bạn sẽ chạy trong thời gian và hạn chế về bộ nhớ.
Ở cấp độ này, bạn chỉ cần suy nghĩ và sử dụng bàn phím trong khoảng từ 5 đến 10 phút và có thuật toán siêu rõ ràng trước khi bắt đầu viết mã.Một khi bạn hoàn thành mã hóa, bạn nhấn biên dịch và thường không có lỗi biên dịch.Bởi vì mã này rất trực quan với bạn. Sau đó dựa trên thuật toán được sử dụng và cấu trúc dữ liệu được sử dụng, bạn mong đợi rằng có thể có một trong các vấn đề sau.

1. một trường hợp góc
2. một vấn đề tràn

Một trường hợp góc là cơ bản giống như bạn đã mã hóa cho trường hợp tổng quát, tuy nhiên khi nói N = 1, câu trả lời là khác nhau từ others.So bạn thường viết nó như là một trường hợp đặc biệt. Lỗi tràn là khi các giá trị trung gian hoặc kết quả tràn quá giới hạn của loại dữ liệu.

Bạn lưu ý mọi vấn đề phát sinh tại thời điểm này và sử dụng dữ liệu này trong giai đoạn Thử thách (như trong TopCoder).
Sau khi bạn đã kiểm tra hai loại này, bạn nhấn Submit.