Zelkowitz MV.  1990.  A functional correctness model of program verification. Computer. 23(11):30-39.