TAILIEUCHUNG - Bài giảng Đặc tả hình thức: Chương 11 - Nguyễn Thị Minh Tuyền

Nội dung của Bài giảng Đặc tả hình thức Chương 11 được trình bày như sau: Cấu trúc của ESC/Java2, chạy ESC/Java2, Platform được hỗ trợ, ứng dụng dựa vào môi trường có, các tùy chọn dòng lệnh, Các file đặc tả,.! | LOGO Đặc tả hình thức Giới thiệu về ESC/Java2 Cách sử dụng và thuộc tính Nguyễn Thị Minh Tuyền Nội dung slide này được dịch từ các slide của David Cok, Joe Kiniry, Eric Poll 1 v  ESC/Java §   Extended Static Checker for Java Nguyễn Thị Minh Tuyền 2 Đặc tả hình thức Cấu trúc của ESC/Java2 v  ESC/Java2 gồm §   Một pha kiểm tra cú pháp §   Một pha typechecking (kiểm tra loại và cách sử dụng) §   Một pha kiểm tra tĩnh ( diễn giải để tìm ra các lỗi tìm tàng) – chạy một prover behind-the-scenes gọi là Simplify. v  Kiểm tra cú pháp và typechecking tạo ra các cảnh báo hoặc lỗi. v  Kiểm tra tĩnh đưa ra các cảnh báo. Nguyễn Thị Minh Tuyền 3 Đặc tả hình thức Chạy ESC/Java2 v  Tải ESC/Java2 từ §   ESCJava2/ v  Sử dụng ESC/Java2: §   Chạy công cụ bằng lệnh. §   Sử dụng Eclipse plug-in. §   Hướng dẫn cài đặt: ESCJava2/ Nguyễn Thị Minh Tuyền 4 Đặc tả hình thức Platform được hỗ trợ v  ESC/Java2 được hỗ trợ trên §   Linux §   MacOSX §   Cygwin on Windows §   Windows (nhưng vẫn còn một số vấn đề về môi trường cần được giải quyết) §   Solaris Nguyễn Thị Minh Tuyền 5 Đặc tả hình .

• Kỹ thuật lập trình
• Bài giảng Đặc tả hình thức
• Đặc tả hình thức
• Giới thiệu về ESC Java2
• Cách sử dụng và thuộc tính
• Cấu trúc của ESC
• Các file đặc tả
• Đặc tả hàm
• Đặc tả đệ quy
• Đặc tả hàm tường minh
• Đặc tả hàm không tường minh
• Lập trình phần mềm
• Công nghệ phần mềm
• Đặc tả phần mềm
• Ngôn ngữ đặc tả hình thức
• Đặc tả yêu cầu phần mềm
• Bài giảng Đặc tả yêu cầu phần mềm
• Công nghệ phần mềm nâng cao
• Phân loại đặc tả yêu cầu phần mềm
• Đặc tả phi hình thức phần mềm
• Đặc tả hình thức phần mềm
• Mô hình Thế giới thực
• Quy trình công nghệ phần mềm
• Ngôn ngữ hình thức
• Thiết kế ở mức cao
• Đặc tả ở mức mã nguồn
• JML nâng cao
• Từ khóa chính trong JML
• Các tính năng nâng cao
• Đặc tả các ngoại lệ
• Thừa kế đặc tả
• Các trường model
• Đặc tả không hình thức
• Phép toán vị từ
• Cơ sở đặc tả hình thức
• Luật suy diễn
• Cơ sở toán học trong đặc tả hình thức
• Hệ thống phần mềm
• Lỗi phần mềm
• Ngôn ngữ và hệ thống
• Các ngôn ngữ đặc tả
• Kiểm tra mô hình
• Mô hình hóa dữ liệu
• Kiểu dữ liệu
• Đặc tả operation
• Dữ liệu kiểu mảng
• Kiểu đối tượng phức
• Kiểu tập hợp
• Design by contract
• Ngôn ngữ đặc tả
• Công cụ hỗ trợ
• Thủ thuật và cạm bẫy
• Đặc tả thừa kế
• Đặc tả sử dụng ánh xạ
• Kiểu ánh xạ
• Ngôn ngữ đặc tả Z
• Phép toán trên giản đồ