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

Đặ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ộtbộ ba  (S, C, F). Trong đó S là một tập hợp các kí hiệusắp xếp (sort), C là một tập hợp cáckí hiệu xây dựng (constructor), và F là một tập hợp cáckí 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  và OBJ  là những  đặc tả đại số tuần tự, trong khi Lotos là một đặc tả đại số đồng thời. Cabrera và các đồng nghiệp 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.