明盒正確性驗證是用 基于數學的方法證實一個過程與其規范相符。正像一個長除算法的正確性不是依賴除法而是用乘法來驗證的一樣，過程的正確性驗證也不是依賴細化過程來實現的，而是采用其他形式的手段。在凈室設計中廣泛用到的明盒驗證方法被稱為函數理論正確性驗證。運用函數理論方法，每個控制結構都會與它的預期函數規范相比較。當所有的子控制結構被驗證時，整個過程也就被驗證了。通常在小組評審中實現驗證。
正確性定理(Linger, Mills andWitts 1978)為每個明盒控制結構定義了正確性問題，如表4.4所示。不同的控制結構中問題的數目不同：順序結構是1個、分支結構是2個、而循環結構是3個。由于任何大小的過程都潛在地含有無限多條執行路徑，所以不可能通過跟蹤路徑來驗證。不過，過程包含的結構卻是有取勝的。通過在有取勝的步驟里驗證每個結構，就可以在有陰的步驟里驗證每個結構，就可以在有限的步驟里實現系統化的過程驗證。正確性問題可應用于多種層次，從口頭的證明到詳細的書面證明。嚴格的層次劃分決定于風險和回報，這是個商業性問題。經驗表明小組評審時進行口頭的證明對開發高質量軟件是非常有效的。
表 明盒控制結構的正確性問題
在表中，分析了對應的控制結構中的執行路徑后，就可以確定正確性問題了.對順序結構，惟一的路徑是h跟隨g，所以正確性問題就是：這些功能結點必須執行這個結構的預期函數?.
對ifthen結構，當p真，惟一的路徑是g;正確性就是g必須執行?.當p假，惟一的路徑為do nothing,正確性就是doing nothing必須執行?.也就是說，?必須在p為假時已經完成.對ifthenelse的分析是類似的，只有p為假時有區別：當p為假時，惟一的路徑是h，正確性為h必須執行?.
循環結構的正確性難以直接證明.不過，可通過驗證一個等價的相對簡單的ifthenelse結構來完成對一個可終止的循環的正確性檢驗，這種ifrhenelse結構是通過對循環的執行路徑的變換而得到的.例如，考慮在圖4.5的第一個以圖形形式顯示的whiledo結構.在圖下的第二個圖的中間，創建了一個等價的ifthenelse，其中用whiletest(p)作為斷言.對ifthenelse的真分支，先執行g ，然后是whiledo結構，和原來的whiledo的執行一樣.對假分支，什么也不做.也和原來的whiledo的執行一樣.因此，這個新ifthenelse結構和上面的whiledo結構是等價的.但我們要求真分支上的whiledo結構與?等價，因此將它替換為?，得到圖4.5的第三個圖的結構.這樣，whiledo的正確性問題就變成了ifrhenelse和順序結構的正確性問題.通過分析irthenelse的執行就可以解決whiledo的正確性問題.真路徑要求g和其后的?必須執行?，假路徑是空操作執行?.
為解釋在條件為真時的正確性問題，考慮如下while do :
[read remaining records from file,if any ]
while
[records remain]
do
[read next record]
enddo
正確性問題是：當徨測試為真時，g和其后的?能完成?嗎?它被表達為如下：
當[records remain]為真，
[read next record]和其后的[read remaining records from file,if any ]完成[read remaining records from file,if any]
回答為是.因為對于一個初始為不空的文件(由真什斷言保證).[read next record](表示為g)就會讀取一些數據，然后文件可能為空，也可能不空，而[read remain record](表示?)的功能是讀非空文件或對空文件什么也不做.這樣如果文件的初始化狀態是一樣的，新的結構(g和隨后的?)就有著和預期函數[read remaining records from file,if any ]有著同樣的效果.
注意除了whiledo的真假問題以外，第三個問題是循環能否終止，基于循環的單調性最終要導致終止條件為假.例如 ，這里的循環從文件中讀取連續的記錄保證了文件被讀完時會終止.對于dountil和dowhiledo的分析是類似的.
文章來源于領測軟件測試網 http://www.kjueaiud.com/
