Diagrammatic reasoning in program construction

Abstract:

Correctness is proved formally using pbkp_redicate logic, which requires certain mathematical maturity from the programmer. Proving program correctness has a significant side-benefit of leading step-wise development of programs. Computer programming is taught as a craft with no mental framework as the tool to guide the development. This paper proposes a diagrammatic notation for representing the pbkp_redicates, with a minimal blend of symbolic notation, thus providing an easy-to-use tool to achieve the same benefit. This paper is also intended to build a software tool that could be used for drawing the diagrammatic pbkp_redicates in the course of construction of the program. Using this diagrammatic notation, one can represent pbkp_redicates that should hold at strategic points in the program, such as the pre-condition, the post-condition, and the loop invariant. Using the software tool, the user can diagrammatically represent pbkp_redicates, verify the program using a theorem prover, and generate an outline of the code. © 2011 IEEE.

Año de publicación:

2011

Keywords:

• Invariant Based Programming
• Diagrammatic Reasoning
• Program Correctness
• Formal Methods

Fuente:

scopus