Làm thế nào để tạo ra độ bao phủ mã tốt của logic dấu chấm động?

Question

Tôi đang tạo thủ công mã mới. Tôi muốn chắc chắn rằng tôi không để đá nào bị lật đổ.

Có bất kỳ điều gì cụ thể mà tôi có thể làm ngoài việc chỉ định Hợp đồng mã để hướng dẫn Pex để nó tạo ra mức độ phù hợp tốt trong mã số lượng lớn không?

Hãy thử tìm kiếm http://research.microsoft.com/en-us/projects/pex/pexconcepts.pdf cho từ khóa 'float' để biết một số thông tin cơ bản.

hạn chế số học qua số dấu chấm động được xấp xỉ bằng một bản dịch để số hữu tỉ, và kỹ thuật tìm kiếm heuristic được sử dụng bên ngoài của Z3 để tìm giải pháp gần đúng cho những hạn chế dấu chấm động.

... và cũng ...

Lý tượng trưng. Pex sử dụng trình giải quyết ràng buộc tự động để xác định các giá trị nào có liên quan cho thử nghiệm và mã đang được thử nghiệm. Tuy nhiên, khả năng của người giải quyết hạn chế là, và sẽ luôn bị hạn chế. Đặc biệt, Z3 không thể lý giải chính xác về số học dấu phẩy động.

Ngoài ra, bạn có biết một công cụ trong .NET phù hợp hơn với nhiệm vụ tìm bất thường số dưới .NET không? Tôi biết về http://fscheck.codeplex.com/ nhưng nó không thực hiện lý luận tượng trưng.

Answer 1

Là những gì bạn muốn bảo hiểm tốt? Chỉ cần có một bài kiểm tra chạy mọi nhánh trong một đoạn mã là không thực sự có nghĩa là nó đúng - thường là nhiều hơn về các trường hợp góc và bạn là nhà phát triển được đặt tốt nhất để biết những trường hợp góc này là gì. Nó cũng có vẻ như nó hoạt động bằng cách chỉ nói 'đây là một kết hợp đầu vào thú vị' trong khi nhiều hơn những gì bạn muốn là xác định hành vi của hệ thống bạn muốn xem - nếu bạn đã viết mã sai ở nơi đầu tiên thì thú vị đầu vào có thể hoàn toàn không liên quan đến mã đúng.

Có lẽ đây không phải là câu trả lời bạn đang tìm kiếm nhưng tôi muốn nói cách tốt nhất để làm điều này là bằng tay! Viết ra một spec trước khi bạn bắt đầu viết mã và biến nó thành một tải các trường hợp kiểm tra khi bạn biết/khi bạn đang viết API cho lớp/hệ thống con của bạn.

Khi bắt đầu điền API/viết mã, bạn có thể nhận thêm các bit và phần mà bạn cần thực hiện + tìm ra các bit khó - nếu bạn có điều kiện, v.v ... một người nào đó tái cấu trúc mã của bạn có thể bị sai, sau đó viết một trường hợp thử nghiệm bao gồm chúng. Đôi khi tôi cố ý viết mã sai tại những điểm này, nhận được một thử nghiệm trong đó không thành công và sau đó sửa nó chỉ để đảm bảo rằng thử nghiệm đang kiểm tra đường dẫn chính xác thông qua mã. Sau đó thử và nghĩ về bất kỳ giá trị kỳ lạ nào mà bạn có thể không có - đầu vào tiêu cực, null, vv Thường thì đây là trường hợp không hợp lệ và bạn không muốn phục vụ/phải suy nghĩ - trong những trường hợp này, tôi sẽ thường viết một số bài kiểm tra để nói rằng họ nên ném ngoại lệ - về cơ bản dừng mọi người lạm dụng mã trong trường hợp bạn chưa biết đúng/với dữ liệu không hợp lệ.

Bạn đã đề cập ở trên rằng bạn đang làm việc với mã số lượng lớn - có thể đáng thử nghiệm ở mức trên để bạn có thể kiểm tra hành vi trong hệ thống mà bạn đang tìm kiếm thay vì chỉ số crunching - giả sử mã hoàn toàn bằng số này sẽ giúp bạn thiết lập một số điều kiện thực thi và cũng đảm bảo rằng bất kỳ số bit nào đang thực sự tương tác với phần còn lại của chương trình theo cách bạn cần - nếu đó là thuật toán nào đó bạn có thể sẽ tốt hơn viết một ngôn ngữ thử nghiệm chấp nhận để giúp mô tả các đầu ra mong muốn trong các tình huống khác nhau - điều này cho thấy một bức tranh rõ ràng về những gì bạn đang cố gắng đạt được, nó cũng cho phép bạn ném một lượng lớn dữ liệu (thực) qua một hệ thống. so với đầu vào được tạo bởi máy tính. Lợi ích khác của việc này là nếu bạn nhận ra thuật toán cần viết lại mạnh mẽ để đáp ứng một số yêu cầu mới thì tất cả những gì bạn phải làm là thêm trường hợp thử nghiệm mới và sau đó viết lại/refactor; nếu các xét nghiệm của bạn chỉ xem xét các chi tiết của thuật toán và giả sử các hiệu ứng trên thế giới bên ngoài thì bạn sẽ có một cơn đau đầu đáng kể để tìm hiểu cách thuật toán hiện hành ảnh hưởng đến hành vi như thế nào. di chuyển một tải các bài kiểm tra đơn vị vào một API/thuật toán mới.