Trình khám phá miền trừu tượng

Làm được gì

Dùng lý thuyết diễn giải trừu tượng (abstract interpretation) để phân tích tĩnh chương trình: suy ra miền giá trị của biến, quan hệ giữa các biến và bất biến vòng lặp.

• Hướng dẫn chọn miền: bảng so sánh độ chính xác/chi phí của Sign, Interval, Congruence, Octagon, Polyhedra và Reduced Product.
• Quy trình 6 bước: chọn miền → khởi tạo trạng thái trừu tượng → áp dụng hàm chuyển (gán, điều kiện, join) → widening (∇) cho vòng lặp để đảm bảo dừng → narrowing (△) để tinh chỉnh → trích xuất bất biến.
• Kiểm tra an toàn: phát hiện nguy cơ chia cho 0, truy cập mảng ngoài biên dựa trên xấp xỉ.
• Nêu rõ giới hạn: không được coi giá trị xấp xỉ là chính xác, phải nói rõ miền đã chọn không biểu diễn được gì (ví dụ octagon không biểu diễn y = 2x).

Phù hợp với ai

• Người học/nghiên cứu phân tích tĩnh, kiểm chứng hình thức, tối ưu hóa trình biên dịch.
• Lập trình viên cần lập luận rõ ràng về khoảng giá trị biến và bất biến vòng lặp khi review code.
• Sinh viên làm bài tập môn Program Analysis muốn xem từng bước tính điểm bất động.

Ví dụ sử dụng

1. Với int x=0; while(x<10){x++; y--;}, miền interval cho x ∈ [0,9] trong vòng lặp và x=10, y=90 khi thoát, đồng thời chỉ ra interval không nắm được x+y=100.
2. Với y = x*x; z = 100/y;, miền sign suy ra y ≥ 0 và cảnh báo khả năng chia cho 0 khi x = 0.
3. Với vòng lặp lồng nhau, miền octagon rút ra bất biến quan hệ j ≤ i; còn quan hệ tuyến tính phức tạp như z = 3x thì cần chuyển sang polyhedra.

Hãy đọc hướng dẫn trong tệp này và làm theo để giúp mình:
https://raw.githubusercontent.com/ArabelaTso/Skills-4-SE/HEAD/skills/abstract-domain-explorer/SKILL.md

Mình muốn: (viết việc bạn cần ở đây)

Hãy cài skill mình tìm thấy trên Claude Skill Mart.
Copy thư mục skills/abstract-domain-explorer từ repo GitHub ArabelaTso/Skills-4-SE vào ~/.claude/skills/abstract-domain-explorer/ của mình.
Sau khi cài xong, cho mình biết skill này làm được gì trong một câu.