En programación informática , específicamente en programación orientada a objetos , un invariante de clase (o invariante de tipo ) es un invariante utilizado para restringir objetos de una clase . Los métodos de la clase deben conservar el invariante. El invariante de clase restringe el estado almacenado en el objeto.
Las invariantes de clase se establecen durante la construcción y se mantienen constantemente entre llamadas a métodos públicos. El código dentro de las funciones puede romper las invariantes siempre que estas se restablezcan antes de que finalice una función pública. Con concurrencia , mantener la invariante en los métodos normalmente requiere que se establezca una sección crítica bloqueando el estado con un mutex .
Un invariante de objeto , o invariante de representación , es una construcción de programación informática que consiste en un conjunto de propiedades invariantes que permanecen intactas independientemente del estado del objeto. Esto garantiza que el objeto siempre cumplirá con las condiciones predefinidas y que, por lo tanto, los métodos siempre pueden hacer referencia al objeto sin el riesgo de realizar suposiciones inexactas. La definición de invariantes de clase puede ayudar a los programadores y evaluadores a detectar más errores durante las pruebas de software .
El efecto útil de las invariantes de clase en el software orientado a objetos se mejora en presencia de herencia. Las invariantes de clase se heredan, es decir, "las invariantes de todos los padres de una clase se aplican a la clase misma". [1]
La herencia puede permitir que las clases descendientes alteren los datos de implementación de las clases padre, por lo que sería posible que una clase descendiente cambiara el estado de las instancias de una manera que las hiciera inválidas desde el punto de vista de la clase padre. La preocupación por este tipo de descendientes con mal comportamiento es una de las razones que dan los diseñadores de software orientado a objetos para favorecer la composición en lugar de la herencia (es decir, la herencia rompe la encapsulación). [2]
Sin embargo, debido a que las invariantes de clase se heredan, la invariante de clase para cualquier clase en particular consiste en cualquier afirmación invariante codificada inmediatamente en esa clase junto con todas las cláusulas invariantes heredadas de los padres de la clase. Esto significa que, aunque las clases descendientes pueden tener acceso a los datos de implementación de sus padres, la invariante de clase puede evitar que manipulen esos datos de cualquier manera que produzca una instancia no válida en tiempo de ejecución.
Los lenguajes de programación comunes como Python, [3] PHP, [4] JavaScript, [ cita requerida ] C++ y Java admiten aserciones de forma predeterminada, que se pueden usar para definir invariantes de clase. Un patrón común para implementar invariantes en clases es que el constructor de la clase genere una excepción si no se satisface la invariante. Dado que los métodos preservan las invariantes, pueden asumir la validez de la invariante y no necesitan verificarla explícitamente.
La invariante de clase es un componente esencial del diseño por contrato . Por lo tanto, los lenguajes de programación que brindan soporte nativo completo para el diseño por contrato , como Eiffel , Ada y D , también brindarán soporte completo para invariantes de clase.
Para C++ , la biblioteca Loki proporciona un marco para verificar invariantes de clase, invariantes de datos estáticos y seguridad de excepciones.
Para Java, existe una herramienta más poderosa llamada Lenguaje de Modelado Java que proporciona una forma más sólida de definir invariantes de clase.
El lenguaje de programación Ada tiene soporte nativo para invariantes de tipo (así como precondiciones y postcondiciones, predicados de subtipo, etc.). Un invariante de tipo puede darse en un tipo privado (por ejemplo, para definir una relación entre sus propiedades abstractas), o en su definición completa (normalmente para ayudar a verificar la corrección de la implementación del tipo). [5] Aquí hay un ejemplo de un invariante de tipo dado en la definición completa de un tipo privado utilizado para representar una pila lógica. La implementación utiliza una matriz, y el invariante de tipo especifica ciertas propiedades de la implementación que permiten pruebas de seguridad. En este caso, el invariante asegura que, para una pila de profundidad lógica N, los primeros N elementos de la matriz son valores válidos. La Default_Initial_Condition del tipo Stack, al especificar una pila vacía, asegura la verdad inicial del invariante, y Push preserva el invariante. La verdad del invariante permite entonces a Pop confiar en el hecho de que la parte superior de la pila es un valor válido, lo que es necesario para probar la postcondición de Pop. Un invariante de tipo más complejo permitiría la prueba de corrección funcional completa, como que Pop devuelve el valor pasado a un Push correspondiente, pero en este caso simplemente estamos tratando de demostrar que Pop no devuelve un Invalid_Value.
El tipo genérico Item es privado ; Invalid_Value : en Item ; el paquete Stacks es de tipo Stack ( Max_Depth : Positive ) es privado con Default_Initial_Condition => Is_Empty ( Stack ); función Is_Empty ( S : en la pila ) devuelve Boolean ; función Is_Full ( S : en la pila ) devuelve Boolean ; procedimiento Push ( S : en salida Stack ; I : en Item ) con Pre => no Is_Full ( S ) y entonces I /= Invalid_Value , Post => no Is_Empty ( S ); procedimiento Pop ( S : en salida Stack ; I : fuera Item ) con Pre => no Is_Empty ( S ), Post => no Is_Full ( S ) y entonces I /= Invalid_Value ; el tipo privado Item_Array es una matriz ( rango positivo <>) de Item ; tipo Stack ( Max_Depth : Positive ) es registro Longitud : Natural := 0 ; Datos : Item_Array ( 1 .. Max_Depth ) := ( otros => Invalid_Value ); finalizar registro con Type_Invariant => Length <= Max_Depth y luego ( para todos los J en 1 .. Length => Data ( J ) /= Invalid_Value ); función Is_Empty ( S : en la pila ) devuelve Boolean es ( S . Longitud = 0 ); función Is_Full ( S : en la pila ) devuelve Boolean es ( S . Longitud = S . Profundidad_máx ); fin Stacks ;El lenguaje de programación D tiene soporte nativo para invariantes de clase, así como otras técnicas de programación por contrato . A continuación se muestra un ejemplo de la documentación oficial. [6]
clase Fecha { int día ; int hora ; invariante () { afirmar ( día >= 1 && día <= 31 ); afirmar ( hora >= 0 && hora <= 23 ); } } En Eiffel , la clase invariante aparece al final de la clase después de la palabra clave invariant.
FECHA de clasecrear hacercaracterística { NONE } - Inicialización make ( a_day : INTEGER ; a_hour : INTEGER ) -- Inicializa `Current' con `a_day' y `a_hour'. require valid_day : a_day >= 1 y a_day <= 31 valid_hour : a_hour >= 0 y a_hour <= 23 do day := a_day hour := a_hour ensure day_set : day = a_day hour_set : hour = a_hour end característica -- Acceso día : ENTERO -- Día del mes para 'Actual' hora : ENTERO -- Hora del día para 'Actual' Característica -- Cambio de elemento set_day ( a_day : INTEGER ) -- Establece `day' en `a_day' requiere argumento válido : a_day >= 1 y a_day <= 31 hacer day := a_day asegurar day_set : day = a_day fin set_hour ( a_hour : INTEGER ) -- Establece `hora' en `a_hour' require valid_argument : a_hour >= 0 y a_hour <= 23 do hour := a_hour ensure hour_set : hour = a_hour end invariante valid_day : día >= 1 y día <= 31 valid_hour : hora >= 0 y hora <= 23 fin La biblioteca Loki (C++) proporciona un marco escrito por Richard Sposato para verificar invariantes de clase, invariantes de datos estáticos y el nivel de seguridad de excepciones .
Este es un ejemplo de cómo la clase puede usar Loki::Checker para verificar que las invariantes sigan siendo verdaderas después de que un objeto cambie. El ejemplo usa un objeto de punto geográfico para almacenar una ubicación en la Tierra como una coordenada de latitud y longitud.
Los invariantes del punto geográfico son:
#include <loki/Checker.h> // Necesario para comprobar las invariantes de clase. #include <Grados.hpp> clase GeoPoint { public : GeoPoint ( Grados latitud , Grados longitud ); /// La función Mover moverá la ubicación de GeoPoint. void Move ( Degrees latitude_change , Degrees longitude_change ) { // El objeto verificador llama a IsValid en la entrada y salida de la función para probar que este objeto GeoPoint es válido. El verificador también garantiza que la función GeoPoint::Move nunca lanzará una excepción. CheckFor :: CheckForNoThrow checker ( this , & IsValid ); latitud_ += cambio_de_latitud ; si ( latitud_ >= 90.0 ) latitud_ = 90.0 ; si ( latitud_ <= -90.0 ) latitud_ = -90.0 ; longitud_ += cambio_longitud ; mientras ( longitud_ >= 180.0 ) longitud_ -= 360.0 ; mientras ( longitud_ <= -180.0 ) longitud_ += 360.0 ; } privado : /** @note CheckFor realiza una comprobación de validez en muchas funciones para determinar si el código violó alguna invariante, si algún contenido cambió o si la función lanzó una excepción. */ using CheckFor = :: Loki :: CheckFor < const GeoPoint > ; /// Esta función comprueba todas las invariantes del objeto. bool IsValid () const { assert ( this != nullptr ); assert ( latitud_ >= -90.0 ); assert ( latitud_ <= 90.0 ); assert ( longitud_ >= -180.0 ); assert ( longitud_ <= 180.0 ); return true ; } Grados de latitud_ ; ///< Grados desde el ecuador. El positivo es el norte, el negativo es ///< el sur. Grados de longitud_ ; ///< Grados desde el meridiano de Greenwich. El positivo es el este, ///< el negativo es el oeste. } Este es un ejemplo de una invariante de clase en el lenguaje de programación Java con Lenguaje de modelado Java . La invariante debe cumplirse como verdadera después de que finalice el constructor y en la entrada y salida de todas las funciones miembro públicas. Las funciones miembro públicas deben definir condiciones previas y posteriores para ayudar a garantizar la invariante de clase.
clase pública Fecha { int /*@spec_public@*/ día ; int /*@spec_public@*/ hora ; /*@invariante día >= 1 && día <= 31; @*/ //invariante de clase /*@invariante hora >= 0 && hora <= 23; @*/ //invariante de clase /*@ @requiere d >= 1 && d <= 31; @requiere h >= 0 && h <= 23; @*/ public Date ( int d , int h ) { // constructor día = d ; hora = h ; } /*@ @requiere d >= 1 && d <= 31; @garantiza que día == d; @*/ public void setDay ( int d ) { día = d ; } /*@ @requiere h >= 0 && h <= 23; @garantiza que la hora == h; @*/ public void setHour ( int h ) { hora = h ; } }