Diagrammatic reasoning in program construction

Correctness is proved formally using predicate 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 predicates, 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 predicates in the course of construction of the program. Using this diagrammatic notation, one can represent predicates 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 predicates, verify the program using a theorem prover, and generate an outline of the code.