¿Qué son las invariantes, cómo se pueden usar y alguna vez las ha usado en su programa?

Estoy leyendo Coders at Work , y en él se habla mucho de invariantes. Por lo que he entendido, una invariante es una condición que tiene tanto antes como después de una expresión. Son, entre otras cosas, útiles para demostrar que ese ciclo es correcto, si recuerdo mi curso de lógica correctamente.

¿Es correcta mi descripción o me he perdido algo? ¿Alguna vez los has usado en tu programa? Y si es así, ¿cómo se beneficiaron?

En OOP, un invariante es un conjunto de afirmaciones que siempre deben ser ciertas durante la vida de un objeto para que el programa sea válido. Debería ser cierto desde el final del constructor hasta el inicio del destructor siempre que el objeto no esté ejecutando actualmente un método que cambie su estado.

Un ejemplo de invariante podría ser que exactamente una de las dos variables miembro debería ser nula. O que si uno tiene un valor dado, entonces el conjunto de valores permitidos para el otro es esto o aquello ...

A veces uso una función miembro del objeto para verificar que la invariante se mantenga. Si este no es el caso, se plantea una afirmación. Y el método se llama al inicio y a la salida de cada método que cambia el objeto (en C ++, esta es solo una línea ...)

Bueno, todo lo que veo en este hilo es genial, pero tengo una definición de 'invariante' que me ha sido de gran ayuda en el trabajo.

Una invariante es cualquier regla lógica que debe obedecerse durante la ejecución de su programa y que puede comunicarse a un humano, pero no a su compilador.

Esta definición es útil porque divide las condiciones en dos grupos: aquellos en los que se puede confiar que el compilador aplicará, y aquellos que deben documentarse, debatirse, comentarse o comunicarse de otra manera a los contribuyentes para que interactúen con la base de código sin introducir errores. .

Además, esta definición es útil porque le permite utilizar la generalización, "Las invariantes son malas".

Como ejemplo, la palanca de cambios en un automóvil de transmisión manual está diseñada para evitar una invariante. Si quisiera, podría construir una transmisión con una palanca para cada marcha. Esta palanca podría estar hacia adelante ("activada") o hacia atrás ("desactivada"). En dicho sistema, he creado un "invariante", que podría documentarse como tal:

"Es crítico que el engranaje actualmente enganchado se desacople antes de que se enganche un engranaje diferente. Enganchar cualquiera de los dos engranajes al mismo tiempo causará tensión mecánica que desgarrará la transmisión. Siempre desacople el engranaje actualmente enganchado antes de enganchar otro".

Y así, uno podría culpar a las transmisiones rotas de la conducción descuidada. Los autos modernos, sin embargo, usan un solo palo que gira entre los engranajes. Está diseñado de tal manera que, en un automóvil moderno de palanca de cambios, no es posible engranar dos marchas al mismo tiempo.

De esta manera, podríamos decir que la transmisión ha sido diseñada para 'eliminar lo invariante', ya que no permite que se configure mecánicamente de una manera que viole la regla lógica.

Cada invariante de este tipo que elimine de su código es una mejora, ya que reduce la carga cognitiva de trabajar con él.

Una invariante (en sentido común) significa algunas condiciones que deben ser ciertas en algún momento o incluso siempre mientras su programa se está ejecutando. por ejemplo, PreConditions y PostConditions pueden usarse para afirmar algunas condiciones que deben ser verdaderas cuando se llama a una función y cuando regresa. Los invariantes de objetos se pueden usar para afirmar que un objeto debe tener un estado válido durante todo el tiempo que existe. Este es el diseño por principio de contrato.
He usado invariantes informalmente usando cheques en el código. Pero más recientemente estoy jugando con la biblioteca de contratos de código para .Net que admite directamente invariantes.

Basado en la siguiente cita de Coders At Work ...

Pero una vez que conozca la invariante que está manteniendo, puede ver, ah, si mantenemos esa invariante, obtendremos el tiempo de búsqueda de registros.

... Supongo que "invariante" = "condición que desea mantener para garantizar el efecto deseado".

Parece que invariante tiene dos sentidos que difieren de una manera sutil:

1. Algo que se mantiene igual.
2. Algo que intenta mantener igual, para alcanzar el objetivo X (como un "tiempo de búsqueda de registro" arriba).

Entonces 1 es como una afirmación; 2 es como una herramienta para probar la corrección, el rendimiento u otras propiedades, creo. Consulte el artículo de Wikipedia para ver un ejemplo de 2 (que demuestra la corrección de la solución al rompecabezas MU).

En realidad, un tercer sentido de invariante es:

.3. Lo que se supone que debe hacer el programa (o módulo o función); en otras palabras, su propósito.

De la misma entrevista de Coders At Work:

Pero lo que hace que un gran software sea manejable es tener algunas invariantes globales o declaraciones generales sobre lo que se supone que debe hacer y las cosas que se supone que son ciertas.

Una invariante es como una regla o una suposición que se puede utilizar para dictar la lógica de su programa.

Por ejemplo, suponga que tiene alguna aplicación de software que realiza un seguimiento de las cuentas de usuario. Supongamos también que el usuario puede tener múltiples cuentas, pero por cualquier razón, necesita diferenciar entre la cuenta principal de un usuario y las cuentas "alias".

Esto podría ser un registro de base de datos u otra cosa, pero por ahora supongamos que cada cuenta de usuario está representada por un objeto de clase.

clase userAccount {private char * pUserName; private char * pParentAccountUserName;

...}

Una invariante podría ser la suposición de que si pParentAccountUserName es NULL o está vacío, entonces este objeto es la cuenta principal. Puede usar este invariante para distinguir diferentes tipos de cuenta. Probablemente haya mejores métodos para distinguir los diferentes tipos de cuentas de usuario, así que tenga en cuenta que este es solo un ejemplo para mostrar cómo se puede usar un invariante.

Viniendo de un fondo de física, en física tenemos invariantes, que son esencialmente cantidades que no varían a lo largo de toda la computación / simulación. Por ejemplo, en física, para un sistema cerrado se conserva la energía total. O, de nuevo, en física, si dos partículas chocan, los fragmentos resultantes deben contener exactamente la energía con la que comenzaron y exactamente el mismo impulso (una cantidad vectorial). Por lo general, no hay suficientes invariantes para especificar totalmente el resultado. Por ejemplo, en la colisión de 2 partículas, tenemos cuatro invariantes, tres componentes de impulso y un componente de energía, pero el sistema tiene seis grados de libertad (seis números para describir su estado). Los invariantes deben conservarse dentro del error de redondeo, pero su conservación no prueba que la solución sea correcta.

Por lo general, estas cosas son importantes como controles de cordura, pero por sí mismas no pueden probar la corrección.