Tài liệu Các kỹ thuật đặc tã

Phát triểnKhi một đặc tả hình thức đã được phát triển xong, đặc tả đó có thể được sử dụng làm một hướng dẫn trong quá trình hệ thống thực được phát triển (nghĩa là được hiện thực hóa trong phần mềm và/hoặc phần cứng). Ví dụ:

Nếu đặc tả hình thức là một ngữ nghĩa hoạt động, hành vi được quan sát của hệ thống thực sẽ có thể được so sánh với hành vi trong đặc tả (chính đặc tả cũng nên chạy được hoặc giả lập được). Thêm vào đó, các lệnh hoạt động của đặc tả có thể thích hợp cho việc dịch thẳng mã chạy được.
Nếu đặc tả hình thức là một ngữ nghĩa tiên đề, các tiền điều kiện và hậu điều kiện của đặc tả có thể trở thành các assertion
If the formal specification is in an axiomatic semantics, the preconditions and postconditions of the specification may become khẳng định (assertion') trong mã chạy được