クラス不変

コンピュータ プログラミング、特にオブジェクト指向プログラミングでは、クラス不変条件(または型不変条件) は、クラスのオブジェクトを制約するために使用される不変条件です。クラスのメソッドは不変条件を保持する必要があります。クラス不変条件は、オブジェクトに格納されている状態を制約します。

クラス不変条件は構築中に確立され、パブリック メソッドの呼び出し間で常に維持されます。パブリック関数が終了する前に不変条件が復元される限り、関数内のコードは不変条件を破ることができます。並行性では、メソッド内で不変条件を維持するには通常、ミューテックスを使用して状態をロックすることによってクリティカル セクションを確立する必要があります。

オブジェクト不変条件、または表現不変条件は、オブジェクトの状態に関係なく損なわれない不変プロパティのセットで構成されるコンピュータ プログラミング構造です。これにより、オブジェクトが常に定義済みの条件を満たすことが保証され、メソッドは不正確な推定を行うリスクなしに常にオブジェクトを参照できます。クラス不変条件を定義すると、プログラマーとテスターはソフトウェア テスト中により多くのバグを検出できるようになります。

オブジェクト指向ソフトウェアにおけるクラス不変条件の有用な効果は、継承の存在によって強化されます。クラス不変条件は継承されます。つまり、「クラスのすべての親の不変条件がクラス自体に適用されます。」^[1]

継承により、子孫クラスは親クラスの実装データを変更できるようになるため、子孫クラスがインスタンスの状態を親クラスの観点から無効にするような方法で変更することが可能になります。このような不正な子孫に対する懸念は、オブジェクト指向ソフトウェア設計者が継承よりも合成を優先する理由の 1 つです(つまり、継承はカプセル化を破壊します)。^[2]

ただし、クラス不変条件は継承されるため、特定のクラスのクラス不変条件は、そのクラスに直接コード化された不変条件アサーションと、そのクラスの親から継承されたすべての不変条件節から構成されます。つまり、子孫クラスが親の実装データにアクセスできる場合でも、クラス不変条件によって、実行時に無効なインスタンスを生成するような方法でそれらのデータを操作できないようにすることができます。

Python、^[3] PHP、^[4] JavaScript、^[要出典] C++、Javaなどの一般的なプログラミング言語は、デフォルトでアサーションをサポートしており、これを使用してクラスの不変条件を定義できます。クラスで不変条件を実装する一般的なパターンは、不変条件が満たされない場合にクラスのコンストラクターが例外をスローすることです。メソッドは不変条件を保持するため、不変条件の有効性を前提とすることができ、明示的にチェックする必要はありません。

クラス不変条件は、契約による設計の必須コンポーネントです。したがって、Eiffel、Ada、Dなど、契約による設計を完全にネイティブにサポートするプログラミング言語は、クラス不変条件も完全にサポートします。

C++の場合、Loki ライブラリは、クラス不変条件、静的データ不変条件、および例外安全性をチェックするためのフレームワークを提供します。

Java には、クラス不変条件をより堅牢に定義する方法を提供する、 Java モデリング言語と呼ばれるより強力なツールがあります。

Adaプログラミング言語は、型不変条件 (および事前条件と事後条件、サブタイプ述語など) をネイティブにサポートしています。型不変条件は、プライベート型 (たとえば、その抽象プロパティ間の関係を定義するため) または完全定義 (通常は型の実装の正しさを検証するため) に指定できます。^[5] 以下は、論理スタックを表すために使用されるプライベート型の完全定義に指定された型不変条件の例です。実装では配列を使用し、型不変条件は安全性の証明を可能にする実装の特定のプロパティを指定します。この場合、不変条件は、論理深度 N のスタックに対して、配列の最初の N 要素が有効な値であることを保証します。Stack 型の Default_Initial_Condition は、空のスタックを指定することにより、不変条件の初期値が真であることを保証し、Push は不変条件を保持します。不変条件が真実であれば、Pop はスタックの最上部が有効な値であるという事実に頼ることができ、これは Pop の事後条件を証明するために必要です。より複雑な型不変条件であれば、Pop が対応する Push に渡された値を返すなど、完全な機能的正しさを証明できますが、この場合は、Pop が Invalid_Value を返さないことを証明しようとしているだけです。

ジェネリック
    型 Itemは プライベートです 。Invalid_Value :はItem内にあります。パッケージStacksは型Stack ( Max_Depth : Positive )がプライベートで、Default_Initial_Condition => Is_Empty ( Stack )です。
       
  
        
            

    関数 Is_Empty ( S  :スタック内 )はBooleanを返します。関数Is_Full ( S :スタック内)はBooleanを返します。  
         

    手順 Push ( S  : in  out  Stack ;  I  : in  Item ) 、 
        Pre => not Is_Full ( S ) 、I /= Invalid_Value 、Post => not Is_Empty ( S )の場合。 手順Pop ( S : in out Stack ; I : out Item ) 、 Pre => not Is_Empty ( S )、Post => not Is_Full ( S )の場合、 I /= Invalid_Valueの場合。プライベート型Item_Arrayは、 Itemの配列(正の範囲<> )です。        
                
           
             
                    

            

    type  Stack ( Max_Depth  : Positive ) は、 レコード
        Length  :  Natural  :=  0 ; 
        Data  :  Item_Array  ( 1  ..  Max_Depth )  :=  ( others  =>  Invalid_Value );レコード
    の終了
        Type_Invariant => Length <= Max_Depthであり、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プログラミング言語は、クラス不変条件やその他の契約プログラミング技術をネイティブにサポートしています。以下は公式ドキュメントからの例です。^[6]

クラスDate { int日; int時間;  
   
   

  不変() { assert (日>= 1 &&日<= 31 ); assert (時間>= 0 &&時間<= 23 ); } } 
          
          
  

Eiffelでは、クラス不変条件はキーワード に続くクラスの末尾に表示されますinvariant。

クラス
日付	

作成
する	

機能{ NONE } -- 初期化  

	make ( a_day : INTEGER ; a_hour : INTEGER ) -- `Current' を `a_day' と `a_hour' で初期化します。valid_day : a_day >= 1かつa_day <= 31であることが必要ですvalid_hour : a_hour >= 0かつa_hour <= 23 であることが必要ですdo day := a_day hour := a_hour であることが必要ですensure day_set : day = a_day hour_set : hour = a_hour であることが必要です end    
			
		
			       
			       
		
			  
			  
		
			   
			   
		

機能-- アクセス 

	day : INTEGER -- 「現在の」月の日 
		

	hour : INTEGER -- 「現在の」時刻 
		

機能-- 要素の変更 

	set_day ( a_day : INTEGER ) -- `day' を `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 ) -- `hour' を `a_hour' に設定するrequire valid_argument : a_hour >= 0 and a_hour <= 23 do hour := a_hour Ensure hour_set : hour = a_hour end  
			
		
			       
		
			  
		
			   
		

不変
valid_day :日>= 1かつ日<= 31 valid_hour :時間>= 0かつ時間<= 23終了	       
	       

Loki (C++)ライブラリは、クラス不変条件、静的データ不変条件、および例外安全性レベルをチェックするための、Richard Sposato によって書かれたフレームワークを提供します。

これは、クラスが Loki::Checker を使用して、オブジェクトが変更された後も不変条件が真であることを確認する方法の例です。 この例では、geopoint オブジェクトを使用して、地球上の位置を緯度と経度の座標として保存します。

ジオポイント不変量は次のとおりです。

• 緯度は北緯 90 度を超えてはなりません。
• 緯度は南-90°未満であってはなりません。
• 経度は東経180度を超えてはなりません。
• 経度は西経 -180° 未満であってはなりません。

#include <loki/Checker.h>   // クラスの不変条件をチェックするために必要です。 

#include <度数.hpp> 

クラスGeoPoint { public : GeoPoint (緯度 (度) 、経度(度) );  
 
     

  /// Move 関数は GeoPoint の位置を移動します。void 
Move ( Degrees latitude_change , Degrees longitude_change ) { //チェッカー オブジェクトは関数の入口と出口で IsValid を呼び出して、このGeoPoint オブジェクトが有効であることを証明します。また、チェッカーは GeoPoint::Move 関数が例外をスローしないことも保証します。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 は、多くの関数で有効性チェックを実行し、   コードが不変条件に違反していないか、コンテンツが変更されていないか、または   関数が例外をスローしていないかを判断します。   */ using CheckFor = :: Loki :: CheckFor < const GeoPoint > ;  



      

  /// この関数は、すべてのオブジェクトの不変条件をチェックします。
bool IsValid () const { assert ( this != nullptr ); assert ( latitude_ >= -90.0 ); assert ( latitude_ <= 90.0 ); assert ( longitude_ >= -180.0 ); assert ( longitude_ <= 180.0 ); return true ; }     
      
      
      
      
      
     
  

  緯度_ ; ///< 赤道からの度数。正は北、負は///< 南。経度_ ; ///< 本初子午線からの度数。正は東、負は ///< 西。}    
                       
     
                       

これは、 Java モデリング言語を使用したJava プログラミング言語のクラス不変条件の例です。不変条件は、コンストラクタの終了後、およびすべてのパブリック メンバー関数の入口と出口で true に保たれる必要があります。パブリック メンバー関数は、クラス不変条件を確実にするために、 前提条件と事後条件を定義する必要があります。

パブリッククラスDate { int /*@spec_public@*/日; int /*@spec_public@*/時間;   
      
      

    /*@invariant day >= 1 && day <= 31; @*/ //クラス不変/*@invariant hour >= 0 && hour <= 23; @*/ //クラス不変 
     

    /*@ 
    @requires d >= 1 && d <= 31; 
    @requires h >= 0 && h <= 23; 
    @*/ 
public Date ( int d , int h ) { // コンストラクター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 ; } }