Anh ấy đang đề cập đến định lý ngữ.
Không có gì ngăn cản cộng đồng nguồn mở hoặc thương mại thực hiện riêng của họ. Các lớp Hợp đồng là một phần của BCL và dễ dàng để thêm vào, ví dụ như Mono. "Chúng tôi sẽ" cần phải làm một định lý prover nếu chúng ta muốn kiểm tra tĩnh mọi thứ.
Trình giải thích không phải là một phần của trình biên dịch. Về cơ bản nó chạy như sau:
- Biên dịch phiên bản nhị phân với
CONTRACTS_FULL được xác định. Điều này phát ra tất cả các thuộc tính của Hợp đồng và gọi tới các phương thức tĩnh lớp học Contract.
- Tải lắp ráp "chỉ để phản chiếu" và phân tích cú pháp tất cả mã byte của phương thức. Phân tích lưu lượng chi tiết với thông tin tiểu bang sẽ cho phép một số hợp đồng nhất định được hiển thị "luôn đúng". Một số sẽ được "biết sai tại một số điểm." Những người khác sẽ "không thể chứng minh tĩnh hợp đồng."
Khi công cụ trở nên tốt hơn, nó sẽ đi từ việc đưa ra cảnh báo về mọi hợp đồng để cung cấp kết quả chứng minh tương tự cho phiên bản Microsoft.
Chỉnh sửa: Man, nếu Reflector được mở nguồn, nó sẽ là tuyệt vời cho việc này. Việc triển khai lần đầu tiên có thể hoạt động như một plugin. Bằng cách đó, logic prover có thể được thiết kế mà không phải lo lắng về cách các tệp nhị phân được tải. Một khi nó chứng minh chức năng (có được nó?), Logic có thể được trích xuất và xây dựng để hoạt động trên các cây cú pháp được tạo ra bởi một bộ tải lắp ráp khác (một trong đó là mã nguồn mở). Điều quan trọng/mới lạ ở đây là logic prover - bộ nạp lắp ráp đã được thực hiện nhiều lần và không có gì thay đổi ngoạn mục cho việc sử dụng này.
Nguồn
2009-07-23 06:34:23
gendarme đã có cơ sở hạ tầng đáng kể để tải hội đồng và phân tích cú pháp bytecode: http://www.mono-project.com/Gendarme –