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;
    }
}

Referências

links externos