Bất biến là một thuật ngữ được sử dụng trong điện toán để chỉ một phần tử không thay đổi theo thời gian hoặc phản ứng với các tác động bên ngoài. Nó là một khái niệm được sử dụng trong công nghệ phần mềm, mô hình hóa dữ liệu và thiết kế thuật toán để mô tả và chứng minh các thuộc tính nhất định của một hệ thống hoặc một hệ thống con trong một hệ thống.
Các bất biến cung cấp những cách quan trọng để suy luận một cách hiệu quả về hành vi của một hệ thống, vì chúng chỉ ra các đối tượng sẽ giữ nguyên bất kể hành vi độc lập của các đối tượng khác hoặc các ảnh hưởng bên ngoài. Bất biến được sử dụng trong nhiều ngôn ngữ lập trình, mô hình và cách tiếp cận khác nhau, từ logic vị từ đến lập trình hướng đối tượng.
Các bất biến cung cấp một cách hữu ích để xác minh tính đúng đắn của thiết kế phần mềm hoặc hệ thống. Chúng cũng có thể được sử dụng để tìm các lỗi có thể gây ra sự cố khi thực thi chương trình. Ví dụ, khi gỡ lỗi một hệ thống, các bất biến có thể giúp tách biệt một lỗi, vì nếu bất biến đó không được thỏa mãn thì lỗi đó phải do phần hệ thống bị ảnh hưởng bởi nó gây ra.
Các bất biến cũng rất quan trọng trong đặc tả hệ thống hình thức, vì chúng có thể được sử dụng để chứng minh rằng một hệ thống nhất định có các đặc tính mong muốn nhất định như tính chính xác, an toàn, bảo mật hoặc độ tin cậy. Bất biến được sử dụng để mô tả bất kỳ khía cạnh nào của hệ thống trong đó thuộc tính cụ thể không đổi, bao gồm chức năng của chương trình hoặc màu sắc của thực thể trong giao diện người dùng đồ họa.
Các bất biến thường được sử dụng kết hợp với các kỹ thuật khác để kiểm tra tính đúng đắn và độ tin cậy của phần mềm, bao gồm cả những kỹ thuật liên quan đến kiểm tra khẳng định và chứng minh định lý. Kiểm tra bất biến được sử dụng rộng rãi trong các trình biên dịch vì nó có thể giúp xác minh tĩnh mã chương trình trước khi chạy. Nó cũng được sử dụng trong việc phát triển các hệ thống đáng tin cậy hơn, vì có thể nêu một số bất biến của hệ thống và sau đó xác minh rằng các đặc tính này được bảo toàn.
