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

Trợ lý chú thích ACSL

Kỹ năng sinh chú thích đặc tả hình thức ACSL (hợp đồng hàm, bất biến vòng lặp, an toàn bộ nhớ) cho mã C/C++ để kiểm chứng bằng Frama-C.

Lập trìnhNâng cao★ 248⑂ 23Điểm AI 7/10Cập nhật lần cuối: 21 thg 8, 2026

Làm được gì

  • Viết hợp đồng hàm ACSL với requires/ensures/assigns cho hàm C/C++.
  • Sinh bất biến vòng lặp, biểu thức giảm dần (loop variant) chứng minh dừng, và loop assigns.
  • Thêm đặc tả an toàn bộ nhớ: \valid, \valid_read, \separated, kiểm tra con trỏ null, tràn số.
  • Định nghĩa predicate và khối axiomatic tái sử dụng, chèn assert/assume trung gian.
  • Theo quy trình 5 bước: phân tích hàm → hợp đồng → vòng lặp → khẳng định → predicate phụ trợ.
  • Kèm thư mục references/ gồm tham chiếu cú pháp ACSL, mẫu thường dùng và mẹo tích hợp Frama-C.

Phù hợp với ai

  • Kỹ sư, nhà nghiên cứu dùng plugin WP của Frama-C để kiểm chứng mã C.
  • Nhóm làm phần mềm nhúng độ tin cậy cao (hàng không, ô tô, thiết bị y tế).
  • Người muốn chứng minh không tràn mảng, không con trỏ null ở mức toán học.
  • Sinh viên, học viên môn kiểm chứng hình thức cần soạn đặc tả nhanh.

Ví dụ sử dụng

  1. "Thêm hợp đồng ACSL và bất biến vòng lặp cho hàm find_max_index" → sinh hậu điều kiện mô tả tính chất phần tử lớn nhất.
  2. "Viết đặc tả an toàn bộ nhớ cho hàm bọc memcpy" → sinh \valid, \valid_read, \separated và assigns.
  3. "Tách trường hợp n <= 0 và n > 0 thành các behavior" → sinh đặc tả có complete behaviors; disjoint behaviors;.

· · · 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/acsl-annotation-assistant/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/acsl-annotation-assistant từ repo GitHub ArabelaTso/Skills-4-SE vào ~/.claude/skills/acsl-annotation-assistant/ 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 /tmp/skills-4-se && mkdir -p ~/.claude/skills && cp -r /tmp/skills-4-se/skills/acsl-annotation-assistant ~/.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à tải repo: git clone https://github.com/ArabelaTso/Skills-4-SE.git
  2. Tạo thư mục kỹ năng nếu chưa có: mkdir -p ~/.claude/skills
  3. Sao chép đúng kỹ năng này: cp -r Skills-4-SE/skills/acsl-annotation-assistant ~/.claude/skills/
  4. Kiểm tra bằng ls ~/.claude/skills/acsl-annotation-assistant để thấy SKILL.md và references/.
  5. Khởi động lại Claude Code, rồi yêu cầu ví dụ: "thêm chú thích ACSL cho hàm C này".
  6. (Khuyến nghị) Cài Frama-C để kiểm chứng thật: macOS brew install frama-c, Ubuntu sudo apt install frama-c.
  7. Chạy frama-c -wp file.c để chứng minh và tinh chỉnh các mệnh đề chưa chứng minh được.
Xem mã nguồn trên GitHub ↗Giấy phép: Apache-2.0