Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 2 of 2
Full-Text Articles in Physical Sciences and Mathematics
A Systematic Derivation Of Loop Specifications Using Patterns, Aditi Barua, Yoonsik Cheon
A Systematic Derivation Of Loop Specifications Using Patterns, Aditi Barua, Yoonsik Cheon
Departmental Technical Reports (CS)
Any non-trivial program contains loop control structures such as while, for and do statements. A formal correctness proof of code containing loop control structures is typically performed using an induction-based technique, and oftentimes the most challenging step of an inductive proof is formulating a correct induction hypothesis. An incorrectly-formulated induction hypothesis will surely lead to a failure of the proof. In this paper we propose a systematic approach for formulating and driving specifications of loop control structures for formal analysis and verification of programs. We explain our approach using while loops and a functional program verification technique in which a …
Toward Unification Of Explicit And Implicit Invocation-Style Programming, Yoonsik Cheon
Toward Unification Of Explicit And Implicit Invocation-Style Programming, Yoonsik Cheon
Departmental Technical Reports (CS)
Subprograms like procedures and methods can be invoked explicitly or implicitly; in implicit invocation, an event implicitly causes the invocation of subprograms that are registered an interest in the event. Mixing these two styles is common in programming and often unavoidable in developing such software as GUI applications and event-based control systems. However, it isn't also uncommon for the mixed use to complicate programming logic and thus produce unclean code, code that is hard to read and understand. We show, through a small but realistic example, that the problem is not much on mixing two different styles itself but more …