FINDING LOOPS INVARIANTS BY A BACKWARD METHOD USING INDUCTIVE ASSERTIONS AND PROVING THEM CORRECT USING MATHEMATICAL INDUCTION

Ramon A. Mata-Toledo ()
Additional contact information
Ramon A. Mata-Toledo: Rollins College, USA

Journal of Information Systems & Operations Management, 2021, vol. 15, issue 2, 215-222

Abstract: The method of proving programs correct has been an endeavor of computer scientists for decades now. However, little progress, in comparison, with some other aspects of computing, has been made on this respect. The current method using Hoare’ Triple and the Dikjstra’ pre- and post-conditions are not easy to follow by most students. The method of Inductive assertions has been tried too to find loop invariants using the so-called ‘forward method.†The author has found that this ‘forward method†is still difficult and, for some program, even more difficult to follow than the Hoare’s Triple and Dijkstra’ pre and post conditions. In this paper the author proposes a “backward method†using Inductive assertion which starts at the end of the program and works its way up to the beginning of the program. This method has been proven successful the author’s classes where the student has found the method easier to use and understand.

Date: 2021
References: View complete reference list from CitEc
Citations:

Downloads: (external link)
http://www.rebe.rau.ro/RePEc/rau/jisomg/WI21/JISOM-WI21-A19.pdf (application/pdf)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:rau:jisomg:v:15:y:2021:i:2:p:215-222

Access Statistics for this article

More articles in Journal of Information Systems & Operations Management from Romanian-American University Contact information at EDIRC.
Bibliographic data for series maintained by Alex Tabusca ().