Luận Văn Thạc Sĩ Nghiên Cứu Về Chứng Minh Tự Động (Theorem Proving) Trong Cafeobj

Nghiên Cứu Về Chứng Minh Tự Động (Theorem Proving) Trong Cafeobj​

Đặc tả và kiểm chứng hình thức là một pha quan trọng nhằm nâng cao độ tin cậy và chất lượng của phần mềm. Có thể chia đặc tả phần mềm ra làm hai loại: đặc tả phi hình thức là đặc tả dựa trên ngôn ngữ tự nhiên và đặc tả hình thức là đặc tả dựa trên kiến trúc toán học. Đặc tả phi hình thức không được chặt chẽ bằng đặc tả hình thức nhưng được nhiều người biết và có thể dùng để trao đổi với nhau để làm chính xác hóa các điểm chưa rõ, chưa thống nhất giữa các bên phát triển hệ thống. Đặc tả hình thức là đặc tả mà ở đó các từ ngữ, cú pháp, ngữ nghĩa được định nghĩa hình thức dựa vào toán học. Đặc tả hình thức có thể coi là một phần của hoạt động đặc tả phần mềm. Trong đặc tả hình thức các đặc tả yêu cầu được phân tích chi tiết, các mô tả trừu tượng của các chức năng chương trình có thể được tạo ra để làm rõ yêu cầu.

• Luận văn thạc sĩ Công nghệ thông tin
• Chuyên ngành Công nghệ phần mềm
• Người hướng dẫn khoa học: TS. Phạm Ngọc Hùng
• Tác giả: Tạ Thị Thu Hiền
• Số trang: 71
• Kiểu file: PDF
• Ngôn ngữ: Tiếng Việt
• Trường Đại học Công nghệ. Đại học Quốc gia Hà Nội 2010

Link Download
http://dlib.vnu.edu.vn/iii/cpro/DigitalItemViewPage.external?lang=vie&sp=1002838
https://drive.google.com/drive/folders/1yLBzZ1rSQoNjmWeJTM6cEZ3WGQHg04L1