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

48

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?

gablin
fuente
@Robert Harvey: Sí, acabo de leer eso en realidad. Pero me parece que los invariantes solo son útiles cuando intentas probar algo. ¿Es esto correcto (sin juego de palabras)?
gablin
Ese es mi entendimiento; cuando intentas razonar sobre tu programa, para probar su corrección.
Robert Harvey
3
@ user9094: Una afirmación es una declaración de que algo es verdadero en un punto particular en tiempo de ejecución y está representado en el código. Una invariante es una declaración (se espera que esté bien fundada) que siempre será cierta siempre que se aplique, y que no esté representada en el código mismo.
David Thornley
1
Las invariantes son de hecho útiles para probar la corrección, pero no se limitan a ese caso. También son útiles para la programación defensiva y durante la depuración. No solo ayudan a demostrar que su código es correcto, sino que ayudan a razonar sobre el código y a encontrar la ubicación de los errores cerca de los orígenes.
Pensamiento extraño

Respuestas:

41

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 ...)

Xavier Nodet
fuente
11
No es necesario que +1 para mencionar invariantes sea verdadero en medio de un método de ejecución.
Pensamiento extraño
1
@Oddthinking Best para evitar eso cuando sea posible. Sería fácil ingresar a un estado de ruptura invariable y olvidarse de restaurar todo correctamente antes de regresar. Las excepciones también pueden darte problemas.
Alexander
3
@Alexander: Para los invariantes no triviales, es casi imposible de evitar. Si necesita actualizar más de una variable en un método, como se describe en la respuesta, hay un punto en el que solo se ha actualizado una y la invariante es falsa. Existen suficientes restricciones para escribir un buen código sin agregar nuevos.
Pensamiento extraño
@Oddthinking Sí, a menudo es bastante inevitable. Pero, por ejemplo, si hay un grupo de variables que lógicamente pertenecen juntas (por ejemplo, una matriz y el índice de un elemento "seleccionado" en la matriz), entonces probablemente valga la pena extraerlas a un tipo. A partir de ahí, las mutaciones de la matriz o el tipo se pueden expresar como una sola asignación de una nueva instancia de ese tipo
Alexander
13

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.

Daniel Burbank
fuente
1
Si un invariante es una regla lógica que debe obedecerse durante la ejecución de su programa, y ​​su regla lógica es que no se pueden activar dos engranajes al mismo tiempo, entonces no es el invariante que no se puedan activar dos engranajes al mismo tiempo ¿hora? Sin esta invariante, su transmisión podría estar en dos marchas al mismo tiempo y, por lo tanto, desgarrarse. Primero, ¿no es un cambiador de palanca único que realmente impone esa invariante? Segundo, ¿por qué un invariante sería intrínsecamente bueno o malo?
Dustin Cleveland
1
La comparación con los engranajes del automóvil es muy clara para mí. ¡Gracias!
Marecky
"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". - Me gusta bastante, conciso y fácil de recordar.
ZeroKnight
@DustinCleveland Creo que en este ejemplo, los mecanismos detrás del cambio de palanca son el 'compilador' que 'hace cumplir' las reglas, mientras que el controlador que podría causar un incidente es uno de los muchos clientes que deben consumir y recordar la información que está sido "documentado, discutido, comentado o comunicado de otra manera".
ebernard
¡Brillante explicación! Realmente entiendo ahora el razonamiento sobre por qué tener invariantes en su código es una mala práctica.
Ben C Wang
3

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.

softveda
fuente
3

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.

Jonathan Aquino
fuente
1

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.

Pemdas
fuente
Las invariantes verifican el estado de un programa. No son decisiones de diseño.
Xavier Nodet
3
Las invariantes no comprueban nada. Puede verificar el estado del programa para ver si un invariante es VERDADERO o FALSO, pero los invariantes "no" hacen nada.
Pemdas
2
Por lo general, en C ++ vería algún tipo de invariancia de clase, como el miembro x debe ser menor que 25 y mayor que 0. Esa es la invariante. Cualquier verificación contra esa invariante son afirmaciones. En el ejemplo que tengo arriba, mi invariante es si pParentAccountUserName es NULL o está vacío, entonces es una cuenta principal. Las invariantes son decisiones diseñadas.
Pemdas
¿Cómo verifica que si pParentAccountUserName es NULL o está vacío, este objeto es la cuenta principal? Su declaración solo define lo que se supone que representa un valor nulo / vacío. Lo invariable es que el sistema se ajusta a eso, es decir, que pParentAccountUserName solo puede ser nulo o vacío si es una cuenta principal. Es una distinción sutil.
Cameron
1

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.

Omega Centauri
fuente
1
-1 Las invariantes en física son diferentes. Calcular una solución no es lo mismo que probar que un algoritmo es correcto. Para este último, los invariantes pueden probar la corrección.
aaronasterling