Class invariant

In computer programming, specifically object-oriented programming, a class invariant (or type invariant) is an invariant used for constraining objects of a class. Methods of the class should preserve the invariant. The class invariant constrains the state stored in the object.

Class invariants are established during construction and constantly maintained between calls to public methods. Code within functions may break invariants as long as the invariants are restored before a public function ends. With concurrency, maintaining the invariant in methods typically requires a critical section to be established by locking the state using a mutex.

An object invariant, or representation invariant, is a computer programming construct consisting of a set of invariant properties that remain uncompromised regardless of the state of the object. This ensures that the object will always meet predefined conditions, and that methods may, therefore, always reference the object without the risk of making inaccurate presumptions. Defining class invariants can help programmers and testers to catch more bugs during software testing.

Class invariants and inheritance

The useful effect of class invariants in object-oriented software is enhanced in the presence of inheritance. Class invariants are inherited, that is, "the invariants of all the parents of a class apply to the class itself."[1]

Inheritance can allow descendant classes to alter implementation data of parent classes, so it would be possible for a descendant class to change the state of instances in a way that made them invalid from the viewpoint of the parent class. The concern for this type of misbehaving descendant is one reason object-oriented software designers give for favoring composition over inheritance (i.e., inheritance breaks encapsulation).[2]

However, because class invariants are inherited, the class invariant for any particular class consists of any invariant assertions coded immediately on that class in conjunction with all the invariant clauses inherited from the class's parents. This means that even though descendant classes may have access to the implementation data of their parents, the class invariant can prevent them from manipulating those data in any way that produces an invalid instance at runtime.

Programming language support

Assertions

Common programming languages like Python,[3] PHP,[4] JavaScript,[citation needed] C++ and Java support assertions by default, which can be used to define class invariants. A common pattern to implement invariants in classes is for the constructor of the class to throw an exception if the invariant is not satisfied. Since methods preserve the invariants, they can assume the validity of the invariant and need not explicitly check for it.

Native support

The class invariant is an essential component of design by contract. So, programming languages that provide full native support for design by contract, such as Eiffel, Ada, and D, will also provide full support for class invariants.

Non-native support

For C++, the Loki Library provides a framework for checking class invariants, static data invariants, and exception safety.

For Java, there is a more powerful tool called Java Modeling Language that provides a more robust way of defining class invariants.

Examples

Native support

Ada

The Ada programming language has native support for type invariants (as well as pre- and postconditions, subtype predicates, etc.). A type invariant may be given on a private type (for example to define a relationship between its abstract properties), or on its full definition (typically to help in verifying the correctness of the implementation of the type).[5] Here is an example of a type invariant given on the full definition of a private type used to represent a logical stack. The implementation uses an array, and the type invariant specifies certain properties of the implementation that enable proofs of safety. In this case, the invariant ensures that, for a stack of logical depth N, the first N elements of the array are valid values. The Default_Initial_Condition of the Stack type, by specifying an empty stack, ensures the initial truth of the invariant, and Push preserves the invariant. The truth of the invariant then enables Pop to rely on the fact that the top of the stack is a valid value, which is needed to prove Pop's postcondition. A more complex type invariant would enable the proof of full functional correctness, such as that Pop returns the value passed into a corresponding Push, but in this case we are merely trying to prove that Pop does not return an Invalid_Value.

generic
    type Item is private;
    Invalid_Value : in Item;
package Stacks is
    type Stack(Max_Depth : Positive) is private
        with Default_Initial_Condition => Is_Empty (Stack);

    function Is_Empty(S : in Stack) return Boolean;
    function Is_Full(S : in Stack) return Boolean;

    procedure Push(S : in out Stack; I : in Item)
        with Pre  => not Is_Full(S) and then I /= Invalid_Value,
             Post => not Is_Empty(S);
    procedure Pop(S : in out Stack; I : out Item)
        with Pre  => not Is_Empty(S),
             Post => not Is_Full(S) and then I /= Invalid_Value;
private
    type Item_Array is array (Positive range <>) of Item;

    type Stack(Max_Depth : Positive) is record
        Length : Natural := 0;
        Data : Item_Array (1 .. Max_Depth) := (others => Invalid_Value);
    end record
        with Type_Invariant => Length <= Max_Depth and then
          (for all J in 1 .. Length => Data (J) /= Invalid_Value);

    function Is_Empty(S : in Stack) return Boolean
        is (S.Length = 0);
    function Is_Full(S : in Stack) return Boolean
        is (S.Length = S.Max_Depth);
end Stacks;

D

D programming language has native support of class invariants, as well as other contract programming techniques. Here is an example from the official documentation.[6]

class Date {
  int day;
  int hour;

  invariant() {
    assert(day >= 1 && day <= 31);
    assert(hour >= 0 && hour <= 23);
  }
}

Eiffel

In Eiffel, the class invariant appears at the end of the class following the keyword 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

Non-native support

C++

The Loki (C++) library provides a framework written by Richard Sposato for checking class invariants, static data invariants, and exception safety level.

This is an example of how class can use Loki::Checker to verify invariants remain true after an object changes. The example uses a geopoint object to store a location on Earth as a coordinate of latitude and longitude.

The geopoint invariants are:

  • latitude may not be more than 90° north.
  • latitude may not be less than -90° south.
  • longitude may not be more than 180° east.
  • longitude may not be less than -180° west.
#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

This is an example of a class invariant in the Java programming language with Java Modeling Language. The invariant must hold to be true after the constructor is finished and at the entry and exit of all public member functions. Public member functions should define precondition and postcondition to help ensure the class invariant.

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

References

  1. ^ Meyer, Bertrand. Object-Oriented Software Construction, second edition, Prentice Hall, 1997, p. 570.
  2. ^ E. Gamma, R. Helm, R. Johnson, and J. Vlissides. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading, Massachusetts, 1995., p. 20.
  3. ^ Official Python Docs, assert statement
  4. ^ "PHP assert function". Archived from the original on 2001-03-21.
  5. ^ "Ada Reference Manual 7.3.2 Type Invariants". ada-auth.org. Retrieved 2022-11-27.
  6. ^ "Contract Programming - D Programming Language". dlang.org. Retrieved 2020-10-29.

Read other articles:

Yamada NagamasaPotret Yamada Nagamasa sekitar tahun 1630Nama asli山田 長政Lahir1590Numazu, Shizuoka, JepangMeninggal1630Ligor, Nakhon Si Thammarat, Kerajaan AyutthayaPengabdian Jepang Kerajaan Ayutthaya PangkatOk-ya Senaphimuk (bahasa Thai: ออกญาเสนาภิมุข)Nama JepangKanji 山田 長政 Hiragana やまだ ながまさ TranskripsiRomanisasiYamada Nagamasa Ini adalah nama Jepang, nama keluarganya adalah Yamada. Yamada Nagamasa (山田 長政code: ja is depreca...

 

У этого топонима есть и другие значения, см. Катино. ДеревняКатино 57°43′29″ с. ш. 41°00′38″ в. д.HGЯO Страна  Россия Субъект Федерации Костромская область Муниципальный район Костромской Сельское поселение Минское История и география Высота центра 122 м Часовой поя

 

Achille Fould Información personalNacimiento 17 de noviembre de 1800 París (Primera República Francesa) Fallecimiento 5 de octubre de 1867 (66 años)Laloubère (Francia) Sepultura Cementerio del Père-Lachaise Nacionalidad FrancesaReligión Protestantismo Lengua materna Francés FamiliaPadres Beer Léon Fould Charlotte Brull Cónyuge Henriette Goldschmidt Información profesionalOcupación Político, banquero y financiero Cargos ocupados Diputado francésSenador del Segundo Imperioministre...

يفتقر محتوى هذه المقالة إلى الاستشهاد بمصادر. فضلاً، ساهم في تطوير هذه المقالة من خلال إضافة مصادر موثوق بها. أي معلومات غير موثقة يمكن التشكيك بها وإزالتها. (ديسمبر 2018) حارة النفيش  - حارة -  تقسيم إداري البلد  اليمن المحافظة محافظة صنعاء المديرية مديرية ضواحي ال

 

Limehouse Library A statue of Clement Attlee in its former position in front of the boarded-up Limehouse Library Limehouse Public Library is a historical building in Limehouse, London, formerly a public library. The library was first proposed for construction in 1888, but the required finances could not be raised until 1900 when John Passmore Edwards was approached for assistance. He subscribed a sum of £5,000[1] and he subsequently laid the foundation stone on 19 October that year. ...

 

إيرباص إيه 350 Airbus 350الشعارطائرة اإيرباص إيه 350-941 في أول طيران لهامعلومات عامةالنوع طائرة بدن واسعبلد الأصل عدة دولالمهام طيران تجاري سعر الوحدة ايه 350-800 : 245.5 مليون دولار ، 190 مليون يورو (2012) ايه 350-900 : 277.7 مليون دولار ، 215 مليون يورو (2012) ايه 350-1000 : 320.6 مليون دولار ، 248 مليو...

هذه المقالة يتيمة إذ تصل إليها مقالات أخرى قليلة جدًا. فضلًا، ساعد بإضافة وصلة إليها في مقالات متعلقة بها. (يونيو 2020) نهاية أسبوع قذرة (بالإنجليزية: Dirty Weekend)‏  الصنف فيلم إثارة  الموضوع قاتل متسلسل  تاريخ الصدور 1993  مدة العرض 102 دقيقة  البلد المملكة المتحدة  ال...

 

Latvian political party People's Party Tautas partijaLeaderAndris ŠķēleFounded1998Dissolved2011HeadquartersRigaIdeologyConservatism[1]National conservatism[2]Political positionCentre-rightNational affiliationFor a Good LatviaEuropean affiliationEuropean People's PartyEuropean Parliament groupEuropean People's Party (2004–2009)ColoursOrangePolitics of LatviaPolitical partiesElections The People's Party (Latvian: Tautas partija, TP) was a conservative[1] politi...

 

Constituent college of the University of Cambridge Hughes HallCambridge UniversityMargaret Wileman Building, Hughes HallArms of Hughes HallArms: Quarterly 1st and 3rd Gules an owl proper Or.; 5th Gules a torch proper Sable; 2nd, 4th and 6th ErmineScarf colours: light blue with three equally-spaced narrow stripes, the outer stripes of Cambridge blue and wider, the central stripe of white and narrower LocationMortimer Road (map)Full nameHughes Hall in the University of CambridgeAbbreviationHH&#...

This article needs additional citations for verification. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed.Find sources: Qatar Handball Association – news · newspapers · books · scholar · JSTOR (July 2018) (Learn how and when to remove this template message) Qatar Handball AssociationQHAIOC nationState of Qatar (QAT)National flagSportHandballOther sportsBeach handballWheelchair h...

 

Australian politician This article is about the Australian politician. For the American basketball player Maurice Mardy Collins, see Mardy Collins. Maurice CollinsMember of the Australian Parliamentfor WakefieldIn office17 November 1928 – 12 October 1929Preceded byRichard FosterSucceeded byCharles Hawker Personal detailsBorn1878Mount Bryan, South AustraliaDied9 August 1945 (aged 66–67)Political partyAustralian Country PartyOccupationGrazier Maurice Collins (1878 – ...

 

L-Isoleucine إيزوليوسين إيزوليوسين الاسم النظامي (IUPAC) Isoleucine أسماء أخرى 2-Amino-3-methylpentanoic acid المعرفات رقم CAS 73-32-5 Y بوب كيم (PubChem) 791 مواصفات الإدخال النصي المبسط للجزيئات CC[C@H](C)[C@@H](C(=O)O)N المعرف الكيميائي الدولي 1S/C6H13NO2/c1-3-4(2)5(7)6(8)9/h4-5H,3,7H2,1-2H3,(H,8,9)/t4-,5-/m0/s1 YKey: AGPKZVBTJJNPAG-WHFBIAKZSA-N Y الخواص صي...

Historic building in New South Wales This article is an orphan, as no other articles link to it. Please introduce links to this page from related articles; try the Find link tool for suggestions. (November 2019) The Macquarie Street Gatehouse, Parramatta Park The Macquarie Street Gatehouse at the Macquarie Street entrance of Parramatta Park in Parramatta, New South Wales, Australia, is a building of historical significance and is listed on the Heritage Register. It dates back to 1848, when th...

 

Italian manned torpedo design of late WWII Siluro San Bartolomeo History NameSiluro San Bartolomeo Commissioned1943 General characteristics Length6,77m Propulsion7.5 HP Motor Speed2.3–4 Knots ArmamentNormal: explosives charge 300 kg Version 2: 400 kg Version 3: Double 180/200 kg charge Testing Siluro San Bartolomeo The Siluro San Bartolomeo (St. Bartholomew Torpedo) was an Italian Human Torpedo designed during World War II, used by the Decima Flottiglia MAS for commando style operations. Wh...

 

1983 robbery and mass murder in Seattle, Washington Wah Mee massacrePart of mass shootings in the United StatesThe shuttered entrance of the Wah Mee Club (double doors at left), December 2007Location665 South King Street Seattle, Washington U.S.Coordinates47°35′53″N 122°19′27″W / 47.59806°N 122.32417°W / 47.59806; -122.32417DateFebruary 19, 1983; 40 years ago (1983-02-19) 12:30 a.m. (PST)Attack typeMass shooting, mass murder, armed robbery...

Кабу́ки[1] (яп. 歌舞伎, букв. «песня, танец, мастерство», «искусное пение и танцы») — один из видов традиционного театра Японии. Представляет собой синтез пения, музыки, танца и драмы. Исполнители кабуки используют сложный грим и костюмы с большой символической на...

 

American author and suffragist Eliza Caroline ObenchainBornEliza Caroline Calvert(1856-02-11)February 11, 1856Bowling Green, KentuckyDiedDecember 20, 1935(1935-12-20) (aged 79)Wichita Falls, TexasPen nameEliza Calvert HallEducationWestern Female SeminaryGenreShort storiesNotable worksAunt Jane of KentuckySpouseWilliam Alexander Obenchain (m. 1885) Eliza Caroline Lida Obenchain (née Calvert), (February 11, 1856 – December 20, 1935) was an American author, women's rights advocate, and s...

 

This article relies largely or entirely on a single source. Relevant discussion may be found on the talk page. Please help improve this article by introducing citations to additional sources.Find sources: 2023 San Cristóbal explosion – news · newspapers · books · scholar · JSTOR (August 2023) On 14 August 2023, an explosion occurred in San Cristóbal, Dominican Republic. It killed 28 people and caused 59 deaths. 2023 San Cristóbal explosionDateAugust...

Pour les articles homonymes, voir Ain. Ain Administration Pays France Région Auvergne-Rhône-Alpes Création du département 4 mars 1790 Chef-lieu(Préfecture) Bourg-en-Bresse Sous-préfectures BelleyGexNantua Président duconseil départemental Jean Deguerry (LR) Préfète Chantal Mauchet Code Insee 01 Code ISO 3166-2 FR-01 Code Eurostat NUTS-3 FR711 Démographie Gentilé Aindinois[1] Population 657 856 hab. (2020 ) Densité 114 hab./km2 Géographie Coordonnées 46° 05...

 

Argentine footballer Claudio Caniggia Caniggia in 1988Personal informationFull name Claudio Paul CaniggiaDate of birth (1967-01-09) 9 January 1967 (age 57)Place of birth Henderson, Buenos Aires, ArgentinaHeight 1.73 m (5 ft 8 in)Position(s) Forward, wingerSenior career*Years Team Apps (Gls)1985–1988 River Plate 53 (8)1988–1989 Hellas Verona 21 (3)1989–1992 Atalanta 85 (26)1992–1994 Roma 15 (4)1994–1995 Benfica 24 (8)1995–1998 Boca Juniors 58 (22)1999–2000 Ata...

 

Strategi Solo vs Squad di Free Fire: Cara Menang Mudah!