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 100
- Downloads 0
An Embedded Modbus Compliant Interactive Operator Interface for a Variable Frequency Drive Using Rs 485
The paper proposes the architecture and software design of a Modbus Compliant Operator Interface Panel (MCOIP) for a high speed Variable Frequency Drive (VFD) – a state of the art embedded design that offers several key...
An Analysis on Natural Image Small Patches
The method of computational homology is used to analyze natural image 8 × 8 and 9x9-patches locally. Our experimental results show that there exist subspaces of the spaces of 8x8 and 9x9-patches that are topologically eq...
A Categorical Model of Process Co-Simulation
A set of dynamic systems in which some entities undergo transformations, or receive certain services in successive phases, can be modeled by processes. The specification of a process consists of a description of the prop...
A Survey on Smartphone-Based Accident Reporting and Guidance Systems
Every day, around the world, a large percentage of people die from road accidents and falls. One of the reasons for a person's death during accidents is the unavailability of first aid, due to the delay in informing abou...
A Robust Algorithm of Forgery Detection in Copy-Move and Spliced Images
The paper presents a new method to detect forgery by copy-move, splicing or both in the same image. Multiscale, which limits the computational complexity, is used to check if there is any counterfeit in the image. By app...