Por que os invariantes são importantes em Ciência da Computação

Eu entendo 'invariável' em seu sentido literal. Também os reconheço quando digito código. Mas acho que não entendo a importância desse termo no contexto da ciência da computação.

Sempre que leio conversas \ white papers sobre design de linguagem de programadores \ cientistas de computadores famosos, o termo 'invariável' continua aparecendo como um jargão; e essa é a parte que eu não entendo. O que é tão especial sobre isso?

Um algoritmo é um processo repetível. Se é repetível, deve ter atributos que não mudam com a repetição. Estes são seus invariantes. Os invariantes são combinados e / ou operam nos (potencialmente) dados variáveis ​​que serão alimentados no seu algoritmo.

Portanto, o objetivo principal da programação é identificar o que não varia - que é essencialmente o seu programa.

No programa orientado a objetos, existe a noção de que cada objeto deve fazer bem uma única coisa. Isso significa essencialmente que (para OOP baseado em classe), uma classe define os invariantes para um único algoritmo, juntamente com espaços reservados (variáveis) para quaisquer dados variantes que seus objetos possam precisar. Idealmente, em OO, você isolaria o que variar o máximo possível, para que cada objeto seja praticamente invariável.

A noção de invariante está fortemente ligada a "efeitos colaterais". Acredito que foi promovido pela abordagem 'Design by Contract (DbC)' de Bertrand Meyer para design de software.

O DbC enriquece tipos de dados abstratos (coluna vertebral de classes) com 3 noções importantes, pré-condições, pós-condições, invariantes . É facilmente explicado ao se referir a procedimentos, então tentarei explicar com referência a ele:

1. Uma pré-condição representa os dados de entrada da condição para um procedimento que deve ser respeitado para chamar esse procedimento. Essa pré-condição deve ser respeitada e aplicada pelo cliente desse procedimento específico. O designer do procedimento pode, no entanto, defender de clientes que não respeitam a pré-condição, afirmando essa condição como primeiras linhas no procedimento. Por exemplo, ter um método double divide(double dividend, double divisor)pode ser uma pré-condição divisor != 0.

2. Uma pós-condição representa a condição a nos dados de saída após o retorno do procedimento; é dever do projetista do procedimento respeitar essa pós-condição, desde que a pré-condição seja respeitada; em um estilo de programação de defesa antes de retornar, a pós-condição pode ser afirmada.

3. Um invariante pode ser considerado uma pré-condição e uma pós-condição, mas com um entendimento diferente para a pré-condição e pós-condição dos conceitos acima. Um invariante basicamente diz que, se a entrada tiver uma condição específica atendida antes do procedimento ser chamado, essa condição específica será válida após o procedimento ser chamado. Por exemplo, uma invariável válida para um procedimento boolean search(int term, int array[])pode dizer que o estado arrayanterior à chamada é o mesmo que é após a chamada.

Impor os invariantes aos procedimentos (e não apenas aos procedimentos) é uma grande coisa, pois reduz os efeitos colaterais ; isso é útil, pois os efeitos colaterais são um grande mal na programação. Um procedimento específico pode alterar o estado dos argumentos de entrada, ou alterar o estado de algumas variáveis ​​globais, ou depender de algumas variáveis ​​globais; isso pode levar a situações desagradáveis ​​em que duas chamadas idênticas no mesmo procedimento (com a mesma entrada) podem produzir resultados diferentes. Isso leva a conhecer o histórico das chamadas e é muito difícil depurar, especialmente em um contexto de multithreading.

Uma invariável é uma propriedade lógica que é preservada por algumas operações.

• Você precisa de invariantes para raciocinar sobre loops. Como você não sabe de antemão quantas iterações haverá (ou você não precisaria de um loop), cada iteração deve preservar a invariante, para que no final você possa provar alguma propriedade útil sobre o loop.

• Você precisa de invariantes para raciocinar sobre propriedades de dados encapsulados. Geralmente, os vários dados dentro de um módulo ou objeto precisam satisfazer determinadas propriedades para a operação correta (por exemplo, uma lista que representa um conjunto sempre deve ser classificada). Você deseja que cada função ou método que opere nos dados preserve essas propriedades, portanto elas também são invariantes.

Pelo que sei, a importância de invariante vem do fato de ser o alicerce para provar que um algoritmo calcula uma determinada função. Por exemplo, você desenvolveu um novo algoritmo de classificação, mas como pode ter certeza de que ele realmente se classifica com todas as entradas ou com todas as saídas corretas. O próximo passo é construir invariantes que correspondam ao fluxo do algoritmo e provar que ele classifica usando os invariantes.

No contexto do sistema de tipos de uma linguagem de programação, um tipo invariável é um tipo não conversível. Por exemplo, em java, ao sobrecarregar um método, todos os parâmetros são invariantes, enquanto o tipo de retorno é covariante (pode ser o mesmo ou um subtipo).