tailieunhanh - 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