Claude Skill MartKhám phá skillCâu dùng ngayHọc qua videoDùng terminalSkill là gì?
 
← Về danh sách

Trình sinh bất biến bằng diễn giải trừu tượng

Suy luận loop invariant, tiền điều kiện và hậu điều kiện bằng abstract interpretation rồi xuất ra cú pháp Dafny, Isabelle, Coq, ACSL.

Lập trìnhNâng cao★ 143⑂ 14Điểm AI 7/10Cập nhật lần cuối: 22 thg 2, 2026

Kỹ năng này làm gì

  • Xác định các điểm cần đặc tả trong code: vòng lặp, biên hàm, các assert.
  • Dùng phân tích khoảng (interval), quan hệ (relational) và hình dạng (shape) để suy ra miền giá trị biến, quan hệ giữa các biến và tính chất cấu trúc dữ liệu.
  • Sinh loop invariant thỏa cả ba điều kiện khởi tạo – duy trì – kết thúc, theo mẫu vòng lặp đếm, tích lũy, tìm kiếm.
  • Đề xuất tiền điều kiện (chỉ số trong biên, chia khác 0, con trỏ không null) và hậu điều kiện (đã sắp xếp, bảo toàn multiset, kết quả tìm kiếm).
  • Xuất kết quả sẵn dùng cho Dafny, Isabelle/HOL, Coq và ACSL cho C.
  • Kèm kỹ thuật tăng cường invariant yếu, xử lý vòng lặp lồng và nhiều điều kiện thoát.

Phù hợp với ai

  • Kỹ sư/nghiên cứu viên làm kiểm chứng hình thức với Dafny, Coq, Isabelle, Frama-C.
  • Lập trình viên hệ thống safety-critical (nhúng, hàng không, tài chính) cần thêm contract cho hàm.
  • Sinh viên cao học và giảng viên dạy chứng minh tính đúng đắn của thuật toán.

Ví dụ sử dụng

  1. Dán hàm insertion sort viết bằng Python và yêu cầu chuyển sang Dafny → nhận method kèm invariant cho cả vòng ngoài lẫn vòng trong và điều kiện bảo toàn multiset.
  2. Sinh chú thích ACSL (requires \valid(...), loop invariant, loop variant) cho hàm C find_max để chạy kiểm chứng bằng Frama-C.
  3. Khi trình kiểm chứng báo invariant quá yếu, áp dụng phần "strengthening" để thêm tính chất về phần dữ liệu đã xử lý và vượt qua chứng minh.

· · · Hướng dẫn cài đặt · · ·

Dùng thử ngay, không cần cài

Dán đoạn dưới vào Claude là dùng được skill này mà không cần cài đặt.

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-invariant-generator/SKILL.md

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

Nếu Claude không mở được liên kết, hãy mở liên kết và copy nội dung vào rồi dán.

↓ Thấy hữu ích thì tải ZIP bên dưới và cài. Sau đó skill tự chạy, không phải dán lại mỗi lần.

Cài vào ứng dụng Claude (không cần terminal)
  1. Tải tệp ZIP bằng nút bên dưới.
  2. Trong Claude, mở Settings → Capabilities và bật 'Code execution and file creation'. (chỉ một lần)
  3. Vào Customize → Skills → + → 'Upload a skill' rồi tải tệp ZIP lên.
↓ Tải ZIP
Cài vào Claude Code

Để Claude làm — dán câu dưới đây vào Claude Code

Hãy cài skill mình tìm thấy trên Claude Skill Mart.
Copy thư mục skills/abstract-invariant-generator từ repo GitHub ArabelaTso/Skills-4-SE vào ~/.claude/skills/abstract-invariant-generator/ 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.

Cài bằng lệnh thủ công

git clone https://github.com/ArabelaTso/Skills-4-SE.git && mkdir -p ~/.claude/skills && cp -r Skills-4-SE/skills/abstract-invariant-generator ~/.claude/skills/

⚠ Đây là skill do người khác tạo. Hãy kiểm tra repo gốc trước khi cài.

  1. Mở terminal và clone repo: git clone https://github.com/ArabelaTso/Skills-4-SE.git
  2. Tạo thư mục skills nếu chưa có: mkdir -p ~/.claude/skills
  3. Sao chép riêng kỹ năng này: cp -r Skills-4-SE/skills/abstract-invariant-generator ~/.claude/skills/
  4. Kiểm tra bằng ls ~/.claude/skills/abstract-invariant-generator xem đã có SKILL.md (và thư mục references).
  5. Khởi động lại Claude Code, rồi thử câu lệnh: "Sinh loop invariant Dafny cho hàm này".
  6. Muốn kiểm chứng thật, hãy cài thêm công cụ đích (Dafny, Coq, Isabelle, Frama-C) và chạy lại đặc tả được sinh ra.
Xem mã nguồn trên GitHub ↗Giấy phép: Apache-2.0