¿Por qué los invariantes son importantes en informática?

Entiendo 'invariante' en su sentido literal. También los reconozco cuando escribo código. Pero no creo entender la importancia de este término en el contexto de la informática.

Cada vez que leo conversaciones \ informes sobre diseño de lenguaje de programadores famosos \ informáticos, el término "invariante" sigue apareciendo como una jerga; y esa es la parte que no entiendo. ¿Qué tiene de especial?

Un algoritmo es un proceso repetible. Si es repetible, debe tener atributos que no cambien con la repetición. Estos son tus invariantes. Los invariantes se combinan y / u operan con los datos (potencialmente) variables que se introducirán en su algoritmo.

Por lo tanto, el objetivo de la programación es identificar lo que no varía: ese es esencialmente su programa.

En el programa orientado a objetos, existe la noción de que cada objeto debe hacer bien una sola cosa. Esto esencialmente significa que (para OOP basada en clases) una clase define los invariantes para un solo algoritmo, junto con marcadores de posición (variables) para cualquier variante de datos que sus objetos puedan necesitar. Idealmente en OO, aislarías lo que varía tanto como sea posible, de modo que cada objeto sea mayormente invariable.

La noción de invariante está fuertemente relacionada con los "efectos secundarios". Creo que fue promovido por el enfoque 'Design by Contract (DbC)' de Bertrand Meyer para el diseño de software.

DbC enriquece los tipos de datos abstractos (columna vertebral de clases) con 3 nociones importantes, condiciones previas, condiciones posteriores, invariantes . Se explica fácilmente cuando se hace referencia a los procedimientos, por lo que intentaré explicarlo en referencia con él:

1. Una condición previa representa la condición que los datos de entrada para un procedimiento deben respetar para poder llamar a ese procedimiento. Esta condición previa debe ser respetada y aplicada por el cliente de ese procedimiento en particular. Sin embargo, el diseñador del procedimiento puede defenderse de los clientes que no respetan la condición previa al afirmar esa condición como primeras líneas del procedimiento. Por ejemplo, tener un método double divide(double dividend, double divisor)puede ser una condición previa divisor != 0.

2. A postcondition representa la condición A en los datos de salida después del procedimiento retorna; el diseñador del procedimiento es totalmente responsable de respetar esta condición posterior siempre que se respete la condición previa; en un estilo de programación de defensa antes de regresar, se puede afirmar la condición posterior.

3. Una invariante puede considerarse como una precondición y una condición posterior, pero con una comprensión diferente de la condición previa y posterior a los conceptos anteriores. Un invariante básicamente dice que si la entrada tiene una condición particular cumplida antes de que se llame al procedimiento, entonces esa condición particular es válida después de que se llama al procedimiento. Por ejemplo, un invariante válido para un procedimiento boolean search(int term, int array[])podría decir que el estado de arrayantes de la llamada es el mismo que después de la llamada.

Hacer cumplir invariantes en los procedimientos (y no solo en los procedimientos) es una gran cosa, ya que reduce los efectos secundarios ; Esto es útil ya que los efectos secundarios son un gran mal en la programación. Un procedimiento particular podría cambiar el estado de los argumentos de entrada, o cambiar el estado de algunas variables globales, o depender de algunas variables globales; Esto puede conducir a situaciones desagradables en las que dos llamadas idénticas en el mismo procedimiento (con la misma entrada) pueden producir salidas diferentes. Esto lleva a conocer el historial de las llamadas y es muy difícil de depurar, especialmente en un contexto de subprocesos múltiples.

Una invariante es una propiedad lógica que es preservada por algunas operaciones.

• Necesitas invariantes para razonar sobre los bucles. Como no sabe de antemano cuántas iteraciones habrá (o no necesitaría un bucle), cada iteración debe preservar la invariante, para que al final pueda probar alguna propiedad útil sobre el bucle.

• Necesita invariantes para razonar sobre las propiedades de los datos encapsulados. A menudo, los diversos datos dentro de un módulo u objeto necesitan satisfacer ciertas propiedades para una operación correcta (por ejemplo, una lista que representa un conjunto siempre debe ordenarse). Desea que cada función o método que opera en los datos conserve estas propiedades, por lo que también son invariantes.

Por lo que sé, la importancia de invariante proviene del hecho de que es el bloque de construcción para demostrar que un algoritmo calcula una determinada función. Por ejemplo, ha desarrollado un nuevo algoritmo de clasificación, pero ¿cómo puede estar tan seguro de que realmente se ordena con cada entrada o con cada salida correcta? El siguiente paso es construir invariantes que correspondan al flujo del algoritmo y demostrar que se clasifica utilizando los invariantes.

En el contexto del sistema de tipos de un lenguaje de programación, un tipo invariante es un tipo no convertible. Por ejemplo, en Java, cuando se sobrecarga un método, todos los parámetros son invariables, mientras que el tipo de retorno es covariante (puede ser el mismo o un subtipo).