Ta sẽ định nghĩa về ngôn ngữ CSL (Component Specificaion Language) là nền tảng cho việc thống nhất các công nghệ thành phần. Các lý do khiến nó trở thành ngôn ngữ hình thức:
§ Lọc lại các xáo trộn và sai sót
§ Kích thích trí tuệ
§ Định nghĩa chính xác các điều kiện cần thiết cho nghiên cứu và phát triển trong khuôn khổ đặc tả
§ Mô hình hình thức hỗ trợ các đặc tả hình thức và thẩm tra hình thức
§ Mô hình hình thức hỗ trợ phát triển công cụ tự động
Cú pháp giống BNF.
Kí hiệu đầu cuối sử dụng font chữ dạng typewriter
Không phải các đầu cuối sử dụng font in nghiêng
Thanh sổ dọc | : sự thay phiên
Từ trong ngoặc đơn (…) : một nhóm
Từ trong ngoặc với dấu sao (…)* : chỉ số không, một hoặc một số sự kiện của các phần trong ngoặc.
Từ trong ngoặc với dấu cộng (…)+ : chỉ ra một hoặc một số sự kiện của các phần trong ngoặc.
Dấu ngoặc […] chỉ ra các tùy chọn
Khoảng trắng (Blank)
Bao gồm: space, new-line và Tab ngang. Khoảng trắng ngắn cách các identifier, literal và từ khóa gần kế
Chú thích
Giống chú thích Java. Trên dòng đơn sử dụng //. Cho một khối /* …. */
Identifier
Là chuỗi các kí tự, kí số và _ bắt đầu bằng một kí tự. Có 52 kí từ hoa và thường từ tập ASCII.
Số nguyên
Là chuỗi của một hoặc nhiều kí số. Mặc định số nguyên thuộc hệ thập phân
Integer-literal :: = (0… 9) + |
0x (0 .. 9 | A .. F | a ..f ) + |
0o(0 .. 7) +
Trong đó 0x là hệ thập lục phân, 0o là hệ bát phân
Số Boolean
boolean-literal :: = true |false
Số Bit
Được qui định với dấu ‘
bits-literal ::= ‘(bit)+’
bit :: = 0 | 1 | ∗ | .
Toán tử tiền tố và trung tố
+ – * / ^ ||
+p -p +m -m +e -e
Toán tự trạng thái và thời gian
Dùng để ghi lại ghi lại các yêu cầu về thuộc tính thời gian
Temporal_operator :: =G | F | U | X
State_operator :: = next() |previous()
Trong đó:
G chỉ “luôn luôn”, “từ đây về sau” hoặc “toàn bộ”
F chỉ “cuối cùng”, hoặc “đôi khi”
U chỉ “đến khi”. Công thứ pUq có nghĩa là p true trước khi q đạt true
X chỉ “tiếp” công thức Xp có nghĩa p true vào trạng thái tiếp theo
Từ khóa
extends implements requires effects public protected Private static
Đặc tả thành phần
Ngữ nghĩa hình thức của CSL Dựa theo đại số sắp xếp. Đại số bao gồm miền giá trị và tập các toàn tử hoặc hàm định nghĩa trên miền:
