Invariante de classe - Class invariant
Na programação de computadores , especificamente na programação orientada a objetos , uma invariante de classe (ou invariante de tipo ) é uma invariante usada para restringir objetos de uma classe . Os métodos da classe devem preservar o invariante. A invariante de classe restringe o estado armazenado no objeto.
Invariantes de classe são estabelecidos durante a construção e mantidos constantemente entre chamadas a métodos públicos. O código dentro das funções pode quebrar invariantes, desde que as invariantes sejam restauradas antes do término de uma função pública. Com a simultaneidade, manter a invariante nos métodos normalmente requer que uma seção crítica seja estabelecida bloqueando o estado usando um mutex.
Um invariante de objeto, ou invariante de representação, é uma construção de programação de computador que consiste em um conjunto de propriedades invariantes que permanecem não comprometidas, independentemente do estado do objeto . Isso garante que o objeto sempre atenderá às condições predefinidas e que os métodos podem, portanto, sempre fazer referência ao objeto sem o risco de fazer suposições imprecisas. Definir invariantes de classe pode ajudar os programadores e testadores a detectar mais bugs durante o teste de software .
Invariantes de classe e herança
O efeito útil de invariantes de classe em software orientado a objetos é aprimorado na presença de herança. As invariantes de classe são herdadas, ou seja, "as invariantes de todos os pais de uma classe se aplicam à própria classe".
A herança pode permitir que as classes descendentes alterem os dados de implementação das classes pai, portanto, seria possível para uma classe descendente alterar o estado das instâncias de uma forma que as tornasse inválidas do ponto de vista da classe pai. A preocupação com esse tipo de descendente malcomportado é um dos motivos dados pelos designers de software orientado a objetos para favorecer a composição em vez da herança (isto é, a herança quebra o encapsulamento).
No entanto, como as invariantes de classe são herdadas, a invariante de classe para qualquer classe particular consiste em quaisquer asserções invariantes codificadas imediatamente nessa classe em conjunto com todas as cláusulas invariantes herdadas dos pais da classe. Isso significa que, embora as classes descendentes possam ter acesso aos dados de implementação de seus pais, a invariante da classe pode impedi-los de manipular esses dados de qualquer forma que produza uma instância inválida em tempo de execução.
Suporte a linguagem de programação
Afirmações
Linguagens de programação comuns como Python, JavaScript, C ++ e Java suportam asserções por padrão, que podem ser usadas para definir invariantes de classe. Um padrão comum para implementar invariantes em classes é o construtor da classe lançar uma exceção se a invariante não for satisfeita. Uma vez que os métodos preservam as invariantes, eles podem assumir a validade da invariante e não precisam verificar explicitamente por ela.
Suporte nativo
A invariante de classe é um componente essencial do projeto por contrato . Portanto, as linguagens de programação que fornecem suporte nativo completo para design por contrato , como Rust , Eiffel , Ada e D , também fornecerão suporte total para invariantes de classe.
Suporte não nativo
Para C ++ , a Biblioteca Loki fornece uma estrutura para verificar invariantes de classe, invariantes de dados estáticos e segurança de exceção.
Para Java, existe uma ferramenta mais poderosa chamada Java Modeling Language que fornece uma maneira mais robusta de definir invariantes de classe.
Exemplos
Suporte nativo
D
A linguagem de programação D tem suporte nativo de invariantes de classe, bem como outras técnicas de programação de contrato . Aqui está um exemplo da documentação oficial.
class Date {
int day;
int hour;
invariant() {
assert(day >= 1 && day <= 31);
assert(hour >= 0 && hour <= 23);
}
}
Eiffel
Em Eiffel , a invariante de classe aparece no final da classe após a palavra-chave invariant
.
class
DATE
create
make
feature {NONE} -- Initialization
make (a_day: INTEGER; a_hour: INTEGER)
-- Initialize `Current' with `a_day' and `a_hour'.
require
valid_day: a_day >= 1 and a_day <= 31
valid_hour: a_hour >= 0 and a_hour <= 23
do
day := a_day
hour := a_hour
ensure
day_set: day = a_day
hour_set: hour = a_hour
end
feature -- Access
day: INTEGER
-- Day of month for `Current'
hour: INTEGER
-- Hour of day for `Current'
feature -- Element change
set_day (a_day: INTEGER)
-- Set `day' to `a_day'
require
valid_argument: a_day >= 1 and a_day <= 31
do
day := a_day
ensure
day_set: day = a_day
end
set_hour (a_hour: INTEGER)
-- Set `hour' to `a_hour'
require
valid_argument: a_hour >= 0 and a_hour <= 23
do
hour := a_hour
ensure
hour_set: hour = a_hour
end
invariant
valid_day: day >= 1 and day <= 31
valid_hour: hour >= 0 and hour <= 23
end
Suporte não nativo
C ++
A biblioteca Loki (C ++) fornece uma estrutura escrita por Richard Sposato para verificar invariantes de classe, invariantes de dados estáticos e nível de segurança de exceção .
Este é um exemplo de como a classe pode usar Loki :: Checker para verificar se as invariantes permanecem verdadeiras após a mudança de um objeto. O exemplo usa um objeto geoponto para armazenar um local na Terra como uma coordenada de latitude e longitude.
Os invariantes de geopontos são:
- a latitude não pode ser superior a 90 ° norte.
- a latitude não pode ser inferior a -90 ° sul.
- a longitude não pode ser superior a 180 ° leste.
- a longitude não pode ser inferior a -180 ° oeste.
#include <loki/Checker.h> // Needed to check class invariants.
#include <Degrees.hpp>
class GeoPoint {
public:
GeoPoint(Degrees latitude, Degrees longitude);
/// Move function will move location of GeoPoint.
void Move(Degrees latitude_change, Degrees longitude_change) {
// The checker object calls IsValid at function entry and exit to prove this
// GeoPoint object is valid. The checker also guarantees GeoPoint::Move
// function will never throw.
CheckFor::CheckForNoThrow checker(this, &IsValid);
latitude_ += latitude_change;
if (latitude_ >= 90.0) latitude_ = 90.0;
if (latitude_ <= -90.0) latitude_ = -90.0;
longitude_ += longitude_change;
while (longitude_ >= 180.0) longitude_ -= 360.0;
while (longitude_ <= -180.0) longitude_ += 360.0;
}
private:
/** @note CheckFor performs validity checking in many functions to determine
if the code violated any invariants, if any content changed, or if the
function threw an exception.
*/
using CheckFor = ::Loki::CheckFor<const GeoPoint>;
/// This function checks all object invariants.
bool IsValid() const {
assert(this != nullptr);
assert(latitude_ >= -90.0);
assert(latitude_ <= 90.0);
assert(longitude_ >= -180.0);
assert(longitude_ <= 180.0);
return true;
}
Degrees latitude_; ///< Degrees from equator. Positive is north, negative is
///< south.
Degrees longitude_; ///< Degrees from Prime Meridian. Positive is east,
///< negative is west.
}
Java
Este é um exemplo de uma invariante de classe na linguagem de programação Java com Java Modeling Language . O invariante deve ser verdadeiro depois que o construtor for concluído e na entrada e saída de todas as funções-membro públicas. As funções de membro público devem definir a pré - condição e a pós - condição para ajudar a garantir a invariante da classe.
public class Date {
int /*@spec_public@*/ day;
int /*@spec_public@*/ hour;
/*@invariant day >= 1 && day <= 31; @*/ //class invariant
/*@invariant hour >= 0 && hour <= 23; @*/ //class invariant
/*@
@requires d >= 1 && d <= 31;
@requires h >= 0 && h <= 23;
@*/
public Date(int d, int h) { // constructor
day = d;
hour = h;
}
/*@
@requires d >= 1 && d <= 31;
@ensures day == d;
@*/
public void setDay(int d) {
day = d;
}
/*@
@requires h >= 0 && h <= 23;
@ensures hour == h;
@*/
public void setHour(int h) {
hour = h;
}
}