Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

CHARME

2003

Springer

2003

Springer

This paper shows how classic inductive assertions can be used in conjunction with an operational semantics to prove partial correctness properties of programs. The method imposes only the proof obligations that would be produced by a veriﬁcation condition generator but does not require the deﬁnition of a veriﬁcation condition generation. The paper focuses on iterative programs but recursive programs are brieﬂy discussed. Assertions are attached to the program by deﬁning a predicate on states. This predicate is then “completed” to an alleged invariant by the deﬁnition of a partial function deﬁned in terms of the state transition function of the operational semantics. If this alleged invariant can be proved to be an invariant under the state transition function, it follows that the assertions are true every time they are encountered in execution and thus that the post-condition is true if reached from a state satisfying the pre-condition. But because of the manner in wh...

Related Content

Added |
06 Jul 2010 |

Updated |
06 Jul 2010 |

Type |
Conference |

Year |
2003 |

Where |
CHARME |

Authors |
J. Strother Moore |

Comments (0)