Phần mềm-Ứng dụng

Kỹ thuật đặc tả hệ thống dựa trên thuộc tính có thể được phân loại thành đặc tả tiên đề và đặc tả đại số. Một đặc tả đại số bao gồm một phần cú pháp và một phần ngữ nghĩa. Phần cú pháp định nghĩa các hoạt động có thể thực hiện trên hệ thống. Nó được mô tả bằng một bộ ba  (S, C, F). Trong đó S là một tập hợp các kí hiệu sắp xếp (sort), C là một tập hợp các kí hiệu xây dựng (constructor), và F là một tập hợp các kí hiệu chức năng (Function). Phần ngữ nghĩa mô tả hành vi của hệ thống bằng cách xác định ngữ nghĩa của các hoạt động của nó. Ngữ nghĩa này được mô tả bằng một tập hợp các các tiên đề. Larch [35], và OBJ [36] là những  đặc tả đại số tuần tự, trong khi Lotos [37] là một đặc tả đại số đồng thời. Cabrera và các đồng nghiệp, trong [38], sử dụng GRAPLA là một ngôn ngữ đặc tả đại số để xác định các giao diện người dùng đồ họa với các cửa sổ, các nút, và menu. Các ngôn ngữ sau này được mở rộng thêm với các khái niệm như các đối tượng tương tác, và hành động người dùng.