TAILIEUCHUNG - Bài giảng Đặc tả hình thức: Chương 3 - PGS.TS. Vũ Thanh Nguyên

Bài giảng Đặc tả hình thức: Chương 3 Mô hình hóa dữ liệu kiểu tập hợp, cung cấp cho người đọc những kiến thức như: Kiểu dữ liệu trong VDM; Các tập hợp được định nghĩa sẵn; Mô hình hóa dữ liệu; Kiểu tập hợp; Mô hình hóa các operation; Đặc tả operation. Mời các bạn cùng tham khảo! | Trường Đại học Công Nghệ Thông Tin ĐHQG-HCM Khoa Công Nghệ Phần Mềm Chương 3 Mô hình hóa dữ liệu Kiểu tập hợp Giảng viên . Vũ Thanh Nguyên 1 Kiểu dữ liệu trong VDM integer values -32768 32767 operations - div mod gt Các tập hợp được định nghĩa sẵn Tập số nguyên ℤ -2 -1 0 1 2 Tập số tự nhiên ℕ 0 1 2 3 Tập số nguyên dương ℕ1 1 2 3 Tập số thực ℝ Tập số hữu tỉ ℚ Tập boolean B true false Tập ký tự gồm chữ cái hoa thường số phép toán dấu câu Char a b c d e f g h i j k l m n o p q r s t u v w x y z A B C D E F G H I J K L M N O P Q R S T U V W X Y Z 0 1 2 3 4 5 6 7 8 9 - . 3 Mô hình hóa dữ liệu Technical-Staff values PROJECT-MANAGER TEAM-LEADER ANALYST DESIGNER PROGRAMMER TESTER operations Technical-Staff PROJECT-MANAGER TEAM-LEADER ANALYST DESIGNER PROGRAMMER TESTER 4 Kiểu tập hợp Cho trước kiểu dữ liệu T Cần định nghĩa kiểu dữ liệu trong đó mỗi thể hiện là 1 tập hợp các phần tử thuộc kiểu dữ liệu T Ký hiệu T-set Ví dụ 1 Mode READ WRITE EXECUTE FileMode Mode-set FileMode READ WRITE EXECUTE READ WRITE READ EXECUTE EXECUTE WRITE READ WRITE EXECUTE Ví dụ 2 Intset ℤ-set 5 Kiểu tập hợp Ví dụ 3 Pupils Patrick Christa Emma Pete Frank Lisa Richard David Daniel John Helen Pauline Mark Mike Elisabeth School-trip Pupils-set 6 Kiểu tập hợp Câu hỏi Có thể sử dụng kiểu tập hợp cho các trường hợp nào sau đây Hành khách trên 1 chuyến xe buýt Bệnh nhân trong phòng chờ khám bệnh trong 1 buổi Thí sinh được nhận giải thưởng trong 1 kỳ thi 7 Mô hình hóa các operation Một operation có thể có hai tác dụng Thay đổi nội dung biến bên ngoài Trả về giá trị thông qua tham số kết quả Đối với các biến bên ngoài Biến được truy xuất dạng read-only rd Biến được truy xuất dạng read-write wr Không có dạng truy xuất write-only trong VDM Ví dụ ext rd size ℕ ext wr a b ℕ rd x ℤ 8 Đặc tả operation Tên_Operation thamsố1 Kiểu1 thamsố2 Kiểu2 kq Kiểukq ext wr BiếnRead_Write Kiểu rd BiếnRead_Only Kiểu pre Vị từ pre-condition post Vị từ post-condition 9 Đặc tả operation Ví dụ MULT heso ℝ ext wr x ℝ pre x lt

TỪ KHÓA LIÊN QUAN
TAILIEUCHUNG - Chia sẻ tài liệu không giới hạn
Địa chỉ : 444 Hoang Hoa Tham, Hanoi, Viet Nam
Website : tailieuchung.com
Email : tailieuchung20@gmail.com
Tailieuchung.com là thư viện tài liệu trực tuyến, nơi chia sẽ trao đổi hàng triệu tài liệu như luận văn đồ án, sách, giáo trình, đề thi.
Chúng tôi không chịu trách nhiệm liên quan đến các vấn đề bản quyền nội dung tài liệu được thành viên tự nguyện đăng tải lên, nếu phát hiện thấy tài liệu xấu hoặc tài liệu có bản quyền xin hãy email cho chúng tôi.
Đã phát hiện trình chặn quảng cáo AdBlock
Trang web này phụ thuộc vào doanh thu từ số lần hiển thị quảng cáo để tồn tại. Vui lòng tắt trình chặn quảng cáo của bạn hoặc tạm dừng tính năng chặn quảng cáo cho trang web này.