Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 4 of 4
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 …
How To Speed Up Software Migration And Modernization: Successful Strategies Developed By Precisiating Expert Knowledge, Francisco Zapata, Octavio Lerma, Leobardo Valera, Vladik Kreinovich
How To Speed Up Software Migration And Modernization: Successful Strategies Developed By Precisiating Expert Knowledge, Francisco Zapata, Octavio Lerma, Leobardo Valera, Vladik Kreinovich
Departmental Technical Reports (CS)
Computers are getting faster and faster; the operating systems are getting more sophisticated. Often, these improvements necessitate that we migrate the existing software to the new platform. In the ideal world, the migrated software should run perfectly well on a new platform; however, in reality, when we try that, thousands of errors appear, errors that need correcting. As a result, software migration is usually a very time-consuming process. A natural way to speed up this process is to take into account that errors naturally fall into different categories, and often, a common correction can be applied to all error from …
Optimizing Pred(25) Is Np-Hard, Martine Ceberio, Olga Kosheleva, Vladik Kreinovich
Optimizing Pred(25) Is Np-Hard, Martine Ceberio, Olga Kosheleva, Vladik Kreinovich
Departmental Technical Reports (CS)
Usually, in data processing, to find the parameters of the models that best fits the data, people use the Least Squares method. One of the advantages of this method is that for linear models, it leads to an easy-to-solve system of linear equations. A limitation of this method is that even a single outlier can ruin the corresponding estimates; thus, more robust methods are needed. In particular, in software engineering, often, a more robust pred(25) method is used, in which we maximize the number of cases in which the model's prediction is within the 25% range of the observations. In …