A Proof Rule for While Loop in VDM

Jiang Xinjie, Xu Yongsen. A Proof Rule for While Loop in VDM[J]. Journal of Computer Science and Technology, 1989, 4(2): 178-183.

Citation:

Jiang Xinjie, Xu Yongsen. A Proof Rule for While Loop in VDM[J]. Journal of Computer Science and Technology, 1989, 4(2): 178-183.

Citation:

Jiang Xinjie, Xu Yongsen. A Proof Rule for While Loop in VDM[J]. Journal of Computer Science and Technology, 1989, 4(2): 178-183.

Abstract

A proof rule for while loop which can be used in justification of program w.r.t. specifications using two-state post-conditions is presented in this paper, accompanied with a soundness proof and a comparison with Aczel's rule for while loop.

FullText(HTML)

Export File