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 89
- Downloads 0
Self-Healing Hybrid Protection Architecture for Passive Optical Networks
Expanding size of passive optical networks (PONs) along with high availability expectation makes the reliability performance a crucial need. Most protection architectures utilize redundant network components to enhance n...
A Knowledge-based Topic Modeling Approach for Automatic Topic Labeling
Probabilistic topic models, which aim to discover latent topics in text corpora define each document as a multinomial distributions over topics and each topic as a multinomial distributions over words. Although, humans c...
M/M/1/n+Flush/n Model to Enhance the QoS for Cluster Heads in MANETs
Clustering in MANET is important to achieve scalability in presence of large networks and high mobility in order to maintain the Quality of Services (QoS) of the network. Improving the QoS is the most important and cruci...
Impact of Cloud Computing on ERP implementations in Higher Education
Penetration of Higher Education in all regions is increasing all over the globe at a very fast pace. With the increase in the number of institutions offering higher education, ERP implementations has become one of the ke...
Analysis of End-to-End Packet Delay for Internet of Things in Wireless Communications
Accurate and efficient estimators for End to End delay (E2EPD) plays a significant and critical role in Quality of Service (QoS) provisioning in Internet of Things (IoT) wireless communications. The purpose of this paper...