Training Difficulties in Deductive Methods of Verification and Synthesis of Program
Journal Title: International Journal of Advanced Computer Science & Applications - Year 2018, Vol 9, Issue 7
Abstract
The article analyzes the difficulties which Bachelor Degree in Informatics and Computer Sciences students encounter in the process of being trained in applying deductive methods of verification and synthesis of procedural programs. Education in this field is an important step towards moving from classical software engineering to formal software engineering. The training in deductive methods is done in the introductory courses in programming in some Bulgarian universities. It includes: Floyd’s method for proving partial and total correctness of flowchart programs; Hoare’s method of verification of programs; and Djikstra’s method of transforming predicates for verification and synthesis of Algol−like programs. The difficulties which occurred during the defining of the specification of the program, which is subjected to verification or synthesis; choosing a loop invariant and loop termination function; finding the weakest precondition; proving the formulated verifying conditions, are discussed in the paper. Means of overcoming these difficulties is proposed. Conclusions are drawn in order to improve the training in the field. Special attention is dedicated to motivating the use of specific tools for software analysis, such as interactive theorem proving system HOL, the software analyzers Frama−C and its WP plug−in, as well as the formal language ACSL, which allows formal specification of properties of C/C++ programs.
Authors and Affiliations
Magdalina Todorova, Daniela Orozova
Keywords
Related Articles
- EP ID EP357201
- DOI 10.14569/IJACSA.2018.090703
- Views 61
- Downloads 0
Performance Comparison between MAI and Noise Constrained LMS Algorithm for MIMO CDMA DFE and Linear Equalizers
This paper presents a performance comparison between a constrained least mean squared algorithm for MIMO CDMA decision feedback equalizer and linear equalizer. Both algorithms are constrained on the length of spreading s...
Using Brain Imaging to Gauge Difficulties in Processing Ambiguous Text by Non-native Speakers
Processing ambiguous text is an ever challenging problem for humans. In this study, we investigate how native-Arabic speakers face problems in processing their non-native English language text which involves ambiguity. A...
The Impact of Privacy Concerns and Perceived Vulnerability to Risks on Users Privacy Protection Behaviors on SNS: A Structural Equation Model
This research paper investigates Saudi users’ awareness levels about privacy policies in Social Networking Sites (SNSs), their privacy concerns and their privacy protection measures. For this purpose, a research model th...
Automatic License Plate Localization Using Intrinsic Rules Saliency
This paper addresses an intrinsic rule-based license plate localization (LPL) algorithm. It first selects candidate regions, and then filters negative regions with statistical constraints. Key contribution is assig...
Gene Optimized Deep Neural Round Robin Workflow Scheduling in Cloud
Workflow scheduling is a key problem to be solved in the cloud to increases the quality of services. Few research works have been designed for performing workflow scheduling using different techniques. But, scheduling pe...