Microsoft が提供する C/C++ ヘッダファイルにおける事前条件・事後条件の充実っぷりは異常

ふむ.
むしろ Microsoft の開発現場で,一番 DbC が流行っているのが Visual C++ 関連だと思うのですが.Header Annotations とか SAL AnnotationsC/C++ コード障害の検出と修正 等.
最近の Visual C++ のインクルードファイルや Windows SDKs 以下のインクルードファイルを見ていても,事前条件・事後条件の充実っぷりは異常.その規模は既に COM 全盛期の IDL を凌ぎます.
あれは手で書いているんでしょうかねぇ? 何か DSL から C/C++ のヘッダファイルを自動生成していてもおかしくない気もしますが,はて.

整数範囲注釈

そういえば Visual C++ 2008 SP1 のコード検証は,Header Annotations の整数範囲注釈を活用していないように見えるのですが,誰かその辺の事情をご存じだったりしませんかね?
整数範囲注釈は,例えばこんな感じで引数の事前条件・事後条件を記述するものです.他にも,フィールドや関数戻り値の範囲に注釈を記述することも可能です.

#include <specstrings.h>
#include <iostream>

// 事前条件: i は 64 以上 127 以下
void foo( __in_range(64, 127) int i )
{
    std::cout << i;
}
// 事前条件: i は 50未満
void bar( __in_range(<, 50) int i )
{
    std::cout << i;
}
// 事後条件: iptr は NULL ではなく,*iptr は 11
void buz( __notnull __deref_out_range(==, 11) int* iptr )
{
    *iptr = 10;
}

詳しい文法については specstrings.h にコメントで書かれています.
整数範囲注釈は,Windows SDK 6.0 以降でちらほら使われ始め,最近であれば Direct3D10 のヘッダファイルでも使用されています.例として ID3D10Device::GSSetConstantBuffers の宣言.

virtual void STDMETHODCALLTYPE GSSetConstantBuffers( 
    /*  */ 
    __in_range( 0, D3D10_COMMONSHADER_CONSTANT_BUFFER_API_SLOT_COUNT - 1 )  UINT StartSlot,
    /*  */ 
    __in_range( 0, D3D10_COMMONSHADER_CONSTANT_BUFFER_API_SLOT_COUNT - StartSlot )  UINT NumBuffers,
    /*  */ 
    __in_ecount(NumBuffers)  ID3D10Buffer *const *ppConstantBuffers) = 0;

ただ,手元の環境 (Visual Studio Team Suite 2008 SP1) では,整数範囲制約への違反が静的コード検証で指摘されたことが一度もないんですよな.いまのところ文字通り「注釈」だけなのかなと.__notnull とかは,静的コード分析で活用されているのを見たことがあるんですけどねぇ.

「Win32 API といえばシステムハンガリアン」という印象で止まっていませんか?

Win32 API といえばシステムハンガリアン,というのは比較的有名かと思いますが,その印象で時間が止まっている人は,もう一度最近のヘッダファイルを読み直してみることをおすすめします.今では,C/C++ の型から区別が付かない数多くの情報がヘッダファイルに記述されるようになっており,ヘッダファイルは MSDN Library を補う第二のドキュメントになりつつあります.
時代も徐々に変わるのですよ.
将来的には,ドキュメント自動生成や,IntelliSense との統合なんかも期待ですな.