Back to Search
Start Over
Training Difficulties in Deductive Methods of Verification and Synthesis of Program
- Source :
- International Journal of Advanced Computer Science and Applications. 9
- Publication Year :
- 2018
- Publisher :
- The Science and Information Organization, 2018.
-
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.
- Subjects :
- Flowchart
Loop invariant
Correctness
General Computer Science
business.industry
Computer science
Programming language
Proof assistant
HOL
computer.software_genre
law.invention
Predicate transformer semantics
Software
law
Formal specification
Formal language
business
Software analysis pattern
computer
Subjects
Details
- ISSN :
- 21565570 and 2158107X
- Volume :
- 9
- Database :
- OpenAIRE
- Journal :
- International Journal of Advanced Computer Science and Applications
- Accession number :
- edsair.doi...........29539aed731c59238e1737fc4da17868