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 103
- Downloads 0
Novel Geo-Location Technique for Tourism Guide and Emergency Evacuation at Grand Mosque Al Haram Makkah
Grand Mosque AL Haram is always crowded with pilgrim. The most concentration of crowd happens during Hajj season. Even the grand mosque is already furnished with a lot of route sign board, exit or emergency sign boards....
Fuzzy Logic Tsukamoto for SARIMA On Automation of Bandwidth Allocation
The wireless network is used in different fields to enhance information transfer between remote areas. In the education area, it can support knowledge transfer among academic member including lecturers, students, and sta...
Challenges of Medical Records Interoperability in Developing Countries: A Case Study of the University Teaching Hospital in Zambia
The University Teaching Hospital (UTH) is an integral national referral Hospital made up of eight departments. Standardized systems and semantic interoperability is key for successful flow of patient information from one...
A Machine Learning Approach for Predicting Nicotine Dependence
An examination of the ability of machine learning methodologies in classifying women Waterpipe (WP) smoker’s level of nicotine dependence is proposed in this work. In this study, we developed a classifier that predicts t...
An Image Encryption Technique based on Chaotic S-Box and Arnold Transform
In recent years, chaos has been extensively used in cryptographic systems. In this regard, one dimensional chaotic maps gained increased attention because of their intrinsic simplicity and ease in application. Many image...